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

Front Matter....Pages -
On-the-Fly Exact Computation of Bisimilarity Distances....Pages 1-15
The Quest for Minimal Quotients for Probabilistic Automata....Pages 16-31
LTL Model Checking of Interval Markov Chains....Pages 32-46
Ramsey vs. Lexicographic Termination Proving....Pages 47-61
Structural Counter Abstraction....Pages 62-77
Extending Quantifier Elimination to Linear Inequalities on Bit-Vectors....Pages 78-92
The MathSAT5 SMT Solver....Pages 93-107
Formula Preprocessing in MUS Extraction....Pages 108-123
Proof Tree Preserving Interpolation....Pages 124-138
Asynchronous Multi-core Incremental SAT Solving....Pages 139-153
Model-Checking Iterated Games....Pages 154-168
Synthesis from LTL Specifications with Mean-Payoff Objectives....Pages 169-184
PRISM-games: A Model Checker for Stochastic Multi-Player Games....Pages 185-191
PIC2LNT: Model Transformation for Model Checking an Applied Pi-Calculus....Pages 192-198
An Overview of the mCRL2 Toolset and Its Recent Advances....Pages 199-213
Analysis of Boolean Programs....Pages 214-229
Weighted Pushdown Systems with Indexed Weight Domains....Pages 230-244
Underapproximation of Procedure Summaries for Integer Programs....Pages 245-259
Runtime Verification Based on Register Automata....Pages 260-276
Unbounded Model-Checking with Interpolation for Regular Language Constraints....Pages 277-291
eVolCheck: Incremental Upgrade Checker for C....Pages 292-307
Intertwined Forward-Backward Reachability Analysis Using Interpolants....Pages 308-323
An Integrated Specification and Verification Technique for Highly Concurrent Data Structures....Pages 324-338
A Verification-Based Approach to Memory Fence Insertion in PSO Memory Systems....Pages 339-353
Identifying Dynamic Data Structures by Learning Evolving Patterns in Memory....Pages 354-369
Synthesis of Circular Compositional Program Proofs via Abduction....Pages 370-384
As Soon as Probable: Optimal Scheduling under Stochastic Uncertainty....Pages 385-400
Integer Parameter Synthesis for Timed Automata....Pages 401-415
LTL Model-Checking for Malware Detection....Pages 416-431
Policy Analysis for Self-administrated Role-Based Access Control....Pages 432-447
Model Checking Agent Knowledge in Dynamic Access Control Policies....Pages 448-462
Automatic Testing of Real-Time Graphics Systems....Pages 463-477
Equivalence Checking of Quantum Protocols....Pages 478-492
Encoding Monomorphic and Polymorphic Types....Pages 493-507
Deriving Probability Density Functions from Probabilistic Functional Programs....Pages 508-522
Polyglot: Systematic Analysis for Multiple Statechart Formalisms....Pages 523-529
 Memorax , a Precise and Sound Tool for Automatic Fence Insertion under TSO....Pages 530-536
BULL: A Library for Learning Algorithms of Boolean Functions....Pages 537-542
AppGuard – Enforcing User Requirements on Android Apps....Pages 543-548
Model Checking Database Applications....Pages 549-564
Efficient Property Preservation Checking of Model Refinements....Pages 565-579
Strength-Based Decomposition of the Property Büchi Automaton for Faster Model Checking....Pages 580-593
Second Competition on Software Verification....Pages 594-609
 CPAchecker with Explicit-Value Analysis Based on CEGAR and Interpolation....Pages 610-612
 CPAchecker with Sequential Combination of Explicit-State Analysis and Predicate Analysis....Pages 613-615
CSeq: A Sequentialization Tool for C....Pages 616-618
Handling Unbounded Loops with ESBMC 1.20....Pages 619-622
 LLBMC : Improved Bounded Model Checking of C Programs Using LLVM ....Pages 623-626
Predator: A Tool for Verification of Low-Level List Manipulation....Pages 627-629
Symbiotic: Synergy of Instrumentation, Slicing, and Symbolic Execution....Pages 630-632
Threader: A Verifier for Multi-threaded Programs....Pages 633-636
UFO: Verification with Interpolants and Abstract Interpretation....Pages 637-640
Ultimate Automizer with SMTInterpol....Pages 641-643
Back Matter....Pages -