Tools and Algorithms for the Construction and Analysis of Systems : : 24th International Conference, TACAS 2018, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2018, Thessaloniki, Greece, April 14-20, 2018, Proceedings, Part I / / edited by Dirk Beyer, Marieke Huisman.

• Superior document: Theoretical Computer Science and General Issues, 10805
• Author: Dirk Beyer
• HerausgeberIn: Beyer, Dirk.; Huisman, Marieke.
• Place / Publishing House: Cham : : Springer International Publishing :, Imprint: Springer,, 2018.
• Year of Publication: 2018
• Edition: 1st ed. 2018.
• Language: English
• Series: Theoretical Computer Science and General Issues, 10805
• Physical Description: 1 online resource (XX, 429 p. 93 illus.)

This book is Open Access under a CC BY licence. .

Table of Contents

Theorem Proving -- Unification with Abstraction and Theory Instantiation in Saturation-based Reasoning -- Efficient verification of imperative programs using auto2 -- Frame Inference for Inductive Entailment Proofs in Separation Logic -- Verified Model Checking of Timed Automata -- SAT and SMT I -- Chain Reduction for Binary and Zero-Suppressed Decision Diagrams -- CDCLSym: Introducing E_ective Symmetry Breaking in SAT Solving -- Automatic Generation of Precise and Useful Commutativity Conditions -- Bit-Vector Model Counting using Statistical Estimation -- Deductive Verification -- Hoare Logics for Time Bounds -- A Verified Implementation of the Bounded List Container -- Automating Deductive Verification for Weak-Memory Programs -- Software Verification and Optimisation -- Property Checking Array Programs Using Loop Shrinking -- Invariant Synthesis for Incomplete Verification Engines -- Accelerating Syntax-Guided Invariant Synthesis -- Daisy - Framework for Analysis and Optimization of Numerical Programs -- Model Checking -- Oink: an Implementation and Evaluation of Modern Parity Game Solvers -- More Scalable LTL Model Checking via Discovering Design-Space Dependencies (D^3) -- Generation of Minimum Tree-like Witnesses for Existential CTL -- From Natural Projection to Partial Model Checking and Back -- Machine Learning -- ICE-based Refinement Type Discovery for Higher-Order Functional Programs -- Strategy Representation by Decision Trees in Reactive Synthesis -- Feature-Guided Black-Box Safety Testing of Deep Neural Networks. .