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 BibTeX

Model Checking I

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

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
Electronic Edition (link) BibTeX
Elina Pacini Naumovich, Simona Bernardi, Marco Gribaudo:
ITPN-PerfBound: A Performance Bound Tool for Interval Time Petri Nets. 50-53
Electronic Edition (link) BibTeX
Didier Lime, Olivier H. Roux, Charlotte Seidner, Louis-Marie Traonouez:
Romeo: A Parametric Model-Checker for Petri Nets with Stopwatches. 54-57
Electronic Edition (link) BibTeX
Dietmar Berwanger, Krishnendu Chatterjee, Martin De Wulf, Laurent Doyen, Thomas A. Henzinger:
Alpaga: A Tool for Solving Parity Games with Imperfect Information. 58-61
Electronic Edition (link) BibTeX

Game-Theoretic Approaches

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

Verification of Concurrent Programs

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

Tools II

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

Model Checking II

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

Parametric Analysis

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

Generative Approaches

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

Program Analysis

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

Hybrid Systems

Erion Plaku, Lydia E. Kavraki, Moshe Y. Vardi:
Falsification of LTL Safety Properties in Hybrid Systems. 368-382
Electronic Edition (link) BibTeX
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
Electronic Edition (link) BibTeX

Decision Procedures and Theorem Proving

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

Invited Contribution

Steven P. Miller:
Bridging the Gap Between Model-Based Development and Model Checking. 443-453
Electronic Edition (link) BibTeX