| 2013 | On the concept of variable roles and its use in software analysis. | Yulia Demyanova, Helmut Veith, Florian Zuleger |
| 2013 | Computing prime implicants. | David Dharbe, Pascal Fontaine, Daniel Le Berre, Bertrand Mazure |
| 2013 | Invariants for finite instances and beyond. | Sylvain Conchon, Amit Goel, Sava Krstic, Alain Mebsout, Fatiha Zadi |
| 2013 | Using process modeling and analysis techniques to reduce errors in healthcare. | Lori A. Clarke |
| 2013 | A circuit approach to LTL model checking. | Koen Claessen, Niklas En, Baruch Sterin |
| 2013 | Parameter synthesis with IC3. | Alessandro Cimatti, Alberto Griggio, Sergio Mover, Stefano Tonetta |
| 2013 | Distributed synthesis for LTL fragments. | Krishnendu Chatterjee, Thomas A. Henzinger, Jan Otop, Andreas Pavlogiannis |
| 2013 | Verifying periodic programs with priority inheritance locks. | Sagar Chaki, Arie Gurfinkel, Ofer Strichman |
| 2013 | Efficient modular SAT solving for IC3. | Sam Bayless, Celina G. Val, Thomas Ball, Holger H. Hoos, Alan J. Hu |
| 2013 | Static verification based signoff - A key enabler for managing verification complexity in the modern soc. | Pranav Ashar |
| 2013 | Counter-strategy guided refinement of GR(1) temporal logic specifications. | Rajeev Alur, Salar Moarref, Ufuk Topcu |
| 2013 | Syntax-guided synthesis. | Rajeev Alur, Rastislav Bodk, Garvit Juniwal, Milo M. K. Martin, Mukund Raghothaman, Sanjit A. Seshia, Rishabh Singh, Armando Solar-Lezama, Emina Torlak, Abhishek Udupa |
| 2013 | Generalized counterexamples to liveness properties. | Gadi Aleksandrowicz, Jason Baumgartner, Alexander Ivrii, Ziv Nevo |
| 2012 | Piecewise linear modeling of nonlinear devices for formal verification of analog circuits. | Yan Zhang, Sriram Sankaranarayanan, Fabio Somenzi |
| 2012 | Forward and backward: Bounded model checking of linear hybrid automata from two directions. | Yang Yang, Lei Bu, Xuandong Li |
| 2012 | Oscillator verification with probability one. | Chao Yan, Mark R. Greenstreet |
| 2012 | Enhanced reachability analysis via automated dynamic netlist-based hint generation. | Jiazhao Xu, Mark Williams, Hari Mony, Jason Baumgartner |
| 2012 | Lazy abstraction and SAT-based reachability in hardware model checking. | Yakir Vizel, Orna Grumberg, Sharon Shoham |
| 2012 | Formal for everyone - Challenges in achievable multicore design and verification. | Daryl Stewart |
| 2012 | Verification with small and short worlds. | Rohit Sinha, Cynthia Sturton, Petros Maniatis, Sanjit A. Seshia, David A. Wagner |
| 2012 | Efficient predictive analysis for detecting nondeterminism in multi-threaded programs. | Arnab Sinha, Sharad Malik, Aarti Gupta |
| 2012 | Incremental upgrade checking by means of interpolation-based function summaries. | Ondrej Sery, Grigory Fedyukovich, Natasha Sharygina |
| 2012 | Answer Set Programming. | Torsten Schaub |
| 2012 | Decompilation into logic - Improved. | Magnus O. Myreen, Michael J. C. Gordon, Konrad Slind |
| 2012 | Formal verification of error correcting circuits using computational algebraic geometry. | Alexey Lvov, Luis Alfonso Lastras-Montao, Viresh Paruthi, Robert Shadowen, Ali El-Zein |