TACAS 2012

48 papers

1. A Bit Too Precise? Bounded Verification of Quantized Digital Filters · Arlen Cox, Sriram Sankaranarayanan, Bor-Yuh Evan Chang
2. A Platform for High Performance Statistical Model Checking - PLASMA · Cyrille Jégourel, Axel Legay, Sean Sedwards
3. A Proof Assistant for Alloy Specifications · Mattias Ulbrich, Ulrich Geilmann, Aboubakr Achraf El Ghazi, Mana Taghdiri
4. Aspect-Oriented Runtime Monitor Certification · Kevin W. Hamlen, Micah Jones, Meera Sridhar
5. Automated Analysis of AODV Using UPPAAL · Ansgar Fehnker, Rob J. van Glabbeek, Peter Höfner, Annabelle McIver, Marius Portmann, Wee Lum Tan
6. Automatic Verification of Competitive Stochastic Systems · Taolue Chen, Vojtech Forejt, Marta Z. Kwiatkowska, David Parker, Aistis Simaitis
7. Block Abstraction Memoization for CPAchecker - (Competition Contribution) · Daniel Wonisch
8. Bounded Phase Analysis of Message-Passing Programs · Ahmed Bouajjani, Michael Emmi
9. CPAchecker with Adjustable Predicate Analysis - (Competition Contribution) · Stefan Löwe, Philipp Wendler
10. Competition on Software Verification - (SV-COMP) · Dirk Beyer
11. Compositional Termination Proofs for Multi-threaded Programs · Corneliu Popeea, Andrey Rybalchenko
12. Context-Bounded Model Checking with ESBMC 1.17 - (Competition Contribution) · Lucas C. Cordeiro, Jeremy Morse, Denis A. Nicole, Bernd Fischer
13. Counter-Example Guided Fence Insertion under TSO · Parosh Aziz Abdulla, Mohamed Faouzi Atig, Yu-Fang Chen, Carl Leonardsson, Ahmed Rezine
14. Coupling and Importance Sampling for Statistical Model Checking · Benoît Barbot, Serge Haddad, Claudine Picaronny
15. Deciding Conditional Termination · Marius Bozga, Radu Iosif, Filip Konecný
16. Demonstrating Learning of Register Automata · Maik Merten, Falk Howar, Bernhard Steffen, Sofia Cassel, Bengt Jonsson
17. From Under-Approximations to Over-Approximations and Back · Aws Albarghouthi, Arie Gurfinkel, Marsha Chechik
18. HSF(C): A Software Verifier Based on Horn Clauses - (Competition Contribution) · Sergey Grebenshchikov, Ashutosh Gupta, Nuno P. Lopes, Corneliu Popeea, Andrey Rybalchenko
19. History-Aware Data Structure Repair Using SAT · Razieh Nokhbeh Zaeem, Divya Gopinath, Sarfraz Khurshid, Kathryn S. McKinley
20. Java Memory Model-Aware Model Checking · Huafeng Jin, Tuba Yavuz-Kahveci, Beverly A. Sanders
21. LLBMC: A Bounded Model Checker for LLVM's Intermediate Representation - (Competition Contribution) · Carsten Sinz, Florian Merz, Stephan Falke
22. LTL to Büchi Automata Translation: Fast and More Deterministic · Tomás Babiak, Mojmír Kretínský, Vojtech Rehák, Jan Strejcek
23. McScM: A General Framework for the Verification of Communicating Machines · Alexander Heußner, Tristan Le Gall, Grégoire Sutre
24. Minimal Critical Subsystems for Discrete-Time Markov Models · Ralf Wimmer, Nils Jansen, Erika Ábrahám, Bernd Becker, Joost-Pieter Katoen
25. Modeling and Verification of a Dual Chamber Implantable Pacemaker · Zhihao Jiang, Miroslav Pajic, Salar Moarref, Rajeev Alur, Rahul Mangharam
26. Numeric Bounds Analysis with Conflict-Driven Learning · Vijay Victor D'Silva, Leopold Haller, Daniel Kroening, Michael Tautschnig
27. Parameterized Synthesis · Swen Jacobs, Roderick Bloem
28. Partial Model Checking Using Networks of Labelled Transition Systems and Boolean Equation Systems · Frédéric Lang, Radu Mateescu
29. Predator: A Verification Tool for Programs with Dynamic Linked Data Structures - (Competition Contribution) · Kamil Dudka, Petr Müller, Petr Peringer, Tomás Vojnar
30. Predicate Analysis with BLAST 2.7 - (Competition Contribution) · Pavel Shved, Mikhail U. Mandrykin, Vadim S. Mutilin
31. Proving Reachability Using FShell - (Competition Contribution) · Andreas Holzer, Daniel Kroening, Christian Schallhart, Michael Tautschnig, Helmut Veith
32. Pushdown Model Checking for Malware Detection · Fu Song, Tayssir Touili
33. Quantitative Models for a Not So Dumb Grid · Holger Hermanns
34. QuteRTL: Towards an Open Source Framework for RTL Design Synthesis and Verification · Hu-Hsi Yeh, Cheng-Yin Wu, Chung-Yang (Ric) Huang
35. Ramsey-Based Analysis of Parity Automata · Oliver Friedmann, Martin Lange
36. Reachability under Contextual Locking · Rohit Chadha, P. Madhusudan, Mahesh Viswanathan
37. Reduction-Based Formal Analysis of BGP Instances · Anduo Wang, Carolyn L. Talcott, Alexander J. T. Gurney, Boon Thau Loo, Andre Scedrov
38. SLMC: A Tool for Model Checking Concurrent Systems against Dynamical Spatial Logic Specifications · Luís Caires, Hugo Torres Vieira
39. Symbolic Automata: The Toolkit · Margus Veanes, Nikolaj S. Bjørner
40. TAPAAL 2.0: Integrated Development Environment for Timed-Arc Petri Nets · Alexandre David, Lasse Jacobsen, Morten Jacobsen, Kenneth Yrke Jørgensen, Mikael H. Møller, Jirí Srba
41. Template-Based Controller Synthesis for Timed Systems · Bernd Finkbeiner, Hans-Jörg Peter
42. 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 + 16 more
43. The Guardol Language and Verification System · David S. Hardin, Konrad Slind, Michael W. Whalen, Tuan-Hung Pham
44. VATA: A Library for Efficient Manipulation of Non-deterministic Tree Automata · Ondrej Lengál, Jirí Simácek, Tomás Vojnar
45. Verifying pCTL Model Checking · Johannes Hölzl, Tobias Nipkow
46. Wolverine: Battling Bugs with Interpolants - (Competition Contribution) · Georg Weissenbacher, Daniel Kroening, Sharad Malik
47. Zeno: An Automated Prover for Properties of Recursive Data Structures · William Sonnex, Sophia Drossopoulou, Susan Eisenbach
48. satabs: A Bit-Precise Verifier for C Programs - (Competition Contribution) · Gérard Basler, Alastair F. Donaldson, Alexander Kaiser, Daniel Kroening, Michael Tautschnig, Thomas Wahl