Tools and Algorithms for the Construction and Analysis of Systems [electronic resource] : 19th International Conference, TACAS 2013, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2013, Rome, Italy, March 16-24, 2013. Proceedings / edited by Nir Piterman, Scott A. Smolka.

On-the-Fly Exact Computation of Bisimilarity Distances -- The Quest for Minimal Quotients for Probabilistic Automata -- LTL Model Checking of Interval Markov Chains -- Ramsey vs. Lexicographic Termination Proving -- Structural Counter Abstraction -- Extending Quantifier Elimination to Linear Inequalities on Bit-Vectors -- The MathSAT5 SMT Solver -- Formula Preprocessing in MUS Extraction -- Proof Tree Preserving Interpolation -- Asynchronous Multi-core Incremental SAT Solving -- Model-Checking Iterated Games -- PRISM-games: A Model Checker for Stochastic Multi-Player Games -- PIC2LNT: Model Transformation for Model Checking an Applied Pi-Calculus -- An Overview of the mCRL2 Toolset and Its Recent Advances -- Analysis of Boolean Programs -- Weighted Pushdown Systems with Indexed Weight Domains -- Underapproximation of Procedure Summaries for Integer Programs -- Runtime Verification Based on Register Automata -- Unbounded Model-Checking with Interpolation for Regular Language Constraints -- eVolCheck: Incremental Upgrade Checker for C -- Intertwined Forward-Backward Reachability Analysis Using Interpolants -- An Integrated Specification and Verification Technique or Highly Concurrent Data Structures -- A Verification-Based Approach to Memory Fence Insertion in PSO Memory Systems -- Identifying Dynamic Data Structures by Learning Evolving Patterns in Memory -- Synthesis of Circular Compositional Program Proofs via Abduction -- As Soon as Probable: Optimal Scheduling under Stochastic Uncertainty -- Integer Parameter Synthesis for Timed Automata -- LTL Model-Checking for Malware Detection -- Policy Analysis for Self-administrated Role-Based Access Control -- Model Checking Agent Knowledge in Dynamic Access Control Policies -- Frontiers (Graphics and Quantum) Automatic Testing of Real-Time Graphics Systems -- Equivalence Checking of Quantum Protocols -- Encoding Monomorphic and Polymorphic Types -- Deriving Probability Density Functions from Probabilistic Functional Programs -- Tool Demonstrations Polyglot: Systematic Analysis for Multiple Statechart Formalisms -- Memorax, a Precise and Sound Tool for Automatic Fence Insertion under TSO -- BULL: A Library for Learning Algorithms of Boolean Functions -- AppGuard - Enforcing User Requirements on Android Apps -- Model Checking Database Applications -- Efficient Property Preservation Checking of Model Refinements -- Strength-Based Decomposition of the Property Büchi Automaton for Faster Model Checking -- Competition on Software Verification Second Competition on Software Verification (Summary of SV-COMP 2013) -- CPAchecker with Explicit-Value Analysis Based on CEGAR and Interpolation (Competition Contribution) -- CPAchecker with Sequential Combination of Explicit-State Analysis and Predicate Analysis (Competition Contribution) -- CSeq: A Sequentialization Tool for C (Competition Contribution) -- Handling Unbounded Loops with ESBMC 1.20 (Competition Contribution) -- LLBMC: Improved Bounded Model Checking of C Programs Using LLVM (Competition Contribution) -- Predator: A Tool for Verification of Low-Level List Manipulation (Competition Contribution) -- Symbiotic: Synergy of Instrumentation, Slicing, and Symbolic Execution (Competition Contribution) -- Threader: A Verifier for Multi-threaded Programs (Competition Contribution) -- UFO: Verification with Interpolants and Abstract Interpretation (Competition Contribution) -- Ultimate Automizer with SMTInterpol (Competition Contribution).