| 2004 | Formal verification in Intel CPU design. | John O'Leary |
| 2004 | Synchronous extensions to operation centric hardware description languages. | Grace Nordin, James C. Hoe |
| 2004 | Bluespec System Verilog: efficient, correct RTL from high level specifications. | Rishiyur S. Nikhil |
| 2004 | Hierarchical reconfiguration of dataflow models. | Stephen Neuendorffer, Edward A. Lee |
| 2004 | Static driver verifier, a formal verification tool for Windows device drivers. | Vladimir Levin |
| 2004 | Classes and subclasses in actor-oriented design. | Edward A. Lee, Stephen Neuendorffer |
| 2004 | Formal verification as a technology transfer problem. | Robert P. Kurshan |
| 2004 | Formal verification of pipelined processors with precise exceptions. | Krishnamani Kalyanasundaram, R. K. Shyamasundar |
| 2004 | Using invariants to optimize formal specifications before code synthesis. | Ralph D. Jeffords, Elizabeth I. Leonard |
| 2004 | Verification of SpecC using predicate abstraction. | Himanshu Jain, Daniel Kroening, Edmund M. Clarke |
| 2004 | Formal methods and software reliability. | Gerard J. Holzmann |
| 2004 | Checkers for SystemC designs. | Daniel Groe, Rolf Drechsler |
| 2004 | Static priority scheduling of event triggered real time embedded systems. | Cagkan Erbas, Selin C. Erbas, Andy D. Pimentel |
| 2004 | The battle of accountable voting systems. | David L. Dill |
| 2004 | Designing a reorder buffer in Bluespec. | Nirav Dave |
| 2004 | Automated, compositional and iterative deadlock detection. | Sagar Chaki, Edmund M. Clarke, Jol Ouaknine, Natasha Sharygina |
| 2004 | System modeling and verification with UCLID. | Randal E. Bryant |
| 2004 | Efficient code synthesis from synchronous dataflow graphs. | Dag Bjrklund |
| 2004 | Is formal being squeezed out of functional verification? | Brian Bailey |
| 2004 | PROBMELA: a modeling language for communicating probabilistic processes. | Christel Baier, Frank Ciesinski, Marcus Grer |
| 2004 | A framework for heterogeneous formal modeling and compositional verification of avionics systems. | Yamine At Ameur, Remi Delmas, Virginie Wiels |
| 2003 | A Generalised Approach to Supervisor Synthesis. | Roberto Ziller, Klaus Schneider |
| 2003 | LOTOS Code Generation for Model Checking of STBus Based SoC: the STBus interconnect. | Pierre Wodey, Geoffrey Camarroque, Fabrice Baray, Richard Hersemeule, Jean-Philippe Cousin |
| 2003 | Analyzing Concurrency in Computational Networks. | Sander Stuijk, Twan Basten |
| 2003 | Formal Verification of an Intel XScale Processor Model with Scoreboarding, Specialized Execution Pipelines, and Impress Data-Memory Exceptions. | Sudarshan K. Srinivasan, Miroslav N. Velev |