| 2005 | Formal verification of SystemC by automatic hardware/software partitioning. | Daniel Kroening, Natasha Sharygina |
| 2005 | Thunderstriking constraints with JUPITER. | Christos Kloukinas |
| 2005 | Verification of low-level crypto-protocol implementations using automated theorem proving. | Jan Jrjens |
| 2005 | Extended abstract: formal verification of architectural patterns in support of dependable distributed systems. | Ralph D. Jeffords, Ramesh Bharadwaj |
| 2005 | PyPBS design and methodologies. | Greg Hoover, Forrest Brewer |
| 2005 | A synchronous language at work: the story of Lustre. | Nicolas Halbwachs |
| 2005 | System design extreme makeover. | Daniel Gajski |
| 2005 | Extended abstract: a formal design approach from software oriented UML descriptions to hardware oriented RTL. | Masahiro Fujita |
| 2005 | Deterministic receptive processes are Kahn processes. | Stephen A. Edwards, Olivier Tardieu |
| 2005 | Automatic synthesis of cache-coherence protocol processors using Bluespec. | Nirav Dave, Man Cheuk Ng, Arvind |
| 2005 | Panel on design for verification. | Tevfik Bultan, Constance L. Heitmeyer, John O'Leary |
| 2005 | Automotive software and systems engineering (Panel). | Manfred Broy |
| 2005 | On the use of a high-level fault model to analyze logical consequence of properties. | Stefano Brait, Franco Fummi, Graziano Pravadelli |
| 2005 | Extended abstract: on the property-based verification in SoC design flow founded on transaction level modeling. | Nicola Bombieri, Andrea Fedeli, Franco Fummi |
| 2005 | Refinemant verification of fair transition systems can contribute to PLTL model checking. | Franoise Bellegarde, Samir Chouali, Jacques Julliand |
| 2005 | A formal approach to system level design: metamodels and unified design environments. | Felice Balarin, Roberto Passerone, Alessandro Pinto, Alberto L. Sangiovanni-Vincentelli |
| 2005 | Making PVS do what you want. | Myla Archer |
| 2004 | Curing schizophrenia by program rewriting in Esterel. | Olivier Tardieu, Robert de Simone |
| 2004 | Compositional verification for secure loading of smart card applets. | Christoph Sprenger, Dilian Gurov, Marieke Huisman |
| 2004 | Check and simulate: a case for incorporating model checking in network simulation. | Ahmed Sobeih, Mahesh Viswanathan, Jennifer C. Hou |
| 2004 | Panel: given that hardware verification has been an uphill battle, what is the future of software verification? | Sandeep K. Shukla, Tevfik Bultan, Constance L. Heitmeyer |
| 2004 | Bounded model checking of infinite state systems: exploiting the automata hierarchy. | Tobias Schle, Klaus Schneider |
| 2004 | The ephemeral history register: flexible scheduling for rule-based designs. | Daniel L. Rosenband |
| 2004 | Designers want proofs - but show me the money. | Carl Pixley, D. Meyers, S. McMaster, A. Chittor |
| 2004 | The BUSpec platform for automated generation of verification aids for standard bus protocols. | Bhaskar Pal, Ansuman Banerjee, Pallab Dasgupta, P. P. Chakrabarti |