Tools and Algorithms for the Construction and Analysis of Systems

1. Front Matter

   PDF

2. Invited Contribution

   1. Quantitative Models for a Not So Dumb Grid

      • Holger Hermanns

      Pages 1-1

3. SAT and SMT Based Methods

   1. History-Aware Data Structure Repair Using SAT

      • Razieh Nokhbeh Zaeem, Divya Gopinath, Sarfraz Khurshid, Kathryn S. McKinley

      Pages 2-17

   2. The Guardol Language and Verification System

      • David Hardin, Konrad Slind, Michael Whalen, Tuan-Hung Pham

      Pages 18-32

   3. A Bit Too Precise? Bounded Verification of Quantized Digital Filters

      • Arlen Cox, Sriram Sankaranarayanan, Bor-Yuh Evan Chang

      Pages 33-47

   4. Numeric Bounds Analysis with Conflict-Driven Learning

      • Vijay D’Silva, Leopold Haller, Daniel Kroening, Michael Tautschnig

      Pages 48-63

4. Automata

   1. Ramsey-Based Analysis of Parity Automata

      • Oliver Friedmann, Martin Lange

      Pages 64-78

   2. VATA: A Library for Efficient Manipulation of Non-deterministic Tree Automata

      • Ondřej Lengál, Jiří Šimáček, Tomáš Vojnar

      Pages 79-94

   3. LTL to Büchi Automata Translation: Fast and More Deterministic

      • Tomáš Babiak, Mojmír Křetínský, Vojtěch Řehák, Jan Strejček

      Pages 95-109

5. Model Checking

   1. Pushdown Model Checking for Malware Detection

      • Fu Song, Tayssir Touili

      Pages 110-125

   2. Aspect-Oriented Runtime Monitor Certification

      • Kevin W. Hamlen, Micah M. Jones, Meera Sridhar

      Pages 126-140

   3. Partial Model Checking Using Networks of Labelled Transition Systems and Boolean Equation Systems

      • Frédéric Lang, Radu Mateescu

      Pages 141-156

   4. From Under-Approximations to Over-Approximations and Back

      • Aws Albarghouthi, Arie Gurfinkel, Marsha Chechik

      Pages 157-172

6. Case Studies

   1. Automated Analysis of AODV Using UPPAAL

      • Ansgar Fehnker, Rob van Glabbeek, Peter Höfner, Annabelle McIver, Marius Portmann, Wee Lum Tan

      Pages 173-187

   2. Modeling and Verification of a Dual Chamber Implantable Pacemaker

      • Zhihao Jiang, Miroslav Pajic, Salar Moarref, Rajeev Alur, Rahul Mangharam

      Pages 188-203

7. Memory Models and Termination

   1. Counter-Example Guided Fence Insertion under TSO

      • Parosh Aziz Abdulla, Mohamed Faouzi Atig, Yu-Fang Chen, Carl Leonardsson, Ahmed Rezine

      Pages 204-219

   2. Java Memory Model-Aware Model Checking

      • Huafeng Jin, Tuba Yavuz-Kahveci, Beverly A. Sanders

      Pages 220-236

   3. Compositional Termination Proofs for Multi-threaded Programs

      • Corneliu Popeea, Andrey Rybalchenko

      Pages 237-251

   4. Deciding Conditional Termination

      • Marius Bozga, Radu Iosif, Filip Konečný

      Pages 252-266

8. Internet Protocol Verification

   1. The AVANTSSAR Platform for the Automated Validation of Trust and Security of Service-Oriented Architectures

      • Alessandro Armando, Wihem Arsac, Tigran Avanesov, Michele Barletta, Alberto Calvi, Alessandro Cappai et al.

      Pages 267-282

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.

• communication networks
• software analysis
• software engineering
• theoretical computer science

• University of California at Santa Cruz, Santa Cruz, USA

  Cormac Flanagan

• Fakultät für Ingenieurwesen, Abteilung für Informatik und Angewandte Kognitionswissenschaft, Universität Duisburg-Essen, Duisburg, Germany

  Barbara König

Policies and ethics