Tools and Algorithms for the Construction and Analysis of Systems: 13th International Conference, TACAS 2007, Held as Part of the Joint European Conferences on Theory and Practice of Software, ETAPS 2007 Braga, Portugal, March 24 – April 1, 2007. Proceedings

Rance Cleaveland (auth.), Orna Grumberg, Michael Huth (eds.)3540712089, 9783540712084

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

The 45 revised full research papers and nine revised tool demonstration papers presented together with one invited paper were carefully reviewed and selected from a total of 204 submissions. The papers are organized in topical sections on software verification, probabilistic model checking and markov chains, static analysis, markov chains and real-time systems, timed automata and duration calculus, assume-guarantee reasoning, biological systems, abstraction refinement, message sequence charts, automata-based model checking, specification languages, security, software and hardware verification, decision procedures and theorem provers, model checking, as well as infinite-state systems.

---

Table of contents :
Front Matter….Pages –
THERE AND BACK AGAIN: Lessons Learned on the Way to the Market….Pages 1-1
Verifying Object-Oriented Software: Lessons and Challenges….Pages 2-2
Shape Analysis by Graph Decomposition….Pages 3-18
A Reachability Predicate for Analyzing Low-Level Software….Pages 19-33
Generating Representation Invariants of Structurally Complex Data….Pages 34-49
Multi-objective Model Checking of Markov Decision Processes….Pages 50-65
PReMo : An Analyzer for P robabilistic Re cursive Mo dels….Pages 66-71
Counterexamples in Probabilistic Model Checking….Pages 72-86
Bisimulation Minimisation Mostly Speeds Up Probabilistic Model Checking….Pages 87-101
Causal Dataflow Analysis for Concurrent Programs….Pages 102-116
Type-Dependence Analysis and Program Transformation for Symbolic Execution….Pages 117-133
JPF–SE: A Symbolic Execution Extension to Java PathFinder….Pages 134-138
A Symbolic Algorithm for Optimal Markov Chain Lumping….Pages 139-154
Flow Faster: Efficient Decision Algorithms for Probabilistic Simulations….Pages 155-169
Model Checking Probabilistic Timed Automata with One or Two Clocks….Pages 170-184
Adaptor Synthesis for Real-Time Components….Pages 185-200
Deciding an Interval Logic with Accumulated Durations….Pages 201-215
From Time Petri Nets to Timed Automata: An Untimed Approach….Pages 216-230
Complexity in Simplicity: Flexible Agent-Based State Space Exploration….Pages 231-245
On Sampling Abstraction of Continuous Time Logic with Durations….Pages 246-260
Assume-Guarantee Synthesis….Pages 261-275
Optimized L*-Based Assume-Guarantee Reasoning….Pages 276-291
Refining Interface Alphabets for Compositional Verification….Pages 292-307
MAVEN: Modular Aspect Verification….Pages 308-322
Model Checking Liveness Properties of Genetic Regulatory Networks….Pages 323-338
Checking Pedigree Consistency with PCS….Pages 339-342
“Don’t Care” Modeling: A Logical Framework for Developing Predictive System Models….Pages 343-357
Deciding Bit-Vector Arithmetic with Abstraction….Pages 358-372
Abstraction Refinement of Linear Programs with Arrays….Pages 373-388
Property-Driven Partitioning for Abstraction Refinement….Pages 389-404
Combining Abstraction Refinement and SAT-Based Model Checking….Pages 405-419
Detecting Races in Ensembles of Message Sequence Charts….Pages 420-434
Replaying Play In and Play Out: Synthesis of Design Models from Scenarios by Learning….Pages 435-450
Improved Algorithms for the Automata-Based Approach to Model-Checking….Pages 451-465
GOAL: A Graphical Tool for Manipulating Büchi Automata and Temporal Formulae….Pages 466-471
Faster Algorithms for Finitary Games….Pages 472-484
Planned and Traversable Play-Out: A Flexible Method for Executing Scenario-Based Programs , ….Pages 485-499
motor :The modest Tool Environment….Pages 500-504
Syntactic Optimizations for PSL Verification….Pages 505-518
The Heterogeneous Tool Set, Hets ….Pages 519-522
Searching for Shapes in Cryptographic Protocols….Pages 523-537
Automatic Analysis of the Security of XOR-Based Key Management Schemes….Pages 538-552
State of the Union: Type Inference Via Craig Interpolation….Pages 553-567
Hoare Logic for Realistically Modelled Machine Code….Pages 568-582
VCEGAR : Verilog CounterExample Guided Abstraction Refinement….Pages 583-586
Alloy Analyzer+PVS in the Analysis and Verification of Alloy Specifications….Pages 587-601
Combined Satisfiability Modulo Parametric Theories….Pages 602-617
A Gröbner Basis Approach to CNF-Formulae Preprocessing….Pages 618-631
Kodkod: A Relational Model Finder….Pages 632-647
Bounded Reachability Checking of Asynchronous Systems Using Decision Diagrams….Pages 648-663
Model Checking on Trees with Path Equivalences….Pages 664-678
Uppaal/DMC – Abstraction-Based Heuristics for Directed Model Checking….Pages 679-682
Distributed Analysis with μ CRL: A Compendium of Case Studies….Pages 683-689
A Generic Framework for Reasoning About Dynamic Networks of Infinite-State Processes….Pages 690-705
Unfolding Concurrent Well-Structured Transition Systems….Pages 706-720
Regular Model Checking Without Transducers (On Efficient Verification of Parameterized Systems)….Pages 721-736
Back Matter….Pages –