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 Proceedin

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. Coverage includes software verification, probabilistic model checking and markov chains, automata-based model checking, security, software and hardware verification, decision procedures and theorem provers, as well as infinite-state systems. front-matter fulltext fulltext_001 fulltext_002 Introduction Overview A Full Heap Abstraction for Lists Abstracting List Segments A Graph Decomposition Abstraction for Lists The Abstract Domain of Shape Subgraphs Abstraction by Graph Decomposition Concretization by Composition of Shape Subgraphs Developing Efficient Abstract Transformersfor the Graph Decomposition Abstraction The Most Precise Abstract Transformer Sound and Efficient Transformers An Incremental Transformer Prototype Implementation and Empirical Results Related Work fulltext_003 Introduction Related Work Motivation Example Operational Semantics of C Reachability and Pointer Arithmetic Annotation Language Implementation Proving Verification Conditions Evaluation Conclusions and Future Work fulltext_004 Introduction Example Deryaft Program Heap as an Edge-Labeled Graph Core and Derived Fields Properties of Interest Algorithm Illustration: Binary Tree Representation of Heaps Experiments Discussion Related Work Conclusions fulltext_005 Introduction Basics and Background Multi-objective Reachability Qualitative Multi-objective Model Checking Quantitative Multi-objective Model Checking Concluding Remarks fulltext_006 Introduction Experimental Results Future Work fulltext_007 Introduction Preliminaries Strongest Evidences and Counterexamples From a DTMC to a Weighted Digraph Finding Strongest Evidences Finding Smallest Counterexamples Lower Bounds on Probabilities Conclusion fulltext_008 Introduction Preliminaries Bisimulation Experiments Discrete Time Continuous Time Rewards Concluding Remarks fulltext_009 Introduction Preliminaries The Control Net of a Program Causal Concurrent Dataflow Framework Meet over All Traces Solution Formulation of Specific Problems in the CCD Framework Solving the Distributive CCD Problem Experiments Conclusions fulltext_010 Introduction Type-Dependence Analysis Building the TDG Performing CFL-Reachability on the TDG Program Transformation Source and Target Languages Transformation Empirical Studies Results and Discussion Related Work Conclusion Type-Dependence Analysis for Fields and Entities of Array-Types Transformation Rules fulltext_011 Introduction JPF--SE Overview Conclusion and Future Work fulltext_012 Introduction Background Notation, CTMC, and Lumpability Explicit State-Level Lumping Algorithm Multi-Terminal Binary Decision Diagram Transforming the Algorithm from Explicit to Symbolic Symbolic Representation of Partitions Replacing Explicit L by Symbolic $\prt$ Symbolic Procedures: SymComputeKeys and SymSplit Improving the Symbolic Algorithm Running Time T1: Computing \textsc{GetClass}$(\bddset(\prt),j+1)$ from \textsc{GetClass}$(\bddset(\prt),j)$ T2: Fast Detection and Skipping of Stable Classes Performance Study Implementation and Example Models Results Conclusion and Future Work fulltext_013 Introduction Preliminaries Algorithms for Deciding Strong Simulation Algorithms for Deciding Weak Simulation Conclusions fulltext_014 Introduction Probabilistic Timed Automata Probabilistic Timed Temporal Logic Model Checking One Clock Probabilistic Timed Automata Model Checking $\sptctlq$ on 1C-PTA Model Checking \ptctlz\ on 1C-PTA Model Checking Two Clocks Probabilistic Timed Automata fulltext_015 Introduction Background Context Architectural Model Overview The Interface Specification and Its Translation Adaptor Synthesis Unification PN Generation Controlled Coverability Graph Synthesis (CCG) Case Study: A Remote Medical Care System Conclusion fulltext_016 Introduction Duration Calculus Syntax Semantics Decidability of the Satisfiability Problem Priced Timed Automata Encoding of DCub Formulae by MPTA The Construction Correspondence Between Interpretations of Formulae and Runs of Corresponding MPTA Conclusion fulltext_017 Introduction Preliminaries From Time Petri Nets to Timed Automata MCTA of a TPN Comparing the MCG, ESCG, and zbMCG Approaches Improving the Effectiveness of the MCG Approach Reducing the Number of Unreachable Locations Trading Clocks for Locations and Speed Dealing with Unboundedness The GreatSPN2TA Tool Conclusions fulltext_018 Introduction Agent Framework Frustration Search Framework Instantiation Applications Conclusions and Future Work fulltext_019 Introduction A Variety of Duration Calculi Duration Calculi PLDC to WSIDL DC to PLDC WSIDL to DDC Validity Checking DC Experimental Results fulltext_020 Introduction Co-synthesis Game Algorithms for Co-synthesis Abstraction-Based Co-synthesis fulltext_021 Introduction Preliminaries The L* Algorithm AG Reasoning with L* Optimized L*-Based AG Reasoning Reusing Counterexamples Selective Membership Queries Minimizing the Assumption Alphabet Experiments fulltext_022 Introduction Background Assume-Guarantee Reasoning and Small Interface Alphabets Learning for Assume-Guarantee Reasoning Learning with Alphabet Refinement Algorithm Extension to $n$ Modules Properties of Learning with Refinement Experiments Related Work Conclusions and Future Work fulltext_023 Introduction Aspect-Oriented Programming Modular Aspectual Verification Results Definitions LTL Tableaux Aspects Weaving Weakly Invasive Aspects Algorithm MAVEN Related Work Conclusion fulltext_024 Introduction Preliminaries A Motivating Example: Tuning a Transcriptional Cascade Model Checking Genetic Regulatory Networks with Parameter Uncertainty PMA Models and LTL Specifications Embedding Transition Systems and Discrete Abstractions Model Checking Uncertain PMA Systems Transient Regions and Liveness Checking Time-Diverging Executions and Transient Regions Ruling Out Time-Converging Executions Transient Region Computation for PMA Systems Analysis of the Tuned Transcriptional Cascade Discussion fulltext_025 Introduction Pedigree Consistency Tool Description Results Conclusions fulltext_026 Introduction Example Problem Formulation Solutions Implementing the Basic Algorithm Improved Algorithm Biological Application Related Work fulltext_027 Introduction Preliminaries The Decision Procedure Overview Generating an Over-Approximating Abstraction Another Step of Abstraction Experimental Results Conclusion fulltext_028 Introduction Model Checking Linear Programs with Arrays Linear Programs and Linear Programs with Arrays Abstracting Linear Programs with Arrays into Linear Programs Checking Trace Feasibility Refinement Implementation and Experimental Results Conclusions fulltext_029 Introduction Background Symbolic Model Checking Abstraction Counterexample-Guided Abstraction Refinement Property-Driven Partitioning for Abstraction Refinement Combining PDP with Abstraction Property-Driven Partitioned Refinement Experimental Results Conclusions fulltext_030 Introduction Overview of the Algorithms Preliminaries DPLL-Style SAT Solvers SAT-Based Bounded Model Checking Proof-Based Abstraction Refinement Interpolation-Based Model Checking Combining Interpolation and Abstraction Refinement Using Proof-Based Abstraction in Interpolation Incremental Interpolation Experimental Analysis Conclusions fulltext_031 Introduction Preliminaries Race Detection in Multiple MSCs Number of MSCs Needed for Closedness MSCs with Coregions Hardness Results Conclusions fulltext_032 Introduction Message Sequence Charts Message-Passing Automata An Extension of Angluin's Algorithm The Basic Algorithm Learning Objects Represented by Subclasses of Regular Word Languages Learning Message-Passing Automata Regular MSC Languages and Product MSC Languages Learning $\forall$ -Bounded Message-Passing Automata Learning $\exists$ -Bounded Message-Passing Automata Learning $\forall$ -Bounded Safe Product Message-Passing Automata Learning $\forall$ -Bounded Product Message-Passing Automata Tool Description and Future Work fulltext_033 Introduction Büchi Automata and Classical Algorithms Simulation Pre-orders and Fixed Points Emptiness of ABW Universality of NBW Implementation and Practical Evaluation Language Inclusion for Büchi Automata Conclusion fulltext_034 Introduction Main Functions Use Cases Concluding Remarks fulltext_035 Introduction Definitions Parity Games Parity Conditions Algorithms Streett Games Streett Conditions Conclusion and Developments fulltext_036 Introduction LSCs Planning Main Approaches to Planning Planning Graphs IPP Translating Play-Out into Planning Initial Conditions The Goal Actions More Formally Extending IPP Forced Mutexes Finding Many Plans Results Traversable Play-Out Cut-Queries Performance Future Work Related Work fulltext_037 The modest Approach motor motor and Möbius Status and Availability fulltext_038 Introduction The Property Specification Language PSL From PSL to NBA: Previous Approaches Syntactic Optimizations for PSL Experimental Evaluation Conclusions and Future Work fulltext_039 Introduction Logics in Hets Heterogeneous Specification Proof Management Conclusion fulltext_040 Introduction Shapes: The Core Idea The Yahalom Protocol Definition Search Steps Yahalom: Shapes for the Responder Search Strategy Implementing CPSA fulltext_041 Introduction Analysing the IBM Recommendations Using CL-AtSe CCA Key Management Commands Modelling the API Analysing IBM's Recommendations Theoretical Results for XOR-Based Key-Management APIs Definitions Well-Formed Protocols Proof of Decidability Implementation and Results Representation of XOR Terms The Implemented Procedure Results Conclusion fulltext_042 Introduction Language and Type System Syntax and Semantics Predicated Refinements of Subtype Hierarchies Type Checking Type Inference Via Interpolation Generating Predicate Constraints Solving Predicate Constraints Implementation and Experiences Related Work fulltext_043 Introduction Approach Basic Specifications Heterogeneous Specifications Positioning Functions Excessive Separation Hoare Triple for Machine Code State Representation Execution Predicate Code Assertion Hoare Triple Example: Composition Example: Procedures and Procedural Recursion Formalisation and Specialisation Summary fulltext_044 Introduction Word-Level Circuit Verification with VCEGAR Conclusion fulltext_045 Introduction Alloy and the Alloy Analyzer A Novel Complete Calculus for Alloy Point-Dense Omega Closure Fork Algebras A Complete Calculus for Alloy Comparing the Source and Target Formalisms The Dynamite Tool Customizations Made on EMACS Customizations Made on PVS A Proof Scenario A Case Study: A Formal Model of Addressing for Interoperating Networks Discussion fulltext_046 Introduction Syntax and Semantics of Higher Order Logic Syntax of HOL Types and Terms Semantics of Types Semantics of Terms Parametric Structures Relational Semantics Fully Parametric Structures HOL Theories and Satisfiability Nelson-Oppen Cooperation The Combined Solver The Combination Theorem Conclusion and Future Work fulltext_047 Introduction Contemporary Preprocessing Approaches Gröbner Bases for CNF-Transformation Methodology Preliminaries Gröbner Bases Transformation Process Partitioning Generating the Gröbner Basis Monomial Ordering Transforming Polynomials into CNF Clauses Results Categories of SAT-Instances Combining SAT Preprocessors Interpreting the Results Conclusion fulltext_048 Introduction Related Work Model Finding Basics Abstract Syntax Semantics Analysis Symmetry Detection Sparse-Matrix Translation to Boolean Logic Sharing Detection with Compact Boolean Circuits Results fulltext_049 Introduction Background Bounded Reachability Checking Using Decision Diagrams Experimental Results Discussion and Related Work Conclusions and Future Work fulltext_050 Introduction Trees with Path Equivalences Branching-Time Logics on Equivalence Graphs Model Checking Related Work Conclusion fulltext_051 Introduction Heuristics Monotonicity Abstraction Automata-Theoretic Abstraction Results Outlook fulltext_052 Introduction Applications of Distributed Analysis Evaluation and Conclusion Appendix fulltext_053 Introduction Colored Markings Logic Preliminaries Syntax and Semantics of CML Syntactical Forms and Fragments Satisfiability Problem Constrained Petri Nets Modeling Power of CPN Computing post and pre Images Applications in Verification Pre-post Condition Reasoning Bounded Reachability Analysis Checking Invariance Properties Conclusion fulltext_054 Introduction Labeled Transition Systems and Event Structures Labeled Transition Systems Labeled Event Structures Truncation for Well-Structured Transition Systems Synchronized Product of Well-Structured Transition Systems Finite Property-Preserving Truncation of Well-Structured LES Compositional Unfoldings of Concurrent Systems Unfolding Counters Unfolding Labeled Transition Systems Unfolding Synchronized Products of Components Experimental Results fulltext_055 Introduction Preliminaries Transition System Approximation Generic Scheme Algorithm Extensions Experimental Results Conclusion and Future Work back-matter