| 2012 | A formal model of a large memory that supports efficient execution. Warren A. Hunt Jr., Matt Kaufmann |
| 2012 | A liveness checking algorithm that counts. Koen Claessen, Niklas Sörensson |
| 2012 | A quantifier-free SMT encoding of non-linear hybrid automata. Alessandro Cimatti, Sergio Mover, Stefano Tonetta |
| 2012 | Algebra of concurrent design. Tony Hoare |
| 2012 | Algorithms for software model checking: Predicate abstraction vs. Impact. Dirk Beyer, Philipp Wendler |
| 2012 | Answer Set Programming. Torsten Schaub |
| 2012 | Application of SMT solvers to hybrid system verification. Alessandro Cimatti |
| 2012 | Automated debugging of missing input constraints in a formal verification environment. Brian Keng, Andreas G. Veneris |
| 2012 | Automatic lock insertion in concurrent programs. Vineet Kahlon |
| 2012 | Complete and effective robustness checking by means of interpolation. Stefan Frehse, Görschwin Fey, Eli Arbel, Karen Yorav, Rolf Drechsler |
| 2012 | Deciding floating-point logic with systematic abstraction. Leopold Haller, Alberto Griggio, Martin Brain, Daniel Kroening |
| 2012 | Decompilation into logic - Improved. Magnus O. Myreen, Michael J. C. Gordon, Konrad Slind |
| 2012 | Efficient predictive analysis for detecting nondeterminism in multi-threaded programs. Arnab Sinha, Sharad Malik, Aarti Gupta |
| 2012 | Enhanced reachability analysis via automated dynamic netlist-based hint generation. Jiazhao Xu, Mark Williams, Hari Mony, Jason Baumgartner |
| 2012 | Formal Methods in Computer-Aided Design, FMCAD 2012, Cambridge, UK, October 22-25, 2012 Gianpiero Cabodi, Satnam Singh |
| 2012 | Formal for everyone - Challenges in achievable multicore design and verification. Daryl Stewart |
| 2012 | Formal methods for aerospace applications. Eric Feron |
| 2012 | Formal methods in cell Biology. Jasmin Fisher |
| 2012 | Formal verification of error correcting circuits using computational algebraic geometry. Alexey Lvov, Luis Alfonso Lastras-Montaño, Viresh Paruthi, Robert Shadowen, Ali El-Zein |
| 2012 | Forward and backward: Bounded model checking of linear hybrid automata from two directions. Yang Yang, Lei Bu, Xuandong Li |
| 2012 | IC3-guided abstraction. Jason Baumgartner, Alexander Ivrii, Arie Matsliah, Hari Mony |
| 2012 | Incremental upgrade checking by means of interpolation-based function summaries. Ondrej Sery, Grigory Fedyukovich, Natasha Sharygina |
| 2012 | Lazy abstraction and SAT-based reachability in hardware model checking. Yakir Vizel, Orna Grumberg, Sharon Shoham |
| 2012 | Multi-pushdown systems with budgets. Parosh Aziz Abdulla, Mohamed Faouzi Atig, Othmane Rezine, Jari Stenman |
| 2012 | Oscillator verification with probability one. Chao Yan, Mark R. Greenstreet |
| 2012 | Piecewise linear modeling of nonlinear devices for formal verification of analog circuits. Yan Zhang, Sriram Sankaranarayanan, Fabio Somenzi |
| 2012 | Preprocessing techniques for first-order clausification. Krystof Hoder, Zurab Khasidashvili, Konstantin Korovin, Andrei Voronkov |
| 2012 | Quantifier elimination by Dependency Sequents. Eugene Goldberg, Panagiotis Manolios |
| 2012 | Symbolic Trajectory Evaluation: The primary validation Vehicle for next generation Intel® Processor Graphics FPU. V. M. Achutha KiranKumar, Aarti Gupta, Rajnish Ghughal |
| 2012 | Symbolically synthesizing small circuits. Rüdiger Ehlers, Robert Könighofer, Georg Hofferek |
| 2012 | Verification of parametric system designs. Alessandro Cimatti, Iman Narasamdya, Marco Roveri |
| 2012 | Verification with small and short worlds. Rohit Sinha, Cynthia Sturton, Petros Maniatis, Sanjit A. Seshia, David A. Wagner |