18. TACAS 2012: Tallinn, Estonia (Part of ETAPS 2012)

Cormac Flanagan, Barbara König (Eds.): 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. Lecture Notes in Computer Science 7214 Springer 2012, ISBN 978-3-642-28755-8

Invited Contribution

Holger Hermanns:
Quantitative Models for a Not So Dumb Grid. 1

SAT and SMT Based Methods

Razieh Nokhbeh Zaeem, Divya Gopinath, Sarfraz Khurshid, Kathryn S. McKinley:
History-Aware Data Structure Repair Using SAT. 2-17
David S. Hardin, Konrad Slind, Michael W. Whalen, Tuan-Hung Pham:
The Guardol Language and Verification System. 18-32
Arlen Cox, Sriram Sankaranarayanan, Bor-Yuh Evan Chang:
A Bit Too Precise? Bounded Verification of Quantized Digital Filters. 33-47
Vijay D'Silva, Leopold Haller, Daniel Kroening, Michael Tautschnig:
Numeric Bounds Analysis with Conflict-Driven Learning. 48-63

Automata

Oliver Friedmann, Martin Lange:
Ramsey-Based Analysis of Parity Automata. 64-78
Ondrej Lengál, Jirí Simácek, Tomás Vojnar:
VATA: A Library for Efficient Manipulation of Non-deterministic Tree Automata. 79-94
Tomás Babiak, Mojmír Kretínský, Vojtech Rehák, Jan Strejcek:
LTL to Büchi Automata Translation: Fast and More Deterministic. 95-109

Model Checking

Fu Song, Tayssir Touili:
Pushdown Model Checking for Malware Detection. 110-125
Kevin W. Hamlen, Micah Jones, Meera Sridhar:
Aspect-Oriented Runtime Monitor Certification. 126-140
Frédéric Lang, Radu Mateescu:
Partial Model Checking Using Networks of Labelled Transition Systems and Boolean Equation Systems. 141-156
Aws Albarghouthi, Arie Gurfinkel, Marsha Chechik:
From Under-Approximations to Over-Approximations and Back. 157-172

Case Studies

Ansgar Fehnker, Rob J. van Glabbeek, Peter Höfner, Annabelle McIver, Marius Portmann, Wee Lum Tan:
Automated Analysis of AODV Using UPPAAL. 173-187
Zhihao Jiang, Miroslav Pajic, Salar Moarref, Rajeev Alur, Rahul Mangharam:
Modeling and Verification of a Dual Chamber Implantable Pacemaker. 188-203

Memory Models and Termination

Parosh Aziz Abdulla, Mohamed Faouzi Atig, Yu-Fang Chen, Carl Leonardsson, Ahmed Rezine:
Counter-Example Guided Fence Insertion under TSO. 204-219
Huafeng Jin, Tuba Yavuz-Kahveci, Beverly A. Sanders:
Java Memory Model-Aware Model Checking. 220-236
Corneliu Popeea, Andrey Rybalchenko:
Compositional Termination Proofs for Multi-threaded Programs. 237-251
Marius Bozga, Radu Iosif, Filip Konecný:
Deciding Conditional Termination. 252-266

Internet Protocol Verification

Alessandro Armando, Wihem Arsac, Tigran Avanesov, Michele Barletta, Alberto Calvi, Alessandro Cappai, Roberto Carbone, Yannick Chevalier, Luca Compagna, Jorge Cuéllar, Gabriel Erzse, Simone Frau, Marius Minea, Sebastian Mödersheim, David von Oheimb, Giancarlo Pellegrino, Serena Elisa Ponta, Marco Rocchetto, Michaël Rusinowitch, Mohammad Torabi Dashti, Mathieu Turuani, Luca Viganò:
The AVANTSSAR Platform for the Automated Validation of Trust and Security of Service-Oriented Architectures. 267-282
Anduo Wang, Carolyn L. Talcott, Alexander J. T. Gurney, Boon Thau Loo, Andre Scedrov:
Reduction-Based Formal Analysis of BGP Instances. 283-298

Stochastic Model Checking

Ralf Wimmer, Nils Jansen, Erika Ábrahám, Bernd Becker, Joost-Pieter Katoen:
Minimal Critical Subsystems for Discrete-Time Markov Models. 299-314
Taolue Chen, Vojtech Forejt, Marta Z. Kwiatkowska, David Parker, Aistis Simaitis:
Automatic Verification of Competitive Stochastic Systems. 315-330
Benoît Barbot, Serge Haddad, Claudine Picaronny:
Coupling and Importance Sampling for Statistical Model Checking. 331-346
Johannes Hölzl, Tobias Nipkow:
Verifying pCTL Model Checking. 347-361

Synthesis

Swen Jacobs, Roderick Bloem:
Parameterized Synthesis. 362-376
Hu-Hsi Yeh, Cheng-Yin Wu, Chung-Yang (Ric) Huang:
QuteRTL: Towards an Open Source Framework for RTL Design Synthesis and Verification. 377-391
Bernd Finkbeiner, Hans-Jörg Peter:
Template-Based Controller Synthesis for Timed Systems. 392-406

Provers and Analysis Techniques

William Sonnex, Sophia Drossopoulou, Susan Eisenbach:
Zeno: An Automated Prover for Properties of Recursive Data Structures. 407-421
Mattias Ulbrich, Ulrich Geilmann, Aboubakr Achraf El Ghazi, Mana Taghdiri:
A Proof Assistant for Alloy Specifications. 422-436
Rohit Chadha, P. Madhusudan, Mahesh Viswanathan:
Reachability under Contextual Locking. 437-450
Ahmed Bouajjani, Michael Emmi:
Bounded Phase Analysis of Message-Passing Programs. 451-465

Tool Demonstrations

Maik Merten, Falk Howar, Bernhard Steffen, Sofia Cassel, Bengt Jonsson:
Demonstrating Learning of Register Automata. 466-471
Margus Veanes, Nikolaj Bjørner:
Symbolic Automata: The Toolkit. 472-477
Alexander Heußner, Tristan Le Gall, Grégoire Sutre:
McScM: A General Framework for the Verification of Communicating Machines. 478-484
Luís Caires, Hugo Torres Vieira:
SLMC: A Tool for Model Checking Concurrent Systems against Dynamical Spatial Logic Specifications. 485-491
Alexandre David, Lasse Jacobsen, Morten Jacobsen, Kenneth Yrke Jørgensen, Mikael H. Møller, Jirí Srba:
TAPAAL 2.0: Integrated Development Environment for Timed-Arc Petri Nets. 492-497
Cyrille Jégourel, Axel Legay, Sean Sedwards:
A Platform for High Performance Statistical Model Checking - PLASMA. 498-503

Competition on Software Verification

Dirk Beyer:
Competition on Software Verification - (SV-COMP). 504-524
Pavel Shved, Mikhail Mandrykin, Vadim Mutilin:
Predicate Analysis with BLAST 2.7 - (Competition Contribution). 525-527
Stefan Löwe, Philipp Wendler:
CPAchecker with Adjustable Predicate Analysis - (Competition Contribution). 528-530
Daniel Wonisch:
Block Abstraction Memoization for CPAchecker - (Competition Contribution). 531-533
Lucas Cordeiro, Jeremy Morse, Denis Nicole, Bernd Fischer:
Context-Bounded Model Checking with ESBMC 1.17 - (Competition Contribution). 534-537
Andreas Holzer, Daniel Kroening, Christian Schallhart, Michael Tautschnig, Helmut Veith:
Proving Reachability Using FShell - (Competition Contribution). 538-541
Carsten Sinz, Florian Merz, Stephan Falke:
LLBMC: A Bounded Model Checker for LLVM's Intermediate Representation - (Competition Contribution). 542-544
Kamil Dudka, Petr Müller, Petr Peringer, Tomás Vojnar:
Predator: A Verification Tool for Programs with Dynamic Linked Data Structures - (Competition Contribution). 545-548
Sergey Grebenshchikov, Ashutosh Gupta, Nuno P. Lopes, Corneliu Popeea, Andrey Rybalchenko:
HSF(C): A Software Verifier Based on Horn Clauses - (Competition Contribution). 549-551
Gérard Basler, Alastair F. Donaldson, Alexander Kaiser, Daniel Kroening, Michael Tautschnig, Thomas Wahl:
satabs: A Bit-Precise Verifier for C Programs - (Competition Contribution). 552-555
Georg Weissenbacher, Daniel Kroening, Sharad Malik:
Wolverine: Battling Bugs with Interpolants - (Competition Contribution). 556-558

Last update Sat May 18 19:51:05 2013 CET by the DBLP Team —

Data released under the ODC-BY 1.0 license — See also our legal information page