| Description |
1 online resource (xix, 560 pages) |
| Series |
Lecture notes in computer science, 1611-3349 ; 7214. Advanced research in computing and software science |
|
LNCS sublibrary. SL 1, Theoretical computer science and general issues |
|
Lecture notes in computer science ; 7214. 0302-9743
|
|
Lecture notes in computer science. Advanced research in computing and software science.
|
|
LNCS sublibrary. SL 1, Theoretical computer science and general issues.
|
| Contents |
Quantitative Models for a Not So Dumb Grid / Holger Hermanns -- History-Aware Data Structure Repair Using SAT / Razieh Nokhbeh Zaeem, Divya Gopinath, Sarfraz Khurshid and Kathryn S. McKinley -- The Guardol Language and Verification System / David Hardin, Konrad Slind, Michael Whalen and Tuan-Hung Pham -- A Bit Too Precise? Bounded Verification of Quantized Digital Filters / Arlen Cox, Sriram Sankaranarayanan and Bor-Yuh Evan Chang -- Numeric Bounds Analysis with Conflict-Driven Learning / Vijay D'Silva, Leopold Haller, Daniel Kroening and Michael Tautschnig -- Ramsey-Based Analysis of Parity Automata / Oliver Friedmann and Martin Lange -- VATA: A Library for Efficient Manipulation of Non-deterministic Tree Automata / Ondřej Lengál, Jiří Šimáček and Tomáš Vojnar -- LTL to Büchi Automata Translation: Fast and More Deterministic / Tomáš Babiak, Mojmír Křetínský, Vojtěch Řehák and Jan Strejček -- Pushdown Model Checking for Malware Detection / Fu Song and Tayssir Touili -- Aspect-Oriented Runtime Monitor Certification / Kevin W. Hamlen, Micah M. Jones and Meera Sridhar -- Partial Model Checking Using Networks of Labelled Transition Systems and Boolean Equation Systems / Frédéric Lang and Radu Mateescu -- From Under-Approximations to Over-Approximations and Back / Aws Albarghouthi, Arie Gurfinkel and Marsha Chechik |
|
Automated Analysis of AODV Using UPPAAL / Ansgar Fehnker, Rob van Glabbeek, Peter Höfner, Annabelle McIver and Marius Portmann, et al. -- Modeling and Verification of a Dual Chamber Implantable Pacemaker / Zhihao Jiang, Miroslav Pajic, Salar Moarref, Rajeev Alur and Rahul Mangharam -- Counter-Example Guided Fence Insertion under TSO / Parosh Aziz Abdulla, Mohamed Faouzi Atig, Yu-Fang Chen, Carl Leonardsson and Ahmed Rezine -- Java Memory Model-Aware Model Checking / Huafeng Jin, Tuba Yavuz-Kahveci and Beverly A. Sanders -- Compositional Termination Proofs for Multi-threaded Programs / Corneliu Popeea and Andrey Rybalchenko -- Deciding Conditional Termination / Marius Bozga, Radu Iosif and Filip Konečný -- The AVANTSSAR Platform for the Automated Validation of Trust and Security of Service-Oriented Architectures / Alessandro Armando, Wihem Arsac, Tigran Avanesov, Michele Barletta and Alberto Calvi, et al. -- Reduction-Based Formal Analysis of BGP Instances / Anduo Wang, Carolyn Talcott, Alexander J.T. Gurney, Boon Thau Loo and Andre Scedrov -- Minimal Critical Subsystems for Discrete-Time Markov Models / Ralf Wimmer, Nils Jansen, Erika Ábrahám, Bernd Becker and Joost-Pieter Katoen -- Automatic Verification of Competitive Stochastic Systems / Taolue Chen, Vojtěch Forejt, Marta Kwiatkowska, David Parker and Aistis Simaitis -- Coupling and Importance Sampling for Statistical Model Checking / Benoît Barbot, Serge Haddad and Claudine Picaronny |
|
Verifying pCTL Model Checking / Johannes Hölzl and Tobias Nipkow -- Parameterized Synthesis / Swen Jacobs and Roderick Bloem -- QuteRTL: Towards an Open Source Framework for RTL Design Synthesis and Verification / Hu-Hsi Yeh, Cheng-Yin Wu and Chung-Yang (Ric) Huang -- Template-Based Controller Synthesis for Timed Systems / Bernd Finkbeiner and Hans-Jörg Peter -- Zeno: An Automated Prover for Properties of Recursive Data Structures / William Sonnex, Sophia Drossopoulou and Susan Eisenbach -- A Proof Assistant for Alloy Specifications / Mattias Ulbrich, Ulrich Geilmann, Aboubakr Achraf El Ghazi and Mana Taghdiri -- Reachability under Contextual Locking / Rohit Chadha, P. Madhusudan and Mahesh Viswanathan -- Bounded Phase Analysis of Message-Passing Programs / Ahmed Bouajjani and Michael Emmi -- Demonstrating Learning of Register Automata / Maik Merten, Falk Howar, Bernhard Steffen, Sofia Cassel and Bengt Jonsson -- Symbolic Automata: The Toolkit / Margus Veanes and Nikolaj Bjørner -- McScM: A General Framework for the Verification of Communicating Machines / Alexander Heußner, Tristan Le Gall and Grégoire Sutre -- SLMC: A Tool for Model Checking Concurrent Systems against Dynamical Spatial Logic Specifications / Luís Caires and Hugo Torres Vieira -- TAPAAL 2.0: Integrated Development Environment for Timed-Arc Petri Nets / Alexandre David, Lasse Jacobsen, Morten Jacobsen, Kenneth Yrke Jørgensen and Mikael H. Møller, et al. -- A Platform for High Performance Statistical Model Checking -- PLASMA / Cyrille Jegourel, Axel Legay and Sean Sedwards |
|
Competition on Software Verification / (SV-COMP) / Dirk Beyer -- Predicate Analysis with BLAST 2.7 / (Competition Contribution) / Pavel Shved, Mikhail Mandrykin and Vadim Mutilin -- CPAchecker with Adjustable Predicate Analysis / (Competition Contribution) / Stefan Löwe and Philipp Wendler -- Block Abstraction Memoization for CPAchecker / (Competition Contribution) / Daniel Wonisch -- Context-Bounded Model Checking with ESBMC 1.17 / (Competition Contribution) / Lucas Cordeiro, Jeremy Morse, Denis Nicole and Bernd Fischer -- Proving Reachability Using FShell / (Competition Contribution) / Andreas Holzer, Daniel Kroening, Christian Schallhart, Michael Tautschnig and Helmut Veith -- LLBMC: A Bounded Model Checker for LLVM's Intermediate Representation / (Competition Contribution) / Carsten Sinz, Florian Merz and Stephan Falke -- Predator: A Verification Tool for Programs with Dynamic Linked Data Structures / (Competition Contribution) / Kamil Dudka, Petr Müller, Petr Peringer and Tomáš Vojnar -- HSF(C): A Software Verifier Based on Horn Clauses / (Competition Contribution) / Sergey Grebenshchikov, Ashutosh Gupta, Nuno P. Lopes, Corneliu Popeea and Andrey Rybalchenko -- satabs: A Bit-Precise Verifier for C Programs / (Competition Contribution) / Gérard Basler, Alastair Donaldson, Alexander Kaiser, Daniel Kroening and Michael Tautschnig, et al. -- Wolverine: Battling Bugs with Interpolants / (Competition Contribution) / Georg Weissenbacher, Daniel Kroening and Sharad Malik |
| Summary |
Annotation 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 |
| Analysis |
Computer science |
|
Computer Communication Networks |
|
Software engineering |
|
Logic design |
|
Artificial intelligence |
|
Logics and Meanings of Programs |
|
Programming Languages, Compilers, Interpreters |
|
Artificial Intelligence (incl. Robotics) |
|
Programming Techniques |
|
computerwetenschappen |
|
computer sciences |
|
programmeertalen |
|
programming languages |
|
programmeren |
|
programming |
|
computernetwerken |
|
computer networks |
|
kunstmatige intelligentie |
|
Information and Communication Technology (General) |
|
Informatie- en communicatietechnologie (algemeen) |
| Bibliography |
Includes bibliographical references and author index |
| Notes |
Online resource; title from PDF title page (SpringerLink, viewed October 27, 2014) |
| In |
Springer eBooks |
| Subject |
System design -- Congresses
|
|
System analysis -- Congresses
|
|
Artificial intelligence.
|
|
Electronic Data Processing
|
|
Artificial Intelligence
|
|
artificial intelligence.
|
|
Informatique.
|
|
System analysis
|
|
System design
|
| Genre/Form |
proceedings (reports)
|
|
Conference papers and proceedings
|
|
Conference papers and proceedings.
|
|
Actes de congrès.
|
| Form |
Electronic book
|
| Author |
Flanagan, Cormac
|
|
König, Barbara (Professor of Information Engineering)
|
|
ETAPS (Conference) (2012 : Tallinn, Estonia)
|
| ISBN |
9783642287565 |
|
3642287565 |
|
