| 2015 | An SMT-based Approach to Fair Termination Analysis. | Javier Esparza, Philipp J. Meyer |
| 2015 | The Genesis and Development of Model Checking: Fact vs. Fiction. | Allan Emerson |
| 2015 | Abductive Inference and Its Applications in Program Analysis, Verification, and Synthesis. | Isil Dillig |
| 2015 | Formal Verification of Automatic Circuit Transformations for Fault-Tolerance. | Dmitry Burlyaev, Pascal Fradet |
| 2015 | Compositional Safety Verification with Max-SMT. | Marc Brockschmidt, Daniel Larraz, Albert Oliveras, Enric Rodrguez-Carbonell, Albert Rubio |
| 2015 | Reactive Synthesis. | Roderick Bloem |
| 2015 | Universal Boolean Functional Vectors. | Jesse Bingham |
| 2015 | Compositional Reasoning Gotchas in Practice. | Chirag Agarwal, Paul Hylander, Yogesh Mahajan, Jonathan Michelson, Vigyan Singhal |
| 2015 | Verification of Cache Coherence Protocols wrt. Trace Filters. | Parosh Aziz Abdulla, Mohamed Faouzi Atig, Zeinab Ganjei, Ahmed Rezine, Yunyun Zhu |
| 2015 | IC3 Software Model Checking on Control Flow Automata. | Tim Lange, Martin R. Neuhuer, Thomas Noll |
| 2014 | Predicate abstraction for reactive synthesis. | Adam Walker, Leonid Ryzhyk |
| 2014 | Reducing CTL-live model checking to first-order logic validity checking. | Amirhossein Vakili, Nancy A. Day |
| 2014 | Patient-specific models from inter-patient biological models and clinical records. | Enrico Tronci, Toni Mancini, Ivano Salvo, Stefano Sinisi, Federico Mari, Igor Melatti, Annalisa Massini, Francesco Dav, Thomas Dierkes, Rainald Ehrig, Susanna Rblitz, Brigitte Leeners, Tillmann H. C. Kruger, Marcel Egli, Fabian Ille |
| 2014 | Using interval constraint propagation for pseudo-Boolean constraint solving. | Karsten Scheibler, Bernd Becker |
| 2014 | Under-approximate flowpipes for non-linear continuous systems. | Xin Chen, Sriram Sankaranarayanan, Erika brahm |
| 2014 | Finding conflicting instances of quantified formulas in SMT. | Andrew Reynolds, Cesare Tinelli, Leonardo Mendona de Moura |
| 2014 | Reduction for compositional verification of multi-threaded programs. | Corneliu Popeea, Andrey Rybalchenko, Andreas Wilhelm |
| 2014 | The FMCAD 2014 graduate student forum. | Ruzica Piskac |
| 2014 | Turbo-charging Lemmas on demand with don't care reasoning. | Aina Niemetz, Mathias Preiner, Armin Biere |
| 2014 | ILP Modulo Data. | Panagiotis Manolios, Vasilis Papavasileiou, Mirek Riedewald |
| 2014 | Kuai: A model checker for software-defined networks. | Rupak Majumdar, Sai Deep Tetali, Zilong Wang |
| 2014 | Infinite-state backward exploration of Boolean broadcast programs. | Peizun Liu, Thomas Wahl |
| 2014 | Compiler verification for fun and profit. | Xavier Leroy |
| 2014 | A program transformation for faster goal-directed search. | Akash Lal, Shaz Qadeer |
| 2014 | Efficient symbolic execution for software testing. | Johannes Kinder |