Limit search to available items
Book Cover
Author TACAS (Conference) (19th : 2013 : Rome, Italy)

Title Tools and algorithms for the construction and analysis of systems : 19th International Conference, TACAS 2013, held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2013, Rome, Italy, March 16-24, 2013. Proceedings / Nir Piterman, Scott A. Smolka (eds.)
Published Berlin ; New York : Springer, [2013]
Online access available from:
Springer eBooks    View Resource Record  


Description 1 online resource
Series Lecture notes in computer science, 0302-9743 ; 7795
LNCS sublibrary. SL 1, Theoretical computer science and general issues
Lecture notes in computer science ; 7795
LNCS sublibrary. SL 1, Theoretical computer science and general issues.
Contents Markov Chains -- On-the-Fly Exact Computation of Bisimilarity Distances / Giorgio Bacci, Giovanni Bacci, Kim G. Larsen, Radu Mardare -- The Quest for Minimal Quotients for Probabilistic Automata / Christian Eisentraut, Holger Hermanns, Johann Schuster, Andrea Turrini, Lijun Zhang -- LTL Model Checking of Interval Markov Chains / Michael Benedikt, Rastislav Lenhardt, James Worrell -- Termination -- Ramsey vs. Lexicographic Termination Proving / Byron Cook, Abigail See, Florian Zuleger -- Structural Counter Abstraction / Kshitij Bansal, Eric Koskinen, Thomas Wies, Damien Zufferey -- Quantifier Elimination -- Extending Quantifier Elimination to Linear Inequalities on Bit-Vectors / Ajith K. John, Supratik Chakraborty -- SAT/SMT -- The MathSAT5 SMT Solver / Alessandro Cimatti, Alberto Griggio, Bastiaan Joost Schaafsma, Roberto Sebastiani -- Formula Preprocessing in MUS Extraction / Anton Belov, Matti Järvisalo, Joao Marques-Silva -- Proof Tree Preserving Interpolation / Jürgen Christ, Jochen Hoenicke, Alexander Nutz -- Asynchronous Multi-core Incremental SAT Solving / Siert Wieringa, Keijo Heljanko
Games and Synthesis -- Model-Checking Iterated Games / Chung-Hao Huang, Sven Schewe, Farn Wang -- Synthesis from LTL Specifications with Mean-Payoff Objectives / Aaron Bohy, Véronique Bruyère, Emmanuel Filiot, Jean-François Raskin -- PRISM-games: A Model Checker for Stochastic Multi-Player Games / Taolue Chen, Vojtěch Forejt, Marta Kwiatkowska, David Parker, Aistis Simaitis -- Process Algebra -- PIC2LNT: Model Transformation for Model Checking an Applied Pi-Calculus / Radu Mateescu, Gwen Salaün -- An Overview of the mCRL2 Toolset and Its Recent Advances / Sjoerd Cranen, Jan Friso Groote, Jeroen J.A. Keiren, Frank P.M. Stappers -- Pushdown Systems Boolean/Integer Programs -- Analysis of Boolean Programs / Patrice Godefroid, Mihalis Yannakakis -- Weighted Pushdown Systems with Indexed Weight Domains / Yasuhiko Minamide -- Underapproximation of Procedure Summaries for Integer Programs / Pierre Ganty, Radu Iosif, Filip Konečný -- Runtime Verification and Model Checking -- Runtime Verification Based on Register Automata / Radu Grigore, Dino Distefano, Rasmus Lerchedahl Petersen, Nikos Tzevelekos
Unbounded Model-Checking with Interpolation for Regular Language Constraints / Graeme Gange, Jorge A. Navas, Peter J. Stuckey, Harald Søndergaard, Peter Schachte -- eVolCheck: Incremental Upgrade Checker for C / Grigory Fedyukovich, Ondrej Sery, Natasha Sharygina -- Intertwined Forward-Backward Reachability Analysis Using Interpolants / Yakir Vizel, Orna Grumberg, Sharon Shoham -- Concurrency -- An Integrated Specification and Verification Technique for Highly Concurrent Data Structures / Parosh Aziz Abdulla, Frédéric Haziza, Lukáš Holík, Bengt Jonsson, Ahmed Rezine -- A Verification-Based Approach to Memory Fence Insertion in PSO Memory Systems / Alexander Linden, Pierre Wolper -- Learning and Abduction -- Identifying Dynamic Data Structures by Learning Evolving Patterns in Memory / David H. White, Gerald Lüttgen -- Synthesis of Circular Compositional Program Proofs via Abduction / Boyang Li, Isil Dillig, Thomas Dillig, Ken McMillan, Mooly Sagiv -- Timed Automata -- As Soon as Probable: Optimal Scheduling under Stochastic Uncertainty / Jean-François Kempf, Marius Bozga, Oded Maler
Integer Parameter Synthesis for Timed Automata / Aleksandra Jovanović, Didier Lime, Olivier H. Roux -- Security and Access Control -- LTL Model-Checking for Malware Detection / Fu Song, Tayssir Touili -- Policy Analysis for Self-administrated Role-Based Access Control / Anna Lisa Ferrara, P. Madhusudan, Gennaro Parlato -- Model Checking Agent Knowledge in Dynamic Access Control Policies / Masoud Koleini, Eike Ritter, Mark Ryan -- Frontiers (Graphics and Quantum) -- Automatic Testing of Real-Time Graphics Systems / Robert Nagy, Gerardo Schneider, Aram Timofeitchik -- Equivalence Checking of Quantum Protocols / Ebrahim Ardeshir-Larijani, Simon J. Gay, Rajagopal Nagarajan -- Functional Programs and Types -- Encoding Monomorphic and Polymorphic Types / Jasmin Christian Blanchette, Sascha Böhme, Andrei Popescu, Nicholas Smallbone -- Deriving Probability Density Functions from Probabilistic Functional Programs / Sooraj Bhat, Johannes Borgström, Andrew D. Gordon, Claudio Russo -- Tool Demonstrations
Polyglot: Systematic Analysis for Multiple Statechart Formalisms / Daniel Balasubramanian, Corina S. Păsăreanu, Gábor Karsai, Michael R. Lowry -- Memorax, a Precise and Sound Tool for Automatic Fence Insertion under TSO / Parosh Aziz Abdulla, Mohamed Faouzi Atig, Yu-Fang Chen, Carl Leonardsson, Ahmed Rezine -- BULL: A Library for Learning Algorithms of Boolean Functions / Yu-Fang Chen, Bow-Yaw Wang -- AppGuard -- Enforcing User Requirements on Android Apps / Michael Backes, Sebastian Gerling, Christian Hammer, Matteo Maffei -- Explicit-State Model Checking -- Model Checking Database Applications / Milos Gligoric, Rupak Majumdar -- Efficient Property Preservation Checking of Model Refinements / Anton Wijs, Luc Engelen -- Büchi Automata -- Strength-Based Decomposition of the Property Büchi Automaton for Faster Model Checking / Etienne Renault, Alexandre Duret-Lutz, Fabrice Kordon, Denis Poitrenaud -- Competition on Software Verification -- Second Competition on Software Verification / Dirk Beyer
CPAchecker with Explicit-Value Analysis Based on CEGAR and Interpolation / Stefan Löwe -- CPAchecker with Sequential Combination of Explicit-State Analysis and Predicate Analysis / Philipp Wendler -- CSeq: A Sequentialization Tool for C / Bernd Fischer, Omar Inverso, Gennaro Parlato -- Handling Unbounded Loops with ESBMC 1.20 / Jeremy Morse, Lucas Cordeiro, Denis Nicole, Bernd Fischer -- LLBMC: Improved Bounded Model Checking of C Programs Using LLVM / Stephan Falke, Florian Merz, Carsten Sinz -- Predator: A Tool for Verification of Low-Level List Manipulation / Kamil Dudka, Petr Müller, Petr Peringer, Tomáš Vojnar -- Symbiotic: Synergy of Instrumentation, Slicing, and Symbolic Execution / Jiri Slaby, Jan Strejček, Marek Trtík -- Threader: A Verifier for Multi-threaded Programs / Corneliu Popeea, Andrey Rybalchenko -- UFO: Verification with Interpolants and Abstract Interpretation / Aws Albarghouthi, Arie Gurfinkel, Yi Li, Sagar Chaki, Marsha Chechik -- Ultimate Automizer with SMTInterpol / Matthias Heizmann, Jürgen Christ, Daniel Dietsch, Evren Ermis, Jochen Hoenicke
Summary This book constitutes the proceedings of the 19th International Conference on Tools and Algorithms for the Construction and Analysis of Systems, TACAS 2013, held in Rome, Italy, in March 2013. The 42 papers presented in this volume were carefully reviewed and selected from 172 submissions. They are organized in topical sections named: Markov chains; termination; SAT/SMT; games and synthesis; process algebra; pushdown; runtime verification and model checking; concurrency; learning and abduction; timed automata; security and access control; frontiers (graphics and quantum); functional programs and types; tool demonstrations; explicit-state model checking; Büchi automata; and competition on software verification
Analysis Computer science
Software engineering
Computer software
Logic design
Logics and Meanings of Programs
Algorithm Analysis and Problem Complexity
Programming Languages, Compilers, Interpreters
Notes International conference proceedings
Bibliography Includes bibliographical references and author index
Subject System design -- Congresses.
Computer software -- Verification -- Congresses.
System analysis -- Congresses.
Computer Systems.
Software Validation.
Systems Analysis.
Genre/Form Conference papers and proceedings.
Computer software.
Conference papers and proceedings.
Form Electronic book
Author Piterman, Nir.
Smolka, Scott A.
ETAPS (Conference) (16th : 2013 : Rome, Italy)
ISBN 9783642367427 (electronic bk.)
3642367429 (electronic bk.)
3642367410 (print)
9783642367410 (print)
Other Titles TACAS 2013
ETAPS 2013