Tools and Algorithms for the Construction and Analysis of Systems [recurso electrónico] 20th International Conference, TACAS 2014, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2014, Grenoble, France, April 5-13,

This book constitutes the proceedings of the 20th International Conference on Tools and Algorithms for the Construction and Analysis of Systems, TACAS 2014, which took place in Grenoble, France, in April 2014, as part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2014. The total of 42 papers included in this volume, consisting of 26 research papers, 3 case study papers, 6 regular tool papers and 7 tool demonstrations papers, were carefully reviewed and selected from 161 submissions. In addition the book contains one invited contribution. The papers are organized in topical sections named: decision procedures and their application in analysis; complexity and termination analysis; modeling and model checking discrete systems; timed and hybrid systems; monitoring, fault detection and identification; competition on software verification; specifying and checking linear time properties; synthesis and learning; quantum and probabilistic systems; as well as tool demonstrations and case studies. -- Source other than Library of Congress Front Matter....Pages - Variations on Safety....Pages 1-14 Decision Procedures for Flat Array Properties....Pages 15-30 SATMC: A SAT-Based Model Checker for Security-Critical Systems....Pages 31-45 IC3 Modulo Theories via Implicit Predicate Abstraction....Pages 46-61 SMT-Based Verification of Software Countermeasures against Side-Channel Attacks....Pages 62-77 Detecting Unrealizable Specifications of Distributed Systems....Pages 78-92 Synthesizing Safe Bit-Precise Invariants....Pages 93-108 PEALT: An Automated Reasoning Tool for Numerical Aggregation of Trust Evidence....Pages 109-123 GRASShopper ....Pages 124-139 Alternating Runtime and Size Complexity Analysis of Integer Programs....Pages 140-155 Proving Nontermination via Safety....Pages 156-171 Ranking Templates for Linear Loops....Pages 172-186 FDR3 — A Modern Refinement Checker for CSP....Pages 187-201 Concurrent Depth-First Search Algorithms....Pages 202-216 Basic Problems in Multi-View Modeling....Pages 217-232 GPUexplore: Many-Core On-the-Fly State Space Exploration Using GPUs....Pages 233-247 Forward Reachability Computation for Autonomous Max-Plus-Linear Systems....Pages 248-262 Compositional Invariant Generation for Timed Systems....Pages 263-278 Characterizing Algebraic Invariants by Differential Radical Invariants....Pages 279-294 Quasi-Equal Clock Reduction: More Networks, More Queries....Pages 295-309 Are Timed Automata Bad for a Specification Language? Language Inclusion Checking for Timed Automata....Pages 310-325 Formal Design of Fault Detection and Identification Components Using Temporal Epistemic Logic....Pages 326-340 Monitoring Modulo Theories....Pages 341-356 Temporal-Logic Based Runtime Observer Pairs for System Health Management of Real-Time Systems....Pages 357-372 Status Report on Software Verification....Pages 373-388 CBMC – C Bounded Model Checker....Pages 389-391 CPAchecker with Sequential Combination of Explicit-Value Analyses and Predicate Analyses....Pages 392-394 CPAlien : Shape Analyzer for CPAChecker....Pages 395-397 Lazy-CSeq: A Lazy Sequentialization Tool for C....Pages 398-401 MU-CSeq: Sequentialization of C Programs by Shared Memory Unwindings....Pages 402-404 ESBMC 1.22....Pages 405-407 FrankenBit : Bit-Precise Verification with Many Bits....Pages 408-411 Predator: A Shape Analyzer Based on Symbolic Memory Graphs....Pages 412-414 Symbiotic 2: More Precise Slicing....Pages 415-417 Ultimate Automizer with Unsatisfiable Cores....Pages 418-420 Ultimate Kojak....Pages 421-423 Discounting in LTL....Pages 424-439 Symbolic Model Checking of Stutter-Invariant Properties Using Generalized Testing Automata....Pages 440-454 Symbolic Synthesis for Epistemic Specifications with Observational Semantics....Pages 455-469 Synthesis for Human-in-the-Loop Control Systems....Pages 470-484 Learning Regular Languages over Large Alphabets....Pages 485-499 Verification of Concurrent Quantum Protocols by Equivalence Checking....Pages 500-514 Computing Conditional Probabilities in Markovian Models Efficiently....Pages 515-530 Permissive Controller Synthesis for Probabilistic Systems....Pages 531-546 Precise Approximations of the Probability Distribution of a Markov Process in Time: An Application to Probabilistic Invariance....Pages 547-561 SACO: Static Analyzer for Concurrent Objects....Pages 562-567 VeriMAP: A Tool for Verifying Programs through Transformations....Pages 568-574 CIF 3: Model-Based Engineering of Supervisory Controllers....Pages 575-580 EDD: A Declarative Debugger for Sequential Erlang Programs....Pages 581-586 APTE: An Algorithm for Proving Trace Equivalence....Pages 587-592 The Modest Toolset: An Integrated Environment for Quantitative Modelling and Verification....Pages 593-598 Bounds2: A Tool for Compositional Multi-parametrised Verification....Pages 599-604 On the Correctness of a Branch Displacement Algorithm....Pages 605-619 Analyzing the Next Generation Airborne Collision Avoidance System....Pages 620-635 Environment-Model Based Testing of Control Systems: Case Studies....Pages 636-650 Back Matter....Pages -