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 / edited by Nir Piterman, Scott Smolka.

Format:

Book

Contributor:

Piterman, Nir, editor.

Smolka, Scott, editor.

SpringerLink (Online service)

Series:

Computer Science (Springer-11645)

LNCS sublibrary. Theoretical computer science and general issues ; SL 1, 7795.

Theoretical Computer Science and General Issues ; 7795

Language:

English

Subjects (All):

Computer logic.

Software engineering.

Algorithms.

Programming languages (Electronic computers).

Logics and Meanings of Programs.

Software Engineering.

Algorithm Analysis and Problem Complexity.

Programming Languages, Compilers, Interpreters.

Local Subjects:

Logics and Meanings of Programs.

Software Engineering.

Algorithm Analysis and Problem Complexity.

Programming Languages, Compilers, Interpreters.

Physical Description:

1 online resource (XXIV, 646 pages) : 137 illustrations.

Edition:

First edition 2013.

Contained In:

Springer eBooks

Place of Publication:

Berlin, Heidelberg : Springer Berlin Heidelberg : Imprint: Springer, 2013.

System Details:

text file PDF

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.

Contents:

On-the-Fly Exact Computation of Bisimilarity Distances

The Quest for Minimal Quotients for Probabilistic Automata

LTL Model Checking of Interval Markov Chains

Ramsey vs. Lexicographic Termination Proving

Structural Counter Abstraction

Extending Quantifier Elimination to Linear Inequalities on Bit-Vectors

The MathSAT5 SMT Solver

Formula Preprocessing in MUS Extraction

Proof Tree Preserving Interpolation

Asynchronous Multi-core Incremental SAT Solving

Model-Checking Iterated Games

PRISM-games: A Model Checker for Stochastic Multi-Player Games

PIC2LNT: Model Transformation for Model Checking an Applied Pi-Calculus

An Overview of the mCRL2 Toolset and Its Recent Advances

Analysis of Boolean Programs

Weighted Pushdown Systems with Indexed Weight Domains

Underapproximation of Procedure Summaries for Integer Programs

Runtime Verification Based on Register Automata

Unbounded Model-Checking with Interpolation for Regular Language Constraints

eVolCheck: Incremental Upgrade Checker for C

Intertwined Forward-Backward Reachability Analysis Using Interpolants

An Integrated Specification and Verification Technique or Highly Concurrent Data Structures

A Verification-Based Approach to Memory Fence Insertion in PSO Memory Systems

Identifying Dynamic Data Structures by Learning Evolving Patterns in Memory

Synthesis of Circular Compositional Program Proofs via Abduction

As Soon as Probable: Optimal Scheduling under Stochastic Uncertainty

Integer Parameter Synthesis for Timed Automata

LTL Model-Checking for Malware Detection

Policy Analysis for Self-administrated Role-Based Access Control

Model Checking Agent Knowledge in Dynamic Access Control Policies

Frontiers (Graphics and Quantum) Automatic Testing of Real-Time Graphics Systems

Equivalence Checking of Quantum Protocols

Encoding Monomorphic and Polymorphic Types

Deriving Probability Density Functions from Probabilistic Functional Programs

Tool Demonstrations Polyglot: Systematic Analysis for Multiple Statechart Formalisms

Memorax, a Precise and Sound Tool for Automatic Fence Insertion under TSO

BULL: A Library for Learning Algorithms of Boolean Functions

AppGuard - Enforcing User Requirements on Android Apps

Model Checking Database Applications

Efficient Property Preservation Checking of Model Refinements

Strength-Based Decomposition of the Property Büchi Automaton for Faster Model Checking

Competition on Software Verification Second Competition on Software Verification (Summary of SV-COMP 2013)

CPAchecker with Explicit-Value Analysis Based on CEGAR and Interpolation (Competition Contribution)

CPAchecker with Sequential Combination of Explicit-State Analysis and Predicate Analysis (Competition Contribution)

CSeq: A Sequentialization Tool for C (Competition Contribution)

Handling Unbounded Loops with ESBMC 1.20 (Competition Contribution)

LLBMC: Improved Bounded Model Checking of C Programs Using LLVM (Competition Contribution)

Predator: A Tool for Verification of Low-Level List Manipulation (Competition Contribution)

Symbiotic: Synergy of Instrumentation, Slicing, and Symbolic Execution (Competition Contribution)

Threader: A Verifier for Multi-threaded Programs (Competition Contribution)

UFO: Verification with Interpolants and Abstract Interpretation (Competition Contribution)

Ultimate Automizer with SMTInterpol (Competition Contribution).

Other Format:

Printed edition:

ISBN:

978-3-642-36742-7

9783642367427

Access Restriction:

Restricted for use by site license.