Tools and Algorithms for the Construction and Analysis of Systems: 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, 2014. Proceedings

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 -