| 2009 | All-Termination(T). Panagiotis Manolios, Aaron Turon |
| 2009 | Alpaga: A Tool for Solving Parity Games with Imperfect Information. Dietmar Berwanger, Krishnendu Chatterjee, Martin De Wulf, Laurent Doyen, Thomas A. Henzinger |
| 2009 | Boolector: An Efficient SMT Solver for Bit-Vectors and Arrays. Robert Brummayer, Armin Biere |
| 2009 | Bridging the Gap Between Model-Based Development and Model Checking. Steven P. Miller |
| 2009 | Büchi Complementation and Size-Change Termination. Seth Fogarty, Moshe Y. Vardi |
| 2009 | Compositional Predicate Abstraction from Game Semantics. Adam Bakewell, Dan R. Ghica |
| 2009 | Compositional Synthesis of Reactive Systems from Live Sequence Chart Specifications. Hillel Kugler, Itai Segall |
| 2009 | Computing Optimized Representations for Non-convex Polyhedra by Detection and Removal of Redundant Linear Constraints. Christoph Scholl, Stefan Disch, Florian Pigorsch, Stefan Kupferschmid |
| 2009 | Computing Weakest Strategies for Safety Games of Imperfect Information. Wouter Kuijper, Jaco van de Pol |
| 2009 | Context-Bounded Analysis for Concurrent Programs with Dynamic Creation of Threads. Mohamed Faouzi Atig, Ahmed Bouajjani, Shaz Qadeer |
| 2009 | Falsification of LTL Safety Properties in Hybrid Systems. Erion Plaku, Lydia E. Kavraki, Moshe Y. Vardi |
| 2009 | From Tests to Proofs. Ashutosh Gupta, Rupak Majumdar, Andrey Rybalchenko |
| 2009 | Ground Interpolation for the Theory of Equality. Alexander Fuchs, Amit Goel, Jim Grundy, Sava Krstic, Cesare Tinelli |
| 2009 | Hierarchical Adaptive State Space Caching Based on Level Sampling. Radu Mateescu, Anton Wijs |
| 2009 | Hierarchical Set Decision Diagrams and Regular Models. Yann Thierry-Mieg, Denis Poitrenaud, Alexandre Hamez, Fabrice Kordon |
| 2009 | ITPN-PerfBound: A Performance Bound Tool for Interval Time Petri Nets. Elina Pacini Naumovich, Simona Bernardi, Marco Gribaudo |
| 2009 | Inferring Synchronization under Limited Observability. Martin T. Vechev, Eran Yahav, Greta Yorsh |
| 2009 | Iterating Octagons. Marius Bozga, Codruta Gîrlea, Radu Iosif |
| 2009 | Learning Minimal Separating DFA's for Compositional Verification. Yu-Fang Chen, Azadeh Farzan, Edmund M. Clarke, Yih-Kuen Tsay, Bow-Yaw Wang |
| 2009 | Memoised Garbage Collection for Software Model Checking. Viet Yen Nguyen, Theo C. Ruys |
| 2009 | MoonWalker: Verification of .NET Programs. Niels H. M. Aan de Brugh, Viet Yen Nguyen, Theo C. Ruys |
| 2009 | Parametric Trace Slicing and Monitoring. Feng Chen, Grigore Rosu |
| 2009 | Path Feasibility Analysis for String-Manipulating Programs. Nikolaj S. Bjørner, Nikolai Tillmann, Andrei Voronkov |
| 2009 | RBAC-PAT: A Policy Analysis Tool for Role Based Access Control. Mikhail I. Gofman, Ruiqi Luo, Ayla C. Solomon, Yingbin Zhang, Ping Yang, Scott D. Stoller |
| 2009 | Romeo: A Parametric Model-Checker for Petri Nets with Stopwatches. Didier Lime, Olivier H. Roux, Charlotte Seidner, Louis-Marie Traonouez |
| 2009 | Satisfiability Procedures for Combination of Theories Sharing Integer Offsets. Enrica Nicolini, Christophe Ringeissen, Michaël Rusinowitch |
| 2009 | Semantic Reduction of Thread Interleavings in Concurrent Programs. Vineet Kahlon, Sriram Sankaranarayanan, Aarti Gupta |
| 2009 | Specification Mining with Few False Positives. Claire Le Goues, Westley Weimer |
| 2009 | Static Analysis Techniques for Parameterised Boolean Equation Systems. Simona Orzan, Wieger Wesselink, Tim A. C. Willemse |
| 2009 | Symbolic String Verification: Combining String Analysis and Size Analysis. Fang Yu, Tevfik Bultan, Oscar H. Ibarra |
| 2009 | TaPAS: The Talence Presburger Arithmetic Suite. Jérôme Leroux, Gérald Point |
| 2009 | Test Input Generation for Programs with Pointers. Dries Vanoverberghe, Nikolai Tillmann, Frank Piessens |
| 2009 | The Complexity of Predicting Atomicity Violations. Azadeh Farzan, P. Madhusudan |
| 2009 | The YogiProject: Software Property Checking via Static Analysis and Testing. Aditya V. Nori, Sriram K. Rajamani, SaiDeep Tetali, Aditya V. Thakur |
| 2009 | Tools and Algorithms for the Construction and Analysis of Systems, 15th International Conference, TACAS 2009, Held as Part of the Joint European Conferences on Theory and Practice of Software, ETAPS 2009, York, UK, March 22-29, 2009. Proceedings Stefan Kowalewski, Anna Philippou |
| 2009 | Transition-Based Directed Model Checking. Martin Wehrle, Sebastian Kupferschmid, Andreas Podelski |
| 2009 | Verifying Reference Counting Implementations. Michael Emmi, Ranjit Jhala, Eddie Kohler, Rupak Majumdar |