default search action
15th TACAS 2009: York, UK (Part of ETAPS 2009)
- Stefan Kowalewski, Anna Philippou:
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 S. 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
manage site settings
To protect your privacy, all features that rely on external API calls from your browser are turned off by default. You need to opt-in for them to become active. All settings here will be stored as cookies with your web browser. For more information see our F.A.Q.