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

Sharad Malik (auth.), C. R. Ramakrishnan, Jakob Rehof (eds.)3540787992, 9783540787990

This book constitutes the refereed proceedings of the 14th International Conference on Tools and Algorithms for the Construction and Analysis of Systems, TACAS 2008, held in Budapest, Hungary, in March/April 2008 as part of ETAPS 2008, the European Joint Conferences on Theory and Practice of Software.

The 31 revised full research papers and 7 revised tool demonstration papers presented together with the abstract of an invited paper were carefully reviewed and selected from a total of 140 submissions. The papers are organized in topical sections on parameterized systems, model checking, applications, static analysis, concurrent/distributed systems, symbolic execution, abstraction, interpolation, trust, and reputation.

---

Table of contents :
Front Matter….Pages –
Hardware Verification: Techniques, Methodology and Solutions….Pages 1-1
Extending Automated Compositional Verification to the Full Class of Omega-Regular Languages….Pages 2-17
Graph Grammar Modeling and Verification of Ad Hoc Routing Protocols….Pages 18-32
Proving Ptolemy Right: The Environment Abstraction Framework for Model Checking Concurrent Systems….Pages 33-47
Revisiting Resistance Speeds Up I/O-Efficient LTL Model Checking….Pages 48-62
Antichains: Alternative Algorithms for LTL Satisfiability and Model-Checking….Pages 63-77
On-the-Fly Techniques for Game-Based Software Model Checking….Pages 78-92
Computing Simulations over Tree Automata….Pages 93-108
Formal Pervasive Verification of a Paging Mechanism….Pages 109-123
Analyzing Stripped Device-Driver Executables….Pages 124-140
Model Checking-Based Genetic Programming with an Application to Mutual Exclusion….Pages 141-156
Conditional Probabilities over Probabilistic and Nondeterministic Systems….Pages 157-172
On Automated Verification of Probabilistic Programs….Pages 173-187
Symbolic Model Checking of Hybrid Systems Using Template Polyhedra….Pages 188-202
Fast Directed Model Checking Via Russian Doll Abstraction….Pages 203-217
A SAT-Based Approach to Size Change Termination with Global Ranking Functions….Pages 218-232
Efficient Automatic STE Refinement Using Responsibility….Pages 233-248
Reasoning Algebraically About P-Solvable Loops….Pages 249-264
On Local Reasoning in Verification….Pages 265-281
Interprocedural Analysis of Concurrent Programs Under a Context Bound….Pages 282-298
Context-Bounded Analysis of Concurrent Queue Systems….Pages 299-314
On Verifying Fault Tolerance of Distributed Protocols….Pages 315-331
The Real-Time Maude Tool….Pages 332-336
Z3: An Efficient SMT Solver….Pages 337-340
Computation and Visualisation of Phase Portraits for Model Checking SPDIs….Pages 341-345
GOAL Extended: Towards a Research Tool for Omega Automata and Temporal Logic….Pages 346-350
RWset: Attacking Path Explosion in Constraint-Based Test Generation….Pages 351-366
Demand-Driven Compositional Symbolic Execution….Pages 367-381
Peephole Partial Order Reduction….Pages 382-396
Efficient Interpolant Generation in Satisfiability Modulo Theories….Pages 397-412
Quantified Invariant Generation Using an Interpolating Saturation Prover….Pages 413-427
Accelerating Interpolation-Based Model-Checking….Pages 428-442
Automatically Refining Abstract Interpretations….Pages 443-458
SVISS : Symbolic Verification of Symmetric Systems….Pages 459-462
RESY: Requirement Synthesis for Compositional Model Checking….Pages 463-466
Scoot : A Tool for the Analysis of SystemC Models….Pages 467-470
Trusted Source Translation of a Total Function Language….Pages 471-485
Rocket-Fast Proof Checking for SMT Solvers….Pages 486-500
SDSIrep: A Reputation System Based on SDSI….Pages 501-516
Back Matter….Pages –