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. Front Matter....Pages - Embedded Systems Design — Scientific Challenges and Work Directions....Pages 1-1 Antichain Algorithms for Finite Automata....Pages 2-22 Assume-Guarantee Verification for Probabilistic Systems....Pages 23-37 Simple O ( m log n ) Time Markov Chain Lumping....Pages 38-52 Model Checking Interactive Markov Chains....Pages 53-68 Approximating the Pareto Front of Multi-criteria Optimization Problems....Pages 69-83 An Alternative to SAT-Based Approaches for Bit-Vectors....Pages 84-98 Satisfiability Modulo the Theory of Costs: Foundations and Applications....Pages 99-113 Optimal Tableau Algorithms for Coalgebraic Logics....Pages 114-128 Blocked Clause Elimination....Pages 129-144 Boom : Taking Boolean Program Model Checking One Step Further....Pages 145-149 The OpenSMT Solver....Pages 150-153 Stranger : An Automata-Based String Analysis Tool for PHP....Pages 154-157 When Simulation Meets Antichains....Pages 158-174 On Weak Modal Compatibility, Refinement, and the MIO Workbench....Pages 175-189 Rational Synthesis....Pages 190-204 Efficient Büchi Universality Checking....Pages 205-220 Automated Termination Analysis for Programs with Second-Order Recursion....Pages 221-235 Ranking Function Synthesis for Bit-Vector Relations....Pages 236-250 Fairness for Dynamic Control....Pages 251-265 JTorX: A Tool for On-Line Model-Driven Test Derivation and Execution....Pages 266-270 SLAB: A Certifying Model Checker for Infinite-State Concurrent Systems....Pages 271-274 Tracking Heaps That Hop with Heap-Hop....Pages 275-279 Automatic Analysis of Scratch-Pad Memory Code for Heterogeneous Multicore Processors....Pages 280-295 Simplifying Linearizability Proofs with Reduction and Abstraction....Pages 296-311 A Polymorphic Intermediate Verification Language: Design and Logical Encoding....Pages 312-327 Trace-Based Symbolic Analysis for Atomicity Violations....Pages 328-342 ACS: Automatic Converter Synthesis for SoC Bus Protocols....Pages 343-348 AlPiNA: An Algebraic Petri Net Analyzer....Pages 349-352 PASS : Abstraction Refinement for Infinite Probabilistic Models....Pages 353-357 Arrival Curves for Real-Time Calculus: The Causality Problem and Its Solutions....Pages 358-372 Computing the Leakage of Information-Hiding Systems....Pages 373-389 Statistical Measurement of Information Leakage....Pages 390-404 SAT Based Bounded Model Checking with Partial Order Semantics for Timed Automata....Pages 405-419 Preemption Sealing for Efficient Concurrency Testing....Pages 420-434 Code Mutation in Verification and Automatic Code Correction....Pages 435-450 Efficient Detection of Errors in Java Components Using Random Environment and Restarts....Pages 451-465 Back Matter....Pages -