| 2009 | A compositional theory for post-reboot observational equivalence checking of hardware. Zurab Khasidashvili, Daher Kaiss, Doron Bustan |
| 2009 | A verified platform for a gate-level electronic control unit. Sergey Tverdyshev |
| 2009 | Assume-guarantee validation for STE properties within an SVA environment. Zurab Khasidashvili, Gavriel Gavrielov, Tom Melham |
| 2009 | Connecting pre-silicon and post-silicon verification. Sandip Ray, Warren A. Hunt Jr. |
| 2009 | Data mining based decomposition for assume-guarantee reasoning. He Zhu, Fei He, William N. N. Hung, Xiaoyu Song, Ming Gu |
| 2009 | Debugging formal specifications using simple counterstrategies. Robert Könighofer, Georg Hofferek, Roderick Bloem |
| 2009 | Decision diagrams for linear arithmetic. Sagar Chaki, Arie Gurfinkel, Ofer Strichman |
| 2009 | Efficient decision procedure for non-linear arithmetic constraints using CORDIC. Malay K. Ganai, Franjo Ivancic |
| 2009 | Enhanced verification by temporal decomposition. Michael L. Case, Hari Mony, Jason Baumgartner, Robert Kanzelman |
| 2009 | Finding heap-bounds for hardware synthesis. Byron Cook, Ashutosh Gupta, Stephen Magill, Andrey Rybalchenko, Jirí Simsa, Satnam Singh, Viktor Vafeiadis |
| 2009 | Formal verification of analog designs using MetiTarski. William Denman, Behzad Akbarpour, Sofiène Tahar, Mohamed H. Zaki, Lawrence C. Paulson |
| 2009 | Formal verification of correctness and performance of random priority-based arbiters. Krishnan Kailas, Viresh Paruthi, Brian Monwai |
| 2009 | Generalized, efficient array decision procedures. Leonardo Mendonça de Moura, Nikolaj S. Bjørner |
| 2009 | Hardware/software co-verification of cryptographic algorithms using Cryptol. Levent Erkök, Magnus Carlsson, Adam Wick |
| 2009 | Industrial strength refinement checking. Jesse D. Bingham, John Erickson, Gaurav Singh, Flemming Andersen |
| 2009 | Interpolation-sequence based model checking. Yakir Vizel, Orna Grumberg |
| 2009 | MCC: A runtime verification tool for MCAPI user applications. Subodh Sharma, Ganesh Gopalakrishnan, Eric Mercer, Jim Holt |
| 2009 | Mixed abstractions for floating-point arithmetic. Angelo Brillout, Daniel Kroening, Thomas Wahl |
| 2009 | Proceedings of 9th International Conference on Formal Methods in Computer-Aided Design, FMCAD 2009, 15-18 November 2009, Austin, Texas, USA |
| 2009 | Protocol verification using flows: An industrial experience. John W. O'Leary, Murali Talupur, Mark R. Tuttle |
| 2009 | Retiming and resynthesis with sweep are complete for sequential transformation. Hai Zhou |
| 2009 | SAT-based synthesis of clock gating functions using 3-valued abstraction. Eli Arbel, Oleg Rokhlenko, Karen Yorav |
| 2009 | Safety first: A two-stage algorithm for LTL games. Saqib Sohail, Fabio Somenzi |
| 2009 | Scalable conditional equivalence checking: An automated invariant-generation based approach. Jason Baumgartner, Hari Mony, Michael L. Case, Jun Sawada, Karen Yorav |
| 2009 | Scaling VLSI design debugging with interpolation. Brian Keng, Andreas G. Veneris |
| 2009 | Software model checking via large-block encoding. Dirk Beyer, Alessandro Cimatti, Alberto Griggio, M. Erkan Keremoglu, Roberto Sebastiani |
| 2009 | Structure-aware computation of predicate abstraction. Alessandro Cimatti, Jori Dubrovin, Tommi A. Junttila, Marco Roveri |
| 2009 | Synthesizing robust systems. Roderick Bloem, Karin Greimel, Thomas A. Henzinger, Barbara Jobstmann |
| 2009 | Towards a formally verified network-on-chip. Tom van den Broek, Julien Schmaltz |
| 2009 | Verification of recursive methods on tree-like data structures. Jyotirmoy V. Deshmukh, E. Allen Emerson |
| 2009 | Verifying equivalence of memories using a first order logic theorem prover. Zurab Khasidashvili, Mahmoud Kinanah, Andrei Voronkov |