Tools and Algorithms for the Construction and Analysis of Systems : 18th International Conference, TACAS 2012, Held As Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2012, Tallinn, Estonia, March 24 -- April 1, 2012, Proc

Annotation. This book constitutes the proceedings of the 18th International Conference on Tools and Algorithms for the Construction and Analysis of Systems, TACAS 2012, held as part of the joint European Conference on Theory and Practice of Software, ETAPS 2012, which took place in Tallinn, Estonia, in March/April 2012. The 25 research papers, 2 case study papers, 3 regular tool papers, and 6 tool demonstrations papers presented in this book were carefully reviewed and selected from a total of 147 submissions. The papers are organized in topical sections named: SAT and SMT based methods; automata; model checking; case studies; memory models and termination; internet protocol verification; stochastic model checking; synthesis; provers and analysis techniques; tool demonstrations; and competition on software verification Front Matter....Pages - Quantitative Models for a Not So Dumb Grid....Pages 1-1 History-Aware Data Structure Repair Using SAT....Pages 2-17 The Guardol Language and Verification System....Pages 18-32 A Bit Too Precise? Bounded Verification of Quantized Digital Filters....Pages 33-47 Numeric Bounds Analysis with Conflict-Driven Learning....Pages 48-63 Ramsey-Based Analysis of Parity Automata....Pages 64-78 VATA: A Library for Efficient Manipulation of Non-deterministic Tree Automata....Pages 79-94 LTL to Büchi Automata Translation: Fast and More Deterministic....Pages 95-109 Pushdown Model Checking for Malware Detection....Pages 110-125 Aspect-Oriented Runtime Monitor Certification....Pages 126-140 Partial Model Checking Using Networks of Labelled Transition Systems and Boolean Equation Systems....Pages 141-156 From Under-Approximations to Over-Approximations and Back....Pages 157-172 Automated Analysis of AODV Using UPPAAL....Pages 173-187 Modeling and Verification of a Dual Chamber Implantable Pacemaker....Pages 188-203 Counter-Example Guided Fence Insertion under TSO....Pages 204-219 Java Memory Model-Aware Model Checking....Pages 220-236 Compositional Termination Proofs for Multi-threaded Programs....Pages 237-251 Deciding Conditional Termination....Pages 252-266 The AVANTSSAR Platform for the Automated Validation of Trust and Security of Service-Oriented Architectures....Pages 267-282 Reduction-Based Formal Analysis of BGP Instances....Pages 283-298 Minimal Critical Subsystems for Discrete-Time Markov Models....Pages 299-314 Automatic Verification of Competitive Stochastic Systems....Pages 315-330 Coupling and Importance Sampling for Statistical Model Checking....Pages 331-346 Verifying pCTL Model Checking....Pages 347-361 Parameterized Synthesis....Pages 362-376 QuteRTL: Towards an Open Source Framework for RTL Design Synthesis and Verification....Pages 377-391 Template-Based Controller Synthesis for Timed Systems....Pages 392-406 Zeno: An Automated Prover for Properties of Recursive Data Structures....Pages 407-421 A Proof Assistant for Alloy Specifications....Pages 422-436 Reachability under Contextual Locking....Pages 437-450 Bounded Phase Analysis of Message-Passing Programs....Pages 451-465 Demonstrating Learning of Register Automata....Pages 466-471 Symbolic Automata: The Toolkit....Pages 472-477 McScM: A General Framework for the Verification of Communicating Machines....Pages 478-484 SLMC: A Tool for Model Checking Concurrent Systems against Dynamical Spatial Logic Specifications....Pages 485-491 TAPAAL 2.0: Integrated Development Environment for Timed-Arc Petri Nets....Pages 492-497 A Platform for High Performance Statistical Model Checking – PLASMA....Pages 498-503 Competition on Software Verification....Pages 504-524 Predicate Analysis with BLAST 2.7....Pages 525-527 CPAchecker with Adjustable Predicate Analysis....Pages 528-530 Block Abstraction Memoization for CPAchecker....Pages 531-533 Context-Bounded Model Checking with ESBMC 1.17....Pages 534-537 Proving Reachability Using FShell ....Pages 538-541 LLBMC : A Bounded Model Checker for LLVM ’s Intermediate Representation....Pages 542-544 Predator: A Verification Tool for Programs with Dynamic Linked Data Structures....Pages 545-548 HSF(C): A Software Verifier Based on Horn Clauses....Pages 549-551 satabs : A Bit-Precise Verifier for C Programs....Pages 552-555 Wolverine : Battling Bugs with Interpolants....Pages 556-558 Back Matter....Pages - Edited By Cormac Flanagan, Barbara König.