15. TACAS 2009: York, UK (Part of ETAPS 2009)

Stefan Kowalewski, Anna Philippou (Eds.): 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. Lecture Notes in Computer Science 5505 Springer 2009, ISBN 978-3-642-00767-5

Model Checking I

Yann Thierry-Mieg, Denis Poitrenaud, Alexandre Hamez, Fabrice Kordon:
Hierarchical Set Decision Diagrams and Regular Models. 1-15
Seth Fogarty, Moshe Y. Vardi:
Büchi Complementation and Size-Change Termination. 16-30
Yu-Fang Chen, Azadeh Farzan, Edmund M. Clarke, Yih-Kuen Tsay, Bow-Yaw Wang:
Learning Minimal Separating DFA's for Compositional Verification. 31-45

Tools I

Mikhail I. Gofman, Ruiqi Luo, Ayla C. Solomon, Yingbin Zhang, Ping Yang, Scott D. Stoller:
RBAC-PAT: A Policy Analysis Tool for Role Based Access Control. 46-49
Elina Pacini Naumovich, Simona Bernardi, Marco Gribaudo:
ITPN-PerfBound: A Performance Bound Tool for Interval Time Petri Nets. 50-53
Didier Lime, Olivier H. Roux, Charlotte Seidner, Louis-Marie Traonouez:
Romeo: A Parametric Model-Checker for Petri Nets with Stopwatches. 54-57
Dietmar Berwanger, Krishnendu Chatterjee, Martin De Wulf, Laurent Doyen, Thomas A. Henzinger:
Alpaga: A Tool for Solving Parity Games with Imperfect Information. 58-61

Game-Theoretic Approaches

Adam Bakewell, Dan R. Ghica:
Compositional Predicate Abstraction from Game Semantics. 62-76
Hillel Kugler, Itai Segall:
Compositional Synthesis of Reactive Systems from Live Sequence Chart Specifications. 77-91
Wouter Kuijper, Jaco van de Pol:
Computing Weakest Strategies for Safety Games of Imperfect Information. 92-106

Verification of Concurrent Programs

Mohamed Faouzi Atig, Ahmed Bouajjani, Shaz Qadeer:
Context-Bounded Analysis for Concurrent Programs with Dynamic Creation of Threads. 107-123
Vineet Kahlon, Sriram Sankaranarayanan, Aarti Gupta:
Semantic Reduction of Thread Interleavings in Concurrent Programs. 124-138
Martin T. Vechev, Eran Yahav, Greta Yorsh:
Inferring Synchronization under Limited Observability. 139-154
Azadeh Farzan, P. Madhusudan:
The Complexity of Predicting Atomicity Violations. 155-169

Tools II

Niels H. M. Aan de Brugh, Viet Yen Nguyen, Theo C. Ruys:
MoonWalker: Verification of .NET Programs. 170-173
Robert Brummayer, Armin Biere:
Boolector: An Efficient SMT Solver for Bit-Vectors and Arrays. 174-177
Aditya V. Nori, Sriram K. Rajamani, SaiDeep Tetali, Aditya V. Thakur:
The YogiProject: Software Property Checking via Static Analysis and Testing. 178-181
Jérôme Leroux, Gérald Point:
TaPAS: The Talence Presburger Arithmetic Suite. 182-185

Model Checking II

Martin Wehrle, Sebastian Kupferschmid, Andreas Podelski:
Transition-Based Directed Model Checking. 186-200
Viet Yen Nguyen, Theo C. Ruys:
Memoised Garbage Collection for Software Model Checking. 201-214
Radu Mateescu, Anton Wijs:
Hierarchical Adaptive State Space Caching Based on Level Sampling. 215-229

Parametric Analysis

Simona Orzan, Wieger Wesselink, Tim A. C. Willemse:
Static Analysis Techniques for Parameterised Boolean Equation Systems. 230-245
Feng Chen, Grigore Rosu:
Parametric Trace Slicing and Monitoring. 246-261

Generative Approaches

Ashutosh Gupta, Rupak Majumdar, Andrey Rybalchenko:
From Tests to Proofs. 262-276
Dries Vanoverberghe, Nikolai Tillmann, Frank Piessens:
Test Input Generation for Programs with Pointers. 277-291
Claire Le Goues, Westley Weimer:
Specification Mining with Few False Positives. 292-306

Program Analysis

Nikolaj Bjørner, Nikolai Tillmann, Andrei Voronkov:
Path Feasibility Analysis for String-Manipulating Programs. 307-321
Fang Yu, Tevfik Bultan, Oscar H. Ibarra:
Symbolic String Verification: Combining String Analysis and Size Analysis. 322-336
Marius Bozga, Codruta Gîrlea, Radu Iosif:
Iterating Octagons. 337-351
Michael Emmi, Ranjit Jhala, Eddie Kohler, Rupak Majumdar:
Verifying Reference Counting Implementations. 352-367

Hybrid Systems

Erion Plaku, Lydia E. Kavraki, Moshe Y. Vardi:
Falsification of LTL Safety Properties in Hybrid Systems. 368-382
Christoph Scholl, Stefan Disch, Florian Pigorsch, Stefan Kupferschmid:
Computing Optimized Representations for Non-convex Polyhedra by Detection and Removal of Redundant Linear Constraints. 383-397

Decision Procedures and Theorem Proving

Panagiotis Manolios, Aaron Turon:
All-Termination(T). 398-412
Alexander Fuchs, Amit Goel, Jim Grundy, Sava Krstic, Cesare Tinelli:
Ground Interpolation for the Theory of Equality. 413-427
Enrica Nicolini, Christophe Ringeissen, Michaël Rusinowitch:
Satisfiability Procedures for Combination of Theories Sharing Integer Offsets. 428-442

Invited Contribution

Steven P. Miller:
Bridging the Gap Between Model-Based Development and Model Checking. 443-453