| 2014 | A program transformation for faster goal-directed search. Akash Lal, Shaz Qadeer |
| 2014 | A tour of CVC4: How it works, and how to use it. Morgan Deters, Andrew Reynolds, Tim King, Clark W. Barrett, Cesare Tinelli |
| 2014 | Challenges in bit-precise reasoning. Armin Biere |
| 2014 | Challenging problems in industrial formal verification. Ziyad Hanna |
| 2014 | Compiler verification for fun and profit. Xavier Leroy |
| 2014 | Computer-aided verification technology for biology. Thomas A. Henzinger |
| 2014 | DRUPing for interpolates. Arie Gurfinkel, Yakir Vizel |
| 2014 | Disproving termination with overapproximation. Byron Cook, Carsten Fuhs, Kaustubh Nimkar, Peter W. O'Hearn |
| 2014 | Efficient extraction of Skolem functions from QRAT proofs. Marijn Heule, Martina Seidl, Armin Biere |
| 2014 | Efficient symbolic execution for software testing. Johannes Kinder |
| 2014 | Efficient verification of periodic programs using sequential consistency and snapshots. Sagar Chaki, Arie Gurfinkel, Nishant Sinha |
| 2014 | Faster temporal reasoning for infinite-state programs. Byron Cook, Heidy Khlaaf, Nir Piterman |
| 2014 | Finding conflicting instances of quantified formulas in SMT. Andrew Reynolds, Cesare Tinelli, Leonardo Mendonça de Moura |
| 2014 | Formal Methods in Computer-Aided Design, FMCAD 2014, Lausanne, Switzerland, October 21-24, 2014 |
| 2014 | ILP Modulo Data. Panagiotis Manolios, Vasilis Papavasileiou, Mirek Riedewald |
| 2014 | Infinite-state backward exploration of Boolean broadcast programs. Peizun Liu, Thomas Wahl |
| 2014 | Interpolation with Guided Refinement: Revisiting incrementality in SAT-based unbounded model checking. Gianpiero Cabodi, Marco Palena, Paolo Pasini |
| 2014 | Kuai: A model checker for software-defined networks. Rupak Majumdar, Sai Deep Tetali, Zilong Wang |
| 2014 | Leveraging linear and mixed integer programming for SMT. Tim King, Clark W. Barrett, Cesare Tinelli |
| 2014 | On interpolants and variable assignments. Pavel Jancík, Jan Kofron, Simone Fulvio Rollini, Natasha Sharygina |
| 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 Röblitz, Brigitte Leeners, Tillmann H. C. Kruger, Marcel Egli, Fabian Ille |
| 2014 | Post-silicon timing diagnosis made simple using formal technology. Daher Kaiss, Jonathan Kalechstain |
| 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 | Reduction for compositional verification of multi-threaded programs. Corneliu Popeea, Andrey Rybalchenko, Andreas Wilhelm |
| 2014 | Response property checking via distributed state space exploration. Brad D. Bingham, Mark R. Greenstreet |
| 2014 | SAT-based methods for circuit synthesis. Roderick Bloem, Uwe Egly, Patrick Klampfl, Robert Könighofer, Florian Lonsing |
| 2014 | Simulation and formal verification of x86 machine-code programs that make system calls. Shilpi Goel, Warren A. Hunt Jr., Matt Kaufmann, Soumava Ghosh |
| 2014 | Small inductive safe invariants. Alexander Ivrii, Arie Gurfinkel, Anton Belov |
| 2014 | Synthesis of synchronization using uninterpreted functions. Roderick Bloem, Georg Hofferek, Bettina Könighofer, Robert Könighofer, Simon Ausserlechner, Raphael Spork |
| 2014 | Template-based circuit understanding. Adrià Gascón, Pramod Subramanyan, Bruno Dutertre, Ashish Tiwari, Dejan Jovanovic, Sharad Malik |
| 2014 | The FMCAD 2014 graduate student forum. Ruzica Piskac |
| 2014 | Towards Pareto-optimal parameter synthesis for monotonic cost functions. Benjamin Bittner, Marco Bozzano, Alessandro Cimatti, Marco Gario, Alberto Griggio |
| 2014 | Turbo-charging Lemmas on demand with don't care reasoning. Aina Niemetz, Mathias Preiner, Armin Biere |
| 2014 | Under-approximate flowpipes for non-linear continuous systems. Xin Chen, Sriram Sankaranarayanan, Erika Ábrahám |
| 2014 | Using interval constraint propagation for pseudo-Boolean constraint solving. Karsten Scheibler, Bernd Becker |