| 2011 | IC3: where monolithic and incremental meet. | Fabio Somenzi, Aaron R. Bradley |
| 2011 | Formal analysis of fractional order systems in HOL. | Umair Siddique, Osman Hasan |
| 2011 | Hybrid verification of a hardware modular reduction engine. | Jun Sawada, Peter Sandon, Viresh Paruthi, Jason Baumgartner, Michael L. Case, Hari Mony |
| 2011 | Pervasive formal verification in control system design. | Lee Pike |
| 2011 | The role of human creativity in mechanized verification: | J Strother Moore |
| 2011 | Interpolants from Z3 proofs. | Kenneth L. McMillan |
| 2011 | Pseudo-Boolean Solving by incremental translation to SAT. | Panagiotis Manolios, Vasilis Papavasileiou |
| 2011 | Static scheduling of latency insensitive designs with Lucy-n. | Louis Mandel, Florence Plateau, Marc Pouzet |
| 2011 | Enhancing ABC for stabilization verification of SystemVerilog/VHDL models. | Jiang Long, Sayak Ray, Baruch Sterin, Alan Mishchenko, Robert K. Brayton |
| 2011 | Scaling probabilistic timing verification of hardware using abstractions in design source code. | Jayanand Asok Kumar, Lingyi Liu, Shobha Vasudevan |
| 2011 | Timing analysis of interrupt-driven programs under context bounds. | Jonathan Kotker, Dorsa Sadigh, Sanjit A. Seshia |
| 2011 | Automated error localization and correction for imperative programs. | Robert Knighofer, Roderick Bloem |
| 2011 | Specification based testing with QuickCheck: | John Hughes |
| 2011 | Realtime regular expressions for analog and mixed-signal assertions. | John Havlicek, Scott Little |
| 2011 | A Study of Sweeping Algorithms in the Context of Model Checking. | Zyad Hassan, Yan Zhang, Fabio Somenzi |
| 2011 | metaSMT: Focus on Your Application not on Solver Integration. | Finn Haedicke, Stefan Frehse, Grschwin Fey, Daniel Groe, Rolf Drechsler |
| 2011 | Verifying concurrent programs: | Aarti Gupta |
| 2011 | Effective word-level interpolation for software verification. | Alberto Griggio |
| 2011 | A theory of abstraction for arrays. | Steven M. German |
| 2011 | Data Structure Choices for On-the-Fly Model Checking of Real-Time Systems. | Peter Fontana, Rance Cleaveland |
| 2011 | Efficient implementation of property directed reachability. | Niklas En, Alan Mishchenko, Robert K. Brayton |
| 2011 | Proving and explaining the unfeasibility of message sequence charts for hybrid systems. | Alessandro Cimatti, Sergio Mover, Stefano Tonetta |
| 2011 | Incremental formal verification of hardware. | Hana Chockler, Alexander Ivrii, Arie Matsliah, Shiri Moran, Ziv Nevo |
| 2011 | Automated specification analysis using an interactive theorem prover. | Harsh Raju Chamarthi, Panagiotis Manolios |
| 2011 | Time-bounded analysis of real-time systems. | Sagar Chaki, Arie Gurfinkel, Ofer Strichman |