14. TACAS 2008: Budapest, Hungary (Part of ETAPS 2008)

C. R. Ramakrishnan, Jakob Rehof (Eds.): Tools and Algorithms for the Construction and Analysis of Systems, 14th International Conference, TACAS 2008, Held as Part of the Joint European Conferences on Theory and Practice of Software, ETAPS 2008, Budapest, Hungary, March 29-April 6, 2008. Proceedings. Lecture Notes in Computer Science 4963 Springer 2008, ISBN 978-3-540-78799-0

Invited Talk

Sharad Malik:
Hardware Verification: Techniques, Methodology and Solutions. 1

Parameterized Systems

Azadeh Farzan, Yu-Fang Chen, Edmund M. Clarke, Yih-Kuen Tsay, Bow-Yaw Wang:
Extending Automated Compositional Verification to the Full Class of Omega-Regular Languages. 2-17
Mayank Saksena, Oskar Wibling, Bengt Jonsson:
Graph Grammar Modeling and Verification of Ad Hoc Routing Protocols. 18-32
Edmund M. Clarke, Muralidhar Talupur, Helmut Veith:
Proving Ptolemy Right: The Environment Abstraction Framework for Model Checking Concurrent Systems. 33-47

Model Checking - I

Jiri Barnat, Lubos Brim, Pavel Simecek, M. Weber:
Revisiting Resistance Speeds Up I/O-Efficient LTL Model Checking. 48-62
Martin De Wulf, Laurent Doyen, Nicolas Maquet, Jean-François Raskin:
Antichains: Alternative Algorithms for LTL Satisfiability and Model-Checking. 63-77
Adam Bakewell, Dan R. Ghica:
On-the-Fly Techniques for Game-Based Software Model Checking. 78-92
Parosh Aziz Abdulla, Ahmed Bouajjani, Lukás Holík, Lisa Kaati, Tomás Vojnar:
Computing Simulations over Tree Automata. 93-108

Applications

Eyad Alkassar, Norbert Schirmer, Artem Starostin:
Formal Pervasive Verification of a Paging Mechanism. 109-123
Gogul Balakrishnan, Thomas W. Reps:
Analyzing Stripped Device-Driver Executables. 124-140
Gal Katz, Doron Peled:
Model Checking-Based Genetic Programming with an Application to Mutual Exclusion. 141-156

Model Checking - II

Miguel E. Andrés, Peter van Rossum:
Conditional Probabilities over Probabilistic and Nondeterministic Systems. 157-172
Axel Legay, Andrzej S. Murawski, Joël Ouaknine, James Worrell:
On Automated Verification of Probabilistic Programs. 173-187
Sriram Sankaranarayanan, Thao Dang, Franjo Ivancic:
Symbolic Model Checking of Hybrid Systems Using Template Polyhedra. 188-202
Sebastian Kupferschmid, Jörg Hoffmann, Kim Guldstrand Larsen:
Fast Directed Model Checking Via Russian Doll Abstraction. 203-217

Static Analysis

Amir M. Ben-Amram, Michael Codish:
A SAT-Based Approach to Size Change Termination with Global Ranking Functions. 218-232
Hana Chockler, Orna Grumberg, Avi Yadgar:
Efficient Automatic STE Refinement Using Responsibility. 233-248
Laura Kovács:
Reasoning Algebraically About P-Solvable Loops. 249-264
Carsten Ihlemann, Swen Jacobs, Viorica Sofronie-Stokkermans:
On Local Reasoning in Verification. 265-281

Concurrent/Distributed Systems

Akash Lal, Tayssir Touili, Nicholas Kidd, Thomas W. Reps:
Interprocedural Analysis of Concurrent Programs Under a Context Bound. 282-298
Salvatore La Torre, P. Madhusudan, Gennaro Parlato:
Context-Bounded Analysis of Concurrent Queue Systems. 299-314
Dana Fisman, Orna Kupferman, Yoad Lustig:
On Verifying Fault Tolerance of Distributed Protocols. 315-331

Tools - I

Peter Csaba Ölveczky, José Meseguer:
The Real-Time Maude Tool. 332-336
Leonardo Mendonça de Moura, Nikolaj Bjørner:
Z3: An Efficient SMT Solver. 337-340
Gordon J. Pace, Gerardo Schneider:
Computation and Visualisation of Phase Portraits for Model Checking SPDIs. 341-345
Yih-Kuen Tsay, Yu-Fang Chen, Ming-Hsien Tsai, Wen-Chin Chan, Chi-Jian Luo:
GOAL Extended: Towards a Research Tool for Omega Automata and Temporal Logic. 346-350

Symbolic Execution

Peter Boonstoppel, Cristian Cadar, Dawson R. Engler:
RWset: Attacking Path Explosion in Constraint-Based Test Generation. 351-366
Saswat Anand, Patrice Godefroid, Nikolai Tillmann:
Demand-Driven Compositional Symbolic Execution. 367-381
Chao Wang, Zijiang Yang, Vineet Kahlon, Aarti Gupta:
Peephole Partial Order Reduction. 382-396

Abstraction, Interpolation

Alessandro Cimatti, Alberto Griggio, Roberto Sebastiani:
Efficient Interpolant Generation in Satisfiability Modulo Theories. 397-412
Kenneth L. McMillan:
Quantified Invariant Generation Using an Interpolating Saturation Prover. 413-427
Nicolas Caniart, Emmanuel Fleury, Jérôme Leroux, Marc Zeitoun:
Accelerating Interpolation-Based Model-Checking. 428-442
Bhargav S. Gulavani, Supratik Chakraborty, Aditya V. Nori, Sriram K. Rajamani:
Automatically Refining Abstract Interpretations. 443-458

Tools - II

Thomas Wahl, Nicolas Blanc, E. Allen Emerson:
SVISS: Symbolic Verification of Symmetric Systems. 459-462
Bernd Finkbeiner, Hans-Jörg Peter, Sven Schewe:
RESY: Requirement Synthesis for Compositional Model Checking. 463-466
Nicolas Blanc, Daniel Kroening, Natasha Sharygina:
Scoot: A Tool for the Analysis of SystemC Models. 467-470

Trust, Reputation

Guodong Li, Konrad Slind:
Trusted Source Translation of a Total Function Language. 471-485
Michal Moskal:
Rocket-Fast Proof Checking for SMT Solvers. 486-500
Ahmed Bouajjani, Javier Esparza, Stefan Schwoon, Dejvuth Suwimonteerabuth:
SDSIrep: A Reputation System Based on SDSI. 501-516