| 2009 | Interpolation-sequence based model checking. | Yakir Vizel, Orna Grumberg |
| 2009 | A verified platform for a gate-level electronic control unit. | Sergey Tverdyshev |
| 2009 | Safety first: A two-stage algorithm for LTL games. | Saqib Sohail, Fabio Somenzi |
| 2009 | MCC: A runtime verification tool for MCAPI user applications. | Subodh Sharma, Ganesh Gopalakrishnan, Eric Mercer, Jim Holt |
| 2009 | Connecting pre-silicon and post-silicon verification. | Sandip Ray, Warren A. Hunt Jr. |
| 2009 | Protocol verification using flows: An industrial experience. | John W. O'Leary, Murali Talupur, Mark R. Tuttle |
| 2009 | Generalized, efficient array decision procedures. | Leonardo Mendona de Moura, Nikolaj S. Bjrner |
| 2009 | Debugging formal specifications using simple counterstrategies. | Robert Knighofer, Georg Hofferek, Roderick Bloem |
| 2009 | Verifying equivalence of memories using a first order logic theorem prover. | Zurab Khasidashvili, Mahmoud Kinanah, Andrei Voronkov |
| 2009 | A compositional theory for post-reboot observational equivalence checking of hardware. | Zurab Khasidashvili, Daher Kaiss, Doron Bustan |
| 2009 | Assume-guarantee validation for STE properties within an SVA environment. | Zurab Khasidashvili, Gavriel Gavrielov, Tom Melham |
| 2009 | Scaling VLSI design debugging with interpolation. | Brian Keng, Andreas G. Veneris |
| 2009 | Formal verification of correctness and performance of random priority-based arbiters. | Krishnan Kailas, Viresh Paruthi, Brian Monwai |
| 2009 | Efficient decision procedure for non-linear arithmetic constraints using CORDIC. | Malay K. Ganai, Franjo Ivancic |
| 2009 | Hardware/software co-verification of cryptographic algorithms using Cryptol. | Levent Erkk, Magnus Carlsson, Adam Wick |
| 2009 | Verification of recursive methods on tree-like data structures. | Jyotirmoy V. Deshmukh, E. Allen Emerson |
| 2009 | Formal verification of analog designs using MetiTarski. | William Denman, Behzad Akbarpour, Sofine Tahar, Mohamed H. Zaki, Lawrence C. Paulson |
| 2009 | Finding heap-bounds for hardware synthesis. | Byron Cook, Ashutosh Gupta, Stephen Magill, Andrey Rybalchenko, Jir Simsa, Satnam Singh, Viktor Vafeiadis |
| 2009 | Structure-aware computation of predicate abstraction. | Alessandro Cimatti, Jori Dubrovin, Tommi A. Junttila, Marco Roveri |
| 2009 | Decision diagrams for linear arithmetic. | Sagar Chaki, Arie Gurfinkel, Ofer Strichman |
| 2009 | Enhanced verification by temporal decomposition. | Michael L. Case, Hari Mony, Jason Baumgartner, Robert Kanzelman |
| 2009 | Towards a formally verified network-on-chip. | Tom van den Broek, Julien Schmaltz |
| 2009 | Mixed abstractions for floating-point arithmetic. | Angelo Brillout, Daniel Kroening, Thomas Wahl |
| 2009 | Synthesizing robust systems. | Roderick Bloem, Karin Greimel, Thomas A. Henzinger, Barbara Jobstmann |
| 2009 | Industrial strength refinement checking. | Jesse D. Bingham, John Erickson, Gaurav Singh, Flemming Andersen |