Ebook: 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. Procee

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.

---

Quantitative Models for a Not So Dumb Grid / Holger Hermanns -- History-Aware Data Structure Repair Using SAT / Razieh Nokhbeh Zaeem, Divya Gopinath, Sarfraz Khurshid and Kathryn S. McKinley -- The Guardol Language and Verification System / David Hardin, Konrad Slind, Michael Whalen and Tuan-Hung Pham -- A Bit Too Precise? Bounded Verification of Quantized Digital Filters / Arlen Cox, Sriram Sankaranarayanan and Bor-Yuh Evan Chang -- Numeric Bounds Analysis with Conflict-Driven Learning / Vijay D'Silva, Leopold Haller, Daniel Kroening and Michael Tautschnig -- Ramsey-Based Analysis of Parity Automata / Oliver Friedmann and Martin Lange -- VATA: A Library for Efficient Manipulation of Non-deterministic Tree Automata / OndrМЊej Lengal, JirМЊi SМЊimacМЊek and TomasМЊ Vojnar -- LTL to Buchi Automata Translation: Fast and More Deterministic / TomasМЊ Babiak, Mojmir KrМЊetinsky, VojteМЊch RМЊehak and Jan StrejcМЊek -- Pushdown Model Checking for Malware Detection / Fu Song and Tayssir Touili -- Aspect-Oriented Runtime Monitor Certification / Kevin W. Hamlen, Micah M. Jones and Meera Sridhar -- Partial Model Checking Using Networks of Labelled Transition Systems and Boolean Equation Systems / Frederic Lang and Radu Mateescu -- From Under-Approximations to Over-Approximations and Back / Aws Albarghouthi, Arie Gurfinkel and Marsha Chechik. Automated Analysis of AODV Using UPPAAL / Ansgar Fehnker, Rob van Glabbeek, Peter Hofner, Annabelle McIver and Marius Portmann, et al. -- Modeling and Verification of a Dual Chamber Implantable Pacemaker / Zhihao Jiang, Miroslav Pajic, Salar Moarref, Rajeev Alur and Rahul Mangharam -- Counter-Example Guided Fence Insertion under TSO / Parosh Aziz Abdulla, Mohamed Faouzi Atig, Yu-Fang Chen, Carl Leonardsson and Ahmed Rezine -- Java Memory Model-Aware Model Checking / Huafeng Jin, Tuba Yavuz-Kahveci and Beverly A. Sanders -- Compositional Termination Proofs for Multi-threaded Programs / Corneliu Popeea and Andrey Rybalchenko -- Deciding Conditional Termination / Marius Bozga, Radu Iosif and Filip KonecМЊny -- The AVANTSSAR Platform for the Automated Validation of Trust and Security of Service-Oriented Architectures / Alessandro Armando, Wihem Arsac, Tigran Avanesov, Michele Barletta and Alberto Calvi, et al. -- Reduction-Based Formal Analysis of BGP Instances / Anduo Wang, Carolyn Talcott, Alexander J. T. Gurney, Boon Thau Loo and Andre Scedrov -- Minimal Critical Subsystems for Discrete-Time Markov Models / Ralf Wimmer, Nils Jansen, Erika Abraham, Bernd Becker and Joost-Pieter Katoen -- Automatic Verification of Competitive Stochastic Systems / Taolue Chen, VojteМЊch Forejt, Marta Kwiatkowska, David Parker and Aistis Simaitis -- Coupling and Importance Sampling for Statistical Model Checking / BenoiМ‚t Barbot, Serge Haddad and Claudine Picaronny. Verifying pCTL Model Checking / Johannes Holzl and Tobias Nipkow -- Parameterized Synthesis / Swen Jacobs and Roderick Bloem -- QuteRTL: Towards an Open Source Framework for RTL Design Synthesis and Verification / Hu-Hsi Yeh, Cheng-Yin Wu and Chung-Yang (Ric) Huang -- Template-Based Controller Synthesis for Timed Systems / Bernd Finkbeiner and Hans-Jorg Peter -- Zeno: An Automated Prover for Properties of Recursive Data Structures / William Sonnex, Sophia Drossopoulou and Susan Eisenbach -- A Proof Assistant for Alloy Specifications / Mattias Ulbrich, Ulrich Geilmann, Aboubakr Achraf El Ghazi and Mana Taghdiri -- Reachability under Contextual Locking / Rohit Chadha, P. Madhusudan and Mahesh Viswanathan -- Bounded Phase Analysis of Message-Passing Programs / Ahmed Bouajjani and Michael Emmi -- Demonstrating Learning of Register Automata / Maik Merten, Falk Howar, Bernhard Steffen, Sofia Cassel and Bengt Jonsson -- Symbolic Automata: The Toolkit / Margus Veanes and Nikolaj BjГёrner -- McScM: A General Framework for the Verification of Communicating Machines / Alexander HeuГџner, Tristan Le Gall and Gregoire Sutre -- SLMC: A Tool for Model Checking Concurrent Systems against Dynamical Spatial Logic Specifications / Luis Caires and Hugo Torres Vieira -- TAPAAL 2.0: Integrated Development Environment for Timed-Arc Petri Nets / Alexandre David, Lasse Jacobsen, Morten Jacobsen, Kenneth Yrke JГёrgensen and Mikael H. MГёller, et al. -- A Platform for High Performance Statistical Model Checking - PLASMA / Cyrille Jegourel, Axel Legay and Sean Sedwards. Competition on Software Verification / (SV-COMP) / Dirk Beyer -- Predicate Analysis with BLAST 2.7 / (Competition Contribution) / Pavel Shved, Mikhail Mandrykin and Vadim Mutilin -- CPAchecker with Adjustable Predicate Analysis / (Competition Contribution) / Stefan Lowe and Philipp Wendler -- Block Abstraction Memoization for CPAchecker / (Competition Contribution) / Daniel Wonisch -- Context-Bounded Model Checking with ESBMC 1.17 / (Competition Contribution) / Lucas Cordeiro, Jeremy Morse, Denis Nicole and Bernd Fischer -- Proving Reachability Using FShell / (Competition Contribution) / Andreas Holzer, Daniel Kroening, Christian Schallhart, Michael Tautschnig and Helmut Veith -- LLBMC: A Bounded Model Checker for LLVM's Intermediate Representation / (Competition Contribution) / Carsten Sinz, Florian Merz and Stephan Falke -- Predator: A Verification Tool for Programs with Dynamic Linked Data Structures / (Competition Contribution) / Kamil Dudka, Petr Muller, Petr Peringer and TomasМЊ Vojnar -- HSF(C): A Software Verifier Based on Horn Clauses / (Competition Contribution) / Sergey Grebenshchikov, Ashutosh Gupta, Nuno P. Lopes, Corneliu Popeea and Andrey Rybalchenko -- satabs: A Bit-Precise Verifier for C Programs / (Competition Contribution) / Gerard Basler, Alastair Donaldson, Alexander Kaiser, Daniel Kroening and Michael Tautschnig, et al. -- Wolverine: Battling Bugs with Interpolants / (Competition Contribution) / Georg Weissenbacher, Daniel Kroening and Sharad Malik