Ebook: Tools and Algorithms for the Construction and Analysis of Systems: 16th International Conference, TACAS 2010, Held as Part of the Joint European Conferences on Theory and Practice of Software, ETAPS 2010, Paphos, Cyprus, March 20-28, 2010. Proceedings

This book constitutes the refereed proceedings of the 16th International Conference on Tools and Algorithms for the Construction and Analysis of Systems, TACAS 2010, held in Paphos, Cyprus, in March 2010, as part of ETAPS 2010, the European Joint Conferences on Theory and Practice of Software. The 35 papers presented were carefully reviewed and selected from 134 submissions. The topics covered are probabilistic systems and optimization, decision procedures, tools, automata theory, liveness, software verification, real time and information flow, and testing.

---

This book constitutes the refereed proceedings of the 16th International Conference on Tools and Algorithms for the Construction and Analysis of Systems, TACAS 2010, held in Paphos, Cyprus, in March 2010, as part of ETAPS 2010, the European Joint Conferences on Theory and Practice of Software. The 35 papers presented were carefully reviewed and selected from 134 submissions. The topics covered are probabilistic systems and optimization, decision procedures, tools, automata theory, liveness, software verification, real time and information flow, and testing. Table of Contents Cover Tools and Algorithms for the Construction and Analysis of Systems, 16th International Conference, TACAS 2010, Held as Part of the Joint European Conferences on Theory and Practice of Software, ETAPS 2010, Paphos, Cyprus, March 20-28, 2010. Proceedings ISBN-10 3642120016 ISBN-13 9783642120015 Foreword Preface Organization Table of Contents Invited Talks Probabilistic Systems and Optimization Decision Procedures Tools I Automata Theory Liveness Tools I I Software Veri.cation Tools III Real Time and Information Flow Testing Embedded Systems Design - Scientific Challenges and Work Directions Antichain Algorithms for Finite Automata 1 Introduction 2 Preliminaries 3 Antichain Fixpoint Algorithms 4 Applications References Assume-Guarantee Verification for Probabilistic Systems 1 Introduction 2 Background 3 Compositional Verification for PAs 4 Quantitative Assume-Guarantee Queries 5 Implementation and Case Studies 6 Conclusions References Simple O(m log n) Time Markov Chain Lumping 1 Introduction 2 The Lumping Problem 3 Background Data Structures and Algorithms 4 The Lumping Algorithm 5 Correctness 6 Performance 7 Testing and Measurements 8 Conclusions References Model Checking Interactive Markov Chains 1 Introduction 2 Preliminaries 3 Interval Bounded Reachability Probability 4 Model Checking the Continuous Stochastic Logic 5 Experimental Results 6 Related Work and Conclusions References Approximating the Pareto Front of Multi-criteria Optimization Problems 1 Introduction 2 Preliminary Defnition 3 Knee Points 4 The Algorithm 5 Experimentation 6 Conclusions References An Alternative to SAT-Based Approaches for Bit-Vectors 1 Introduction 2 Background 3 Encoding BV into Non-linear Arithmetic 4 Dedicated N=M -Propagators for Is/C Domains 5 New Domain: BitList BL 6 Experiments 7 Related Work 8 Conclusion References Satisfability Modulo the Theory of Costs: Foundations and Applications 1 Motivations and Goals 2 Background on SMT and SMT Solving 3 Satisfability Modulo the Theory of Costs 4 Optimization Modulo Theories via SMT(T.C) 5 PseudoBoolean and MAX-SAT/SMT as SMT(C)/SMT(T.C) 6 Empirical Evaluation 7 Related Work 8 Conclusions and Future Work References Optimal Tableau Algorithms for Coalgebraic Logics 1 Introduction 2 Preliminaries and Notation 3 Tableaux and Games for Global Consequence 4 Soundness and Completeness 5 Global Caching 6 Conclusions References Blocked Clause Elimination 1 Introduction 2 Boolean Circuits and CNF SAT 3 Resolution and CNF-Level Simpli cation 4 Blocked Clause Elimination 5 Effectiveness of Blocked Clause Elimination 6 Bene ts of Combining BCE and VE 7 Implementation 8 Experiments 9 Conclusions References BOOM: Taking Boolean Program Model Checking One Step Further 1 Introduction 2 Concurrent Boolean Program Analysis with BOOM 3 Results 4 Related Work and Conclusion References The OpenSMT Solver 1 Introduction 2 Tool Architecture 3 Other Features References STRANGER: An Automata-Based String Analysis Tool for PHP 1 Introduction 2 Tool Description 3 Experiments and Conclusions References When Simulation Meets Antichains (On Checking Language Inclusion of Nondeterministic Finite (Tree) Automata) 1 Introduction 2 Preliminaries 3 Universality of NFAs 4 Correctness of the Optimized Universality Checking 5 The Language Inclusion Problem 6 Tree Automata Preliminaries 7 Universality and Language Inclusion of Tree Automata 8 Experimental Results 9 Conclusion References On Weak Modal Compatibility, Refinemet, and the MIO Workbench 1 Introduction 2 Modal (I/O) Transition Systems 3 Weak Modal Compatibility 4 Overview of Refinemet and Compatibility Notions 5 TheMIOWorkbench 6 Conclusion References Rational Synthesis 1 Introduction 2 Preliminaries 3 Rational Synthesis 4 Solution in the Boolean Setting 5 Solution in the Multi-valued Setting 6 Discussion References Efficient Büchi Universality Checking 1 Introduction 2 Preliminaries 3 Subsumption in the Ramsey-Based Algorithm 4 Empirical Analysis 5 Conclusion References Automated Termination Analysis for Programs with Second-Order Recursion 1 Introduction 2 Size Estimation for Polymorphic Data Types 3 Estimation Proofs 4 Automated Termination Proofs 5 Related Work and Experimental Results 6 Conclusion References Ranking Function Synthesis for Bit-Vector Relations 1 Introduction 2 Termination of Bit-Vector Programs 3 Ranking Functions for Bit-Vector Programs 4 Experiments 5 Related Work 6 Conclusion References Fairness for Dynamic Control 1 Introduction 2 Definiions 3 The Scheduler S88 and Dynamic Control 4 The Scheduler S10 5 The Monitor M88 6 Infiniary Fairness 7 Conclusion References JTorX: A Tool for On-Line Model-Driven Test Derivation and Execution 1 Introduction 2 Features 3 Architecture 4 Usage 5 Future Work 6 Related Work Acknowledgements References SLAB: A Certifying Model Checker for Infinte-State Concurrent Systems 1 Slicing Abstractions 2 Certifying Model Checker 3 Results References Tracking Heaps That Hop with Heap-Hop 1 Introduction 2 Heap-Hop 3 Internals 4 Related Work and Conclusion References Automatic Analysis of Scratch-Pad Memory Code for Heterogeneous Multicore Processors 1 Introduction 2 Direct Memory Access Operations 3 Goto Programs 4 Encoding DMA Operations in Goto Programs 5 k-Induction for Goto Programs 6 Experimental Evaluation 7 Related Work 8 Summary and Future Work References Simplifying Linearizability Proofs with Reduction and Abstraction 1 Introduction 2 Motivation and Overview 3 Concurrent Programs: Syntax and Semantics 4 Program Transformations 5 Soundness Theorems 6 Implementation and Experience References A Polymorphic Intermediate Verifcation Language: Design and Logical Encoding 1 Introduction 2 Boogie 2 Types and Expressions 3 Representation of Types as Terms 4 Translation of Expressions 5 Experimental Results and Related Work 6 Conclusions References Trace-Based Symbolic Analysis for Atomicity Violations 1 Introduction 2 Preliminaries 3 Three-Access Atomicity Violations 4 Capturing the Feasible Interleavings 5 Capturing Erroneous Trace Pre xes 6 Experiments 7 Related Work 8 Conclusions References ACS: Automatic Converter Synthesis for SoC Bus Protocols 1 Introduction 2 The Formal Foundations 3 ACS Process Flow 4 Experiments 5 Status and Future Work References AlPiNA: An Algebraic Petri Net Analyzer 1 Introduction 2 Theoretical Foundations of AlPiNA 3 Tool Description 4 Current Status and Perspectives References PASS: Abstraction Refinemet for Infinit Probabilistic Models 1 Introducing PASS 2 Architecture 3 Selected Features 4 Concluding Remarks References Arrival Curves for Real-Time Calculus: The Causality Problem and Its Solutions 1 Introduction 2 Arrival Curves 3 Causality: Definiion and Characterization 4 Computing the Causality Closure 5 Algorithms for Discrete Finite Curves 6 Conclusion References Computing the Leakage of Information-Hiding Systems 1 Introduction 2 Preliminaries 3 Information Hiding Systems 4 Reachability Analysis Approach 5 The Iterative Approach 6 Information Hiding Systems with Variable a Priori 7 Interactive Information Hiding Systems 8 Related Work 9 Conclusion and Future Work References Statistical Measurement of Information Leakage 1 Introduction 2 Information-Theoretic Measures of Information Leakage 3 System Model and Assumptions 4 Estimating Information Leakage 5 Bounds on the Possible Error 6 Application to the Mixminion Remailer 7 Conclusion References SAT Based Bounded Model Checking with Partial Order Semantics for Timed Automata 1 Introduction 2 Preliminaries 3 Concurrency 4 SAT Reduction 5 Integrating State Invariants 6 Examples and Experiments 7 Conclusions and Future Work References Preemption Sealing for Efficient Concurrency Testing 1 Introduction 2 Preemption-Bounded Scheduling 3 Preemption Sealing 4 Implementation and Evaluation 5 Related Work 6 Conclusions References Code Mutation in Verification and Automatic Code Correction 1 Introduction 2 Background 3 Evolution of Architectures 4 Co-evolution of Programs and Counterexamples 5 Finding and Correcting Errors in a-Core 6 Conclusions References Efficient Detection of Errors in Java Components Using Random Environment and Restarts 1 Introduction 2 Example Components 3 General Notes on Experiments 4 Checking Components with Universal Environment 5 Random-Sequence Environments 6 Restart Strategies 7 Evaluation 8 Related Work 9 Summary and Future Work References Author Index