| 2007 | Formal Modeling and Verification of High-Availability Protocol for Network Security Appliances. | Moonzoo Kim |
| 2007 | Complete SAT-Based Model Checking for Context-Free Processes. | Geng-Dian Huang, Bow-Yaw Wang |
| 2007 | Recent Trend in Industry and Expectation to DA Research. | Atsushi Hasegawa |
| 2007 | Providing Evidence of Likely Being on Time: Counterexample Generation for CTMC Model Checking. | Tingting Han, Joost-Pieter Katoen |
| 2007 | Proving Termination of Tree Manipulating Programs. | Peter Habermehl, Radu Iosif, Adam Rogalewicz, Toms Vojnar |
| 2007 | 3-Valued Circuit SAT for STE with Automatic Refinement. | Orna Grumberg, Assaf Schuster, Avi Yadgar |
| 2007 | On the Efficient Computation of the Minimal Coverability Set for Petri Nets. | Gilles Geeraerts, Jean-Franois Raskin, Laurent Van Begin |
| 2007 | Computing Game Values for Crash Games. | Thomas Gawlitza, Helmut Seidl |
| 2007 | Quantifying the Discord: Order Discrepancies in Message Sequence Charts. | Edith Elkind, Blaise Genest, Doron A. Peled, Paola Spoletini |
| 2007 | Mechanizing the Powerset Construction for Restricted Classes of | Christian Dax, Jochen Eisinger, Felix Klaedtke |
| 2007 | Pruning State Spaces with Extended Beam Search. | Muhammad Torabi Dashti, Anton Wijs |
| 2007 | Exact State Set Representations in the Verification of Linear Hybrid Systems with Large Discrete State Space. | Werner Damm, Stefan Disch, Hardi Hungar, Swen Jacobs, Jun Pang, Florian Pigorsch, Christoph Scholl, Uwe Waldmann, Boris Wirtz |
| 2007 | Timed Control with Observation Based and Stuttering Invariant Strategies. | Franck Cassez, Alexandre David, Kim Guldstrand Larsen, Didier Lime, Jean-Franois Raskin |
| 2007 | Symbolic Fault Tree Analysis for Reactive Systems. | Marco Bozzano, Alessandro Cimatti, Francesco Tapparo |
| 2007 | A Compositional Semantics for Dynamic Fault Trees in Terms of Interactive Markov Chains. | Hichem Boudali, Pepijn Crouzen, Marille Stoelinga |
| 2007 | Efficient Approximate Verification of Promela Models Via Symmetry Markers. | Dragan Bosnacki, Alastair F. Donaldson, Michael Leuschel, Thierry Massart |
| 2007 | Model Checking Bounded Prioritized Time Petri Nets. | Bernard Berthomieu, Florent Peres, Franois Vernadat |
| 2007 | Mind the Shapes: Abstraction Refinement Via Topology Invariants. | Jrg Bauer, Tobe Toben, Bernd Westphal |
| 2007 | Automatic Merge-Point Detection for Sequential Equivalence Checking of System-Level and RTL Descriptions. | Bijan Alizadeh, Masahiro Fujita |
| 2006 | Analyzing Security Protocols in Hierarchical Networks. | Ye Zhang, Hanne Riis Nielson |
| 2006 | Effective Contraction of Timed STGs for Decomposition Based Timed Circuit Synthesis. | Tomohiro Yoneda, Chris J. Myers |
| 2006 | Analysis of Recursive Probabilistic Models. | Mihalis Yannakakis |
| 2006 | Verification Challenges and Opportunities in the New Era of Microprocessor Design. | Jin Yang |
| 2006 | Compositional Reasoning for Hardware/Software Co-verification. | Fei Xie, Guowu Yang, Xiaoyu Song |
| 2006 | Predicate Abstraction of Programs with Non-linear Computation. | Songtao Xia, Ben Di Vito, Csar A. Muoz |