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. Proceedings

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 -