| 2009 | 3-Valued Abstraction for (Bounded) Model Checking. Orna Grumberg |
| 2009 | A Data Symmetry Reduction Technique for Temporal-epistemic Logic. Mika Cohen, Mads Dam, Alessio Lomuscio, Hongyang Qu |
| 2009 | A Decompositional Proof Scheme for Automated Convergence Proofs of Stochastic Hybrid Systems. Jens Oehlerking, Oliver E. Theel |
| 2009 | A Framework for Compositional Verification of Multi-valued Systems via Abstraction-Refinement. Yael Meller, Orna Grumberg, Sharon Shoham |
| 2009 | Automated Analysis of Data-Dependent Programs with Dynamic Memory. Parosh Aziz Abdulla, Muhsin Atto, Jonathan Cederberg, Ran Ji |
| 2009 | Automated Technology for Verification and Analysis, 7th International Symposium, ATVA 2009, Macao, China, October 14-16, 2009. Proceedings Zhiming Liu, Anders P. Ravn |
| 2009 | CLAN: A Tool for Contract Analysis and Conflict Discovery. Stephen Fenech, Gordon J. Pace, Gerardo Schneider |
| 2009 | Dynamic Observers for the Synthesis of Opaque Systems. Franck Cassez, Jérémy Dubreil, Hervé Marchand |
| 2009 | Exploring the Scope for Partial Order Reduction. Jaco Geldenhuys, Henri Hansen, Antti Valmari |
| 2009 | Formal Verification for High-Assurance Behavioral Synthesis. Sandip Ray, Kecheng Hao, Yan Chen, Fei Xie, Jin Yang |
| 2009 | Incremental False Path Elimination for Static Software Analysis. Ansgar Fehnker, Ralf Huuck, Sean Seefried |
| 2009 | LTL Model Checking for Recursive Programs. Geng-Dian Huang, Lin-Zan Cai, Farn Wang |
| 2009 | LTL Model Checking of Time-Inhomogeneous Markov Chains. Taolue Chen, Tingting Han, Joost-Pieter Katoen, Alexandru Mereacre |
| 2009 | Local Search in Model Checking. A. W. Roscoe, Philip J. Armstrong, Pragyesh |
| 2009 | Logahedra: A New Weakly Relational Domain. Jacob M. Howe, Andy King |
| 2009 | Memory Usage Verification Using Hip/Sleek. Guanhua He, Shengchao Qin, Chenguang Luo, Wei-Ngan Chin |
| 2009 | On Detecting Regular Predicates in Distributed Systems. Hongtao Huang |
| 2009 | On Minimal Odd Rankings for Büchi Complementation. Hrishikesh Karmarkar, Supratik Chakraborty |
| 2009 | On-the-fly Emptiness Check of Transition-Based Streett Automata. Alexandre Duret-Lutz, Denis Poitrenaud, Jean-Michel Couvreur |
| 2009 | Quantitative Analysis under Fairness Constraints. Christel Baier, Marcus Größer, Frank Ciesinski |
| 2009 | Solving Parity Games in Practice. Oliver Friedmann, Martin Lange |
| 2009 | Specification Languages for Stutter-Invariant Regular Properties. Christian Dax, Felix Klaedtke, Stefan Leue |
| 2009 | State Space Reduction of Linear Processes Using Control Flow Reconstruction. Jaco van de Pol, Mark Timmer |
| 2009 | Statistical Model Checking Using Perfect Simulation. Diana El Rabih, Nihal Pekergin |
| 2009 | Symbolic CTL Model Checking of Asynchronous Systems Using Constrained Saturation. Yang Zhao, Gianfranco Ciardo |
| 2009 | Synthesis of Fault-Tolerant Distributed Systems. Rayna Dimitrova, Bernd Finkbeiner |
| 2009 | TAPAAL: Editor, Simulator and Verifier of Timed-Arc Petri Nets. Joakim Byg, Kenneth Yrke Jørgensen, Jirí Srba |
| 2009 | UnitCheck: Unit Testing and Model Checking Combined. Michal Kebrt, Ondrej Sery |
| 2009 | Verifying VLSI Circuits. Mark R. Greenstreet |