Automated Technology for Verification and Analysis : 7th International Symposium, ATVA 2009, Macao, China, October 14-16, 2009, Proceedings / edited by Zhiming Liu, Anders P. Ravn.

Format:

Book

Contributor:

Liu, Zhiming, 1961- editor.

Ravn, Anders P., editor.

SpringerLink (Online service)

Series:

Computer Science (Springer-11645)

LNCS sublibrary. Programming and software engineering ; SL 2, 5799.

Programming and Software Engineering ; 5799

Language:

English

Subjects (All):

Computers.

Computer programming.

Programming languages (Electronic computers).

Computer logic.

Logic, Symbolic and mathematical.

Algorithms.

Theory of Computation.

Programming Techniques.

Programming Languages, Compilers, Interpreters.

Logics and Meanings of Programs.

Mathematical Logic and Formal Languages.

Algorithm Analysis and Problem Complexity.

Local Subjects:

Theory of Computation.

Programming Techniques.

Programming Languages, Compilers, Interpreters.

Logics and Meanings of Programs.

Mathematical Logic and Formal Languages.

Algorithm Analysis and Problem Complexity.

Physical Description:

1 online resource (XI, 414 pages).

Edition:

First edition 2009.

Contained In:

Springer eBooks

Place of Publication:

Berlin, Heidelberg : Springer Berlin Heidelberg : Imprint: Springer, 2009.

System Details:

text file PDF

Summary:

This book constitutes the proceedings of the 7th International Symposium on Automated Technology for Verification and Analysis, ATVA 2009, held in Macao, China, in October 2009. The 23 regular papers and 3 took papers presented together with 3 invited talks, were carefully reviewed and selected from 74 research papers and 10 tool papers submissions. The papers are organized in topical sections on state space reduction, tools, probabilistic systems, medley, temporal logic, abstraction and refinement, and fault tolerant systems.

Contents:

Invited Talks

Verifying VLSI Circuits

3-Valued Abstraction for (Bounded) Model Checking

Local Search in Model Checking

State Space Reduction

Exploring the Scope for Partial Order Reduction

State Space Reduction of Linear Processes Using Control Flow Reconstruction

A Data Symmetry Reduction Technique for Temporal-epistemic Logic

Tools

TAPAAL: Editor, Simulator and Verifier of Timed-Arc Petri Nets

CLAN: A Tool for Contract Analysis and Conflict Discovery

UnitCheck: Unit Testing and Model Checking Combined

Probabilistic Systems

LTL Model Checking of Time-Inhomogeneous Markov Chains

Statistical Model Checking Using Perfect Simulation

Quantitative Analysis under Fairness Constraints

A Decompositional Proof Scheme for Automated Convergence Proofs of Stochastic Hybrid Systems

Medley

Memory Usage Verification Using Hip/Sleek

Solving Parity Games in Practice

Automated Analysis of Data-Dependent Programs with Dynamic Memory

Temporal Logic I

On-the-fly Emptiness Check of Transition-Based Streett Automata

On Minimal Odd Rankings for Büchi Complementation

Specification Languages for Stutter-Invariant Regular Properties

Abstraction and Refinement

Incremental False Path Elimination for Static Software Analysis

A Framework for Compositional Verification of Multi-valued Systems via Abstraction-Refinement

Don't Know for Multi-valued Systems

Logahedra: A New Weakly Relational Domain

Fault Tolerant Systems

Synthesis of Fault-Tolerant Distributed Systems

Formal Verification for High-Assurance Behavioral Synthesis

Dynamic Observers for the Synthesis of Opaque Systems

Temporal Logic II

Symbolic CTL Model Checking of Asynchronous Systems Using Constrained Saturation

LTL Model Checking for Recursive Programs

On Detecting Regular Predicates in Distributed Systems.

Other Format:

Printed edition:

ISBN:

978-3-642-04761-9

9783642047619

Access Restriction:

Restricted for use by site license.