| 2010 | Formal verification of an ASIC ethernet switch block. | B. A. Krishna, Anamaya Sullerey, Alok Jain |
| 2010 | Precise static analysis of untrusted driver binaries. | Johannes Kinder, Helmut Veith |
| 2010 | Verifying VIA Nano microprocessor components. | Warren A. Hunt Jr. |
| 2010 | Synthesis for regular specifications over unbounded domains. | Jad Hamza, Barbara Jobstmann, Viktor Kuncak |
| 2010 | Relieving capacity limits on FPGA-based SAT-solvers. | Leopold Haller, Satnam Singh |
| 2010 | Dimensions in program synthesis. | Sumit Gulwani |
| 2010 | Integrating ICP and LRA solvers for deciding nonlinear real arithmetic problems. | Sicun Gao, Malay K. Ganai, Franjo Ivancic, Aarti Gupta, Sriram Sankaranarayanan, Edmund M. Clarke |
| 2010 | Propelling SAT and SAT-based BMC using careset. | Malay K. Ganai |
| 2010 | Applying SMT in symbolic execution of microcode. | Anders Franzn, Alessandro Cimatti, Alexander Nadel, Roberto Sebastiani, Jonathan Shalev |
| 2010 | Encoding industrial hardware verification problems into effectively propositional logic. | Moshe Emmer, Zurab Khasidashvili, Konstantin Korovin, Andrei Voronkov |
| 2010 | A single-instance incremental SAT formulation of proof- and counterexample-based abstraction. | Niklas En, Alan Mishchenko, Nina Amla |
| 2010 | Verifying SystemC: A software model checking approach. | Alessandro Cimatti, Andrea Micheli, Iman Narasamdya, Marco Roveri |
| 2010 | PINCETTE - Validating changes and upgrades in networked software. | Hana Chockler |
| 2010 | A framework for incremental modelling and verification of on-chip protocols. | Peter Bhm |
| 2010 | Predicate abstraction with adjustable-block encoding. | Dirk Beyer, M. Erkan Keremoglu, Philipp Wendler |
| 2010 | Incremental component-based construction and verification using invariants. | Saddek Bensalem, Marius Bozga, Axel Legay, Thanh-Hung Nguyen, Joseph Sifakis, Rongjie Yan |
| 2010 | Coping with Moore's Law (and more): Supporting arrays in state-of-the-art model checkers. | Jason Baumgartner, Michael L. Case, Hari Mony |
| 2010 | SLAM2: Static driver verification with under 4% false alarms. | Thomas Ball, Ella Bounimova, Rahul Kumar, Vladimir Levin |
| 2010 | Scalable and precise program analysis at NEC. | Gogul Balakrishnan, Malay K. Ganai, Aarti Gupta, Franjo Ivancic, Vineet Kahlon, Weihong Li, Naoto Maeda, Nadia Papakonstantinou, Sriram Sankaranarayanan, Nishant Sinha, Chao Wang |
| 2010 | Formal verification of arbiters using property strengthening and underapproximations. | Gadiel Auerbach, Fady Copty, Viresh Paruthi |
| 2010 | Modular specification and verification of interprocess communication. | Eyad Alkassar, Ernie Cohen, Mark A. Hillebrand, Hristo Pentchev |
| 2010 | Verifying shadow page table algorithms. | Eyad Alkassar, Ernie Cohen, Mark A. Hillebrand, Mikhail Kovalev, Wolfgang J. Paul |
| 2010 | SAT-based semiformal verification of hardware. | Sabih Agbaria, Dan Carmi, Orly Cohen, Dmitry Korchemny, Michael Lifshits, Alexander Nadel |
| 2009 | Data mining based decomposition for assume-guarantee reasoning. | He Zhu, Fei He, William N. N. Hung, Xiaoyu Song, Ming Gu |
| 2009 | Retiming and resynthesis with sweep are complete for sequential transformation. | Hai Zhou |