| 2012 | Symbolic Trajectory Evaluation: The primary validation Vehicle for next generation Intel Processor Graphics FPU. | V. M. Achutha KiranKumar, Aarti Gupta, Rajnish Ghughal |
| 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 | A formal model of a large memory that supports efficient execution. | Warren A. Hunt Jr., Matt Kaufmann |
| 2012 | Preprocessing techniques for first-order clausification. | Krystof Hoder, Zurab Khasidashvili, Konstantin Korovin, Andrei Voronkov |
| 2012 | Algebra of concurrent design. | Tony Hoare |
| 2012 | Deciding floating-point logic with systematic abstraction. | Leopold Haller, Alberto Griggio, Martin Brain, Daniel Kroening |
| 2012 | Quantifier elimination by Dependency Sequents. | Eugene Goldberg, Panagiotis Manolios |
| 2012 | Complete and effective robustness checking by means of interpolation. | Stefan Frehse, Grschwin Fey, Eli Arbel, Karen Yorav, Rolf Drechsler |
| 2012 | Formal methods in cell Biology. | Jasmin Fisher |
| 2012 | Formal methods for aerospace applications. | Eric Feron |
| 2012 | Symbolically synthesizing small circuits. | Rdiger Ehlers, Robert Knighofer, Georg Hofferek |
| 2012 | A liveness checking algorithm that counts. | Koen Claessen, Niklas Srensson |
| 2012 | Verification of parametric system designs. | Alessandro Cimatti, Iman Narasamdya, Marco Roveri |
| 2012 | A quantifier-free SMT encoding of non-linear hybrid automata. | Alessandro Cimatti, Sergio Mover, Stefano Tonetta |
| 2012 | Application of SMT solvers to hybrid system verification. | Alessandro Cimatti |
| 2012 | Algorithms for software model checking: Predicate abstraction vs. Impact. | Dirk Beyer, Philipp Wendler |
| 2012 | IC3-guided abstraction. | Jason Baumgartner, Alexander Ivrii, Arie Matsliah, Hari Mony |
| 2012 | Multi-pushdown systems with budgets. | Parosh Aziz Abdulla, Mohamed Faouzi Atig, Othmane Rezine, Jari Stenman |
| 2011 | Post-silicon fault localisation using maximum satisfiability and backbones. | Charlie Shucheng Zhu, Georg Weissenbacher, Sharad Malik |
| 2011 | On Incremental Satisfiability and Bounded Model Checking. | Siert Wieringa |
| 2011 | Hunting deadlocks efficiently in microarchitectural models of communication fabrics. | Freek Verbeek, Julien Schmaltz |
| 2011 | Hardware model checking: status, challenges, and opportunities. | Muralidhar Talupur |
| 2011 | Self-timing: a step beyond synchrony | Ivan E. Sutherland |
| 2011 | Desynchronization: design for verification. | Sudarshan K. Srinivasan, Raj S. Katti |