default search action
Google
Google Scholar
Semantic Scholar
Internet Archive Scholar
CiteSeerX
ORCID18th TACAS 2012: Tallinn, Estonia
- Cormac Flanagan, Barbara König:
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 Victor 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 S. 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 U. Mandrykin, Vadim S. 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 C. Cordeiro, Jeremy Morse, Denis A. 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
manage site settings
To protect your privacy, all features that rely on external API calls from your browser are turned off by default. You need to opt-in for them to become active. All settings here will be stored as cookies with your web browser. For more information see our F.A.Q.
last updated on 2026-01-29 02:07 CET by the dblp team
all metadata released as open data under CC0 1.0 license
see also: Terms of Use | Privacy Policy | Imprint
dblp was originally created in 1993 at:
since 2018, dblp has been operated and maintained by:
the dblp computer science bibliography is funded and supported by:
