| 2018 | Peregrine: A Tool for the Analysis of Population Protocols. | Michael Blondin, Javier Esparza, Stefan Jaax |
| 2018 | A Direct Encoding for NNC Polyhedra. | Anna Becchi, Enea Zaffanella |
| 2018 | Model Checking Indistinguishability of Randomized Security Protocols. | Matthew S. Bauer, Rohit Chadha, A. Prasad Sistla, Mahesh Viswanathan |
| 2018 | A Counting Semantics for Monitoring LTL Specifications over Finite Traces. | Ezio Bartocci, Roderick Bloem, Dejan Nickovic, Franz Rck |
| 2018 | Synthesis of Asynchronous Reactive Programs from Temporal Specifications. | Suguman Bansal, Kedar S. Namjoshi, Yaniv Sa'ar |
| 2018 | Automata vs Linear-Programming Discounted-Sum Inclusion. | Suguman Bansal, Swarat Chaudhuri, Moshe Y. Vardi |
| 2018 | Let this Graph Be Your Witness! - An Attestor for Verifying Java Pointer Programs. | Hannah Arndt, Christina Jansen, Joost-Pieter Katoen, Christoph Matheja, Thomas Noll |
| 2018 | The Learnability of Symbolic Automata. | George Argyros, Loris D'Antoni |
| 2018 | Constrained Dynamic Partial Order Reduction. | Elvira Albert, Miguel Gmez-Zamalloa, Miguel Isabel, Albert Rubio |
| 2018 | Constraint-Based Synthesis of Coupling Proofs. | Aws Albarghouthi, Justin Hsu |
| 2018 | What's Hard About Boolean Functional Synthesis? | S. Akshay, Supratik Chakraborty, Shubham Goel, Sumith Kulal, Shetal Shah |
| 2018 | Counterexample Guided Inductive Synthesis Modulo Theories. | Alessandro Abate, Cristina David, Pascal Kesseli, Daniel Kroening, Elizabeth Polgreen |
| 2017 | Starling: Lightweight Concurrency Verification with Views. | Matt Windsor, Mike Dodds, Ben Simner, Matthew J. Parkinson |
| 2017 | Compositional Model Checking with Incremental Counter-Example Construction. | Anton Wijs, Thomas Neele |
| 2017 | Logical Clustering and Learning for Time-Series Data. | Marcell Vazquez-Chanlatte, Jyotirmoy V. Deshmukh, Xiaoqing Jin, Sanjit A. Seshia |
| 2017 | Program Verification Under Weak Memory Consistency Using Separation Logic. | Viktor Vafeiadis |
| 2017 | Automating Induction for Solving Horn Clauses. | Hiroshi Unno, Sho Torii, Hiroki Sakamoto |
| 2017 | Montre: A Tool for Monitoring Timed Regular Expressions. | Dogan Ulus |
| 2017 | Model Counting for Recursively-Defined Strings. | Minh-Thai Trinh, Duc-Hiep Chu, Joxan Jaffar |
| 2017 | Ascertaining Uncertainty for Efficient Exact Cache Analysis. | Valentin Touzeau, Claire Maza, David Monniaux, Jan Reineke |
| 2017 | On Expansion and Resolution in CEGAR Based QBF Solving. | Leander Tentrup |
| 2017 | Abstract Interpretation with Unfoldings. | Marcelo Sousa, Csar Rodrguez, Vijay Victor D'Silva, Daniel Kroening |
| 2017 | Maximum Satisfiability in Software Analysis: Applications and Techniques. | Xujie Si, Xin Zhang, Radu Grigore, Mayur Naik |
| 2017 | E-QED: Electrical Bug Localization During Post-silicon Validation Enabled by Quick Error Detection and Formal Methods. | Eshan Singh, Clark W. Barrett, Subhasish Mitra |
| 2017 | Runtime Monitoring with Recovery of the SENT Communication Protocol. | Konstantin Selyunin, Stefan Jaksic, Thang Nguyen, Christian Reidl, Udo Hafner, Ezio Bartocci, Dejan Nickovic, Radu Grosu |