TACAS 2012 accepted papers

  • Oliver Friedmann and Martin Lange. Ramsey-Based Analysis of Parity Automata
  • Fu Song and Tayssir Touili. Pushdown Model Checking for Malware Detection
  • Parosh Abdulla, Mohamed Faouzi Atig, Yu-Fang Chen, Carl Leonardsson and Ahmed Rezine. Counter-Example Guided Fence Insertion under TSO
  • Johannes Hölzl and Tobias Nipkow. Verifying pCTL Model Checking
  • Hu Hsi Yeh, Cheng-Yin Wu and Chung-Yang Ric Huang. QuteRTL: Towards an Open Source Framework for RTL Design Synthesis and Verification
  • Kevin Hamlen, Micah Jones and Meera Sridhar. Aspect-Oriented Runtime Monitor Certification via Model-Checking
  • Anduo Wang, Carolyn Talcott, Alexander J.T. Gurney, Boon Thau Loo and Andre Scedrov. Reduction-based Formal Analysis of BGP Instances
  • Cyrille Jegourel, Axel Legay and Sean Sedwards. A Platform for High Performance Statistical Model Checking - PLASMA
  • Huafeng Jin, Tuba Yavuz-Kahveci and Beverly Sanders. Java Memory Model-Aware Model Checking
  • Frédéric Lang and Radu Mateescu. Partial Model Checking using Networks of Labeled Transition Systems and Boolean Equation Systems
  • Benoît Barbot, Serge Haddad and Claudine Picaronny. Coupling and Importance Sampling for Statistical Model Checking
  • Mattias Ulbrich, Ulrich Geilmann, Aboubakr Achraf El Ghazi and Mana Taghdiri. A Proof Assistant for Alloy Specifications
  • Alexandre David, Lasse Jacobsen, Morten Jacobsen, Kenneth Yrke Jørgensen, Mikael H. Møller and Jiri Srba. TAPAAL 2.0: Integrated Development Environment for Timed-Arc Petri Nets
  • Ansgar Fehnker, Rob Van Glabbeek, Peter Höfner, Annabelle Mciver, Marius Portmann and Wee Lum Tan. Automated Analysis of AODV using UPPAAL
  • Alexander Heußner, Tristan Le Gall and Grégoire Sutre. McScM: A Framework for the Verification of Communicating Machines
  • Taolue Chen, Vojtech Forejt, Marta Kwiatkowska, David Parker and Aistis Simaitis. Automatic Verification of Competitive Stochastic Systems
  • Tomáš Babiak, Mojmir Kretinsky, Vojtech Rehak and Jan Strejcek. LTL to Büchi Automata Translation: Fast and More Deterministic
  • Corneliu Popeea and Andrey Rybalchenko. Compositional Termination Proofs for Multi-Threaded Programs
  • Ondrej Lengal, Jiri Simacek and Tomas Vojnar. VATA: A Library for Efficient Manipulation of Non-Deterministic Tree Automata
  • Roderick Bloem and Swen Jacobs. Parameterized Synthesis
  • Rohit Chadha, P. Madhusudan and Mahesh Viswanathan. Reachability under Contextual Locking
  • Luis Caires and Hugo Torres Vieira. SLMC: A Tool for Model Checking Concurrent Systems against Dynamical Spatial Logic Specifications
  • Luca Viganò. The AVANTSSAR Platform for the Automated Validation of Trust and Security of Service-Oriented Architectures
  • Bernd Finkbeiner and Hans-Jörg Peter. Template-based Controller Synthesis for Timed Systems
  • Radu Iosif, Marius Bozga and Filip Konecny. Deciding Conditional Termination
  • Aws Albarghouthi, Arie Gurfinkel and Marsha Chechik. From Under-approximations to Over-approximations and Back
  • William Sonnex, Sophia Drossopoulou and Susan Eisenbach. Zeno: An automated prover for properties of recursive data structures
  • Razieh Nokhbeh Zaeem, Divya Gopinath, Sarfraz Khurshid and Kathryn S. Mckinley. History-Aware Data Structure Repair Using SAT
  • Zhihao Jiang, Miroslav Pajic, Salar Moarref, Rajeev Alur and Rahul Mangharam. Modeling and Verification of a Dual Chamber Implantable Pacemaker
  • Vijay D'Silva, Leopold Haller, Daniel Kroening and Michael Tautschnig. Numeric Bounds Analysis with Conflict-Driven Learning
  • Arlen Cox, Sriram Sankaranarayanan and Bor-Yuh Evan Chang. A Bit Too Precise? Bounded Verification of Quantized Digital Filters
  • Ralf Wimmer, Nils Jansen, Erika Abraham, Bernd Becker and Joost-Pieter Katoen. Minimal Critical Subsystems for Discrete-Time Markov Models
  • Konrad Slind, David Hardin, Mike Whalen and Tuan-Hung Pham. The Guardol Language and Verification System
  • Ahmed Bouajjani and Michael Emmi. Bounded Phase Analysis of Message-Passing Programs
  • Margus Veanes and Nikolaj Bjorner. Symbolic Automata: The Toolkit
  • Falk Howar, Maik Merten, Bernhard Steffen, Sofia Cassel and Bengt Jonsson. Demonstrating Learning of Register