| 2007 | 3-Valued Circuit SAT for STE with Automatic Refinement. Orna Grumberg, Assaf Schuster, Avi Yadgar |
| 2007 | A Brief Introduction to Mercedes G. Merayo, Manuel Núñez, Ismael Rodríguez |
| 2007 | A Compositional Semantics for Dynamic Fault Trees in Terms of Interactive Markov Chains. Hichem Boudali, Pepijn Crouzen, Mariëlle Stoelinga |
| 2007 | A Formal Methodology to Test Complex Heterogeneous Systems. Ismael Rodríguez, Manuel Núñez |
| 2007 | A Generic Constructive Solution for Concurrent Games with Expressive Constraints on Strategies. Sophie Pinchinat |
| 2007 | A New Approach to Bounded Model Checking for Branching Time Logics. Rotem Oshman, Orna Grumberg |
| 2007 | Analog/Mixed-Signal Circuit Verification Using Models Generated from Simulation Traces. Scott Little, David Walter, Kevin R. Jones, Chris J. Myers |
| 2007 | Assertion-Based Proof Checking of Chang-Roberts Leader Election in PVS. Judi Romijn, Wieger Wesselink, Arjan J. Mooij |
| 2007 | Automated Technology for Verification and Analysis, 5th International Symposium, ATVA 2007, Tokyo, Japan, October 22-25, 2007, Proceedings Kedar S. Namjoshi, Tomohiro Yoneda, Teruo Higashino, Yoshio Okamura |
| 2007 | Automatic Merge-Point Detection for Sequential Equivalence Checking of System-Level and RTL Descriptions. Bijan Alizadeh, Masahiro Fujita |
| 2007 | Bounded Model Checking of Analog and Mixed-Signal Circuits Using an SMT Solver. David Walter, Scott Little, Chris J. Myers |
| 2007 | Bounded Synthesis. Sven Schewe, Bernd Finkbeiner |
| 2007 | Branching vs. Linear Time: Semantical Perspective. Sumit Nain, Moshe Y. Vardi |
| 2007 | Complete SAT-Based Model Checking for Context-Free Processes. Geng-Dian Huang, Bow-Yaw Wang |
| 2007 | Computing Game Values for Crash Games. Thomas Gawlitza, Helmut Seidl |
| 2007 | Continuous Petri Nets: Expressive Power and Decidability Issues. Laura Recalde, Serge Haddad, Manuel Silva Suárez |
| 2007 | Deciding Simulations on Probabilistic Automata. Lijun Zhang, Holger Hermanns |
| 2007 | Distributed Synthesis for Alternating-Time Logics. Sven Schewe, Bernd Finkbeiner |
| 2007 | Efficient Approximate Verification of Promela Models Via Symmetry Markers. Dragan Bosnacki, Alastair F. Donaldson, Michael Leuschel, Thierry Massart |
| 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 | Formal Modeling and Verification of High-Availability Protocol for Network Security Appliances. Moonzoo Kim |
| 2007 | Latticed Simulation Relations and Games. Orna Kupferman, Yoad Lustig |
| 2007 | Mechanizing the Powerset Construction for Restricted Classes of Christian Dax, Jochen Eisinger, Felix Klaedtke |
| 2007 | Mind the Shapes: Abstraction Refinement Via Topology Invariants. Jörg Bauer, Tobe Toben, Bernd Westphal |
| 2007 | Model Checking Bounded Prioritized Time Petri Nets. Bernard Berthomieu, Florent Peres, François Vernadat |
| 2007 | Model Checking Contracts - A Case Study. Gordon J. Pace, Cristian Prisacariu, Gerardo Schneider |
| 2007 | On the Efficient Computation of the Minimal Coverability Set for Petri Nets. Gilles Geeraerts, Jean-François Raskin, Laurent Van Begin |
| 2007 | On-the-Fly Model Checking of Fair Non-repudiation Protocols. Guoqiang Li, Mizuhito Ogawa |
| 2007 | Policies and Proofs for Code Auditing. Nathan Whitehead, Jordan Johnson, Martín Abadi |
| 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, Tomás Vojnar |
| 2007 | Pruning State Spaces with Extended Beam Search. Muhammad Torabi Dashti, Anton Wijs |
| 2007 | Quantifying the Discord: Order Discrepancies in Message Sequence Charts. Edith Elkind, Blaise Genest, Doron A. Peled, Paola Spoletini |
| 2007 | Recent Trend in Industry and Expectation to DA Research. Atsushi Hasegawa |
| 2007 | Symbolic Fault Tree Analysis for Reactive Systems. Marco Bozzano, Alessandro Cimatti, Francesco Tapparo |
| 2007 | Timed Control with Observation Based and Stuttering Invariant Strategies. Franck Cassez, Alexandre David, Kim Guldstrand Larsen, Didier Lime, Jean-François Raskin |
| 2007 | Timeout and Calendar Based Finite State Modeling and Verification of Real-Time Systems. Indranil Saha, Janardan Misra, Suman Roy |
| 2007 | Toward Property-Driven Abstraction for Heap Manipulating Programs. Kenneth L. McMillan |
| 2007 | Using Counterexample Analysis to Minimize the Number of Predicates for Predicate Abstraction. Thanyapat Sakunkonchak, Satoshi Komatsu, Masahiro Fujita |
| 2007 | Using Patterns and Composite Propositions to Automate the Generation of LTL Specifications. Salamah Salamah, Ann Q. Gates, Vladik Kreinovich, Steve Roach |
| 2007 | Verifying Heap-Manipulating Programs in an SMT Framework. Zvonimir Rakamaric, Roberto Bruttomesso, Alan J. Hu, Alessandro Cimatti |