| 2011 | A theory of abstraction for arrays. Steven M. German |
| 2011 | Accelerating MUS extraction with recursive model rotation. Anton Belov, João Marques-Silva |
| 2011 | Algebraic approach to arithmetic design verification. Mohamed Abdul Basith, Tariq B. Ahmad, André Rossi, Maciej J. Ciesielski |
| 2011 | An incremental approach to model checking progress properties. Aaron R. Bradley, Fabio Somenzi, Zyad Hassan, Yan Zhang |
| 2011 | Approximate reachability with combined symbolic and ternary simulation. Michael L. Case, Jason Baumgartner, Hari Mony, Robert Kanzelman |
| 2011 | Automated error localization and correction for imperative programs. Robert Könighofer, Roderick Bloem |
| 2011 | Automated specification analysis using an interactive theorem prover. Harsh Raju Chamarthi, Panagiotis Manolios |
| 2011 | Desynchronization: design for verification. Sudarshan K. Srinivasan, Raj S. Katti |
| 2011 | Effective word-level interpolation for software verification. Alberto Griggio |
| 2011 | Efficient implementation of property directed reachability. Niklas Eén, Alan Mishchenko, Robert K. Brayton |
| 2011 | Formal analysis of fractional order systems in HOL. Umair Siddique, Osman Hasan |
| 2011 | Hardware model checking: status, challenges, and opportunities. Muralidhar Talupur |
| 2011 | Hunting deadlocks efficiently in microarchitectural models of communication fabrics. Freek Verbeek, Julien Schmaltz |
| 2011 | Hybrid verification of a hardware modular reduction engine. Jun Sawada, Peter Sandon, Viresh Paruthi, Jason Baumgartner, Michael L. Case, Hari Mony |
| 2011 | IC3: where monolithic and incremental meet. Fabio Somenzi, Aaron R. Bradley |
| 2011 | Incremental formal verification of hardware. Hana Chockler, Alexander Ivrii, Arie Matsliah, Shiri Moran, Ziv Nevo |
| 2011 | International Conference on Formal Methods in Computer-Aided Design, FMCAD '11, Austin, TX, USA, October 30 - November 02, 2011 Per Bjesse, Anna Slobodová |
| 2011 | Interpolants from Z3 proofs. Kenneth L. McMillan |
| 2011 | Learning conditional abstractions. Bryan A. Brady, Randal E. Bryant, Sanjit A. Seshia |
| 2011 | Optimal redundancy removal without fixedpoint computation. Michael L. Case, Jason Baumgartner, Hari Mony, Robert Kanzelman |
| 2011 | Parameterized verification of deadlock freedom in symmetric cache coherence protocols. Brad D. Bingham, Mark R. Greenstreet, Jesse D. Bingham |
| 2011 | Pervasive formal verification in control system design. Lee Pike |
| 2011 | Planning for end-to-end formal using simulation-based coverage: Prashant Aggarwal, Darrow Chu, Vijay Kadamby, Vigyan Singhal |
| 2011 | Post-silicon fault localisation using maximum satisfiability and backbones. Charlie Shucheng Zhu, Georg Weissenbacher, Sharad Malik |
| 2011 | Proving and explaining the unfeasibility of message sequence charts for hybrid systems. Alessandro Cimatti, Sergio Mover, Stefano Tonetta |
| 2011 | Pseudo-Boolean Solving by incremental translation to SAT. Panagiotis Manolios, Vasilis Papavasileiou |
| 2011 | Realtime regular expressions for analog and mixed-signal assertions. John Havlicek, Scott Little |
| 2011 | Scaling probabilistic timing verification of hardware using abstractions in design source code. Jayanand Asok Kumar, Lingyi Liu, Shobha Vasudevan |
| 2011 | Self-timing: a step beyond synchrony Ivan E. Sutherland |
| 2011 | Specification based testing with QuickCheck: John Hughes |
| 2011 | Static scheduling of latency insensitive designs with Lucy-n. Louis Mandel, Florence Plateau, Marc Pouzet |
| 2011 | The role of human creativity in mechanized verification: J Strother Moore |
| 2011 | Time-bounded analysis of real-time systems. Sagar Chaki, Arie Gurfinkel, Ofer Strichman |
| 2011 | Timing analysis of interrupt-driven programs under context bounds. Jonathan Kotker, Dorsa Sadigh, Sanjit A. Seshia |
| 2011 | Verifying concurrent programs: Aarti Gupta |