Tools and Algorithms for the Construction and Analysis of Systems : 16th International Conference, TACAS 2010, Held as Part of the Joint European Conference on Theory and Practice of Software, ETAPS 2010, Paphos, Cyprus, March 20-29, 2010, Proceedings

by Esparza, Javier; Majumdar, Rupak

• ISBN13: 9783642120015
• ISBN10: 3642120016
• Format: Paperback
• Copyright: 2010-04-21
• Publisher: Springer-Verlag New York Inc

Summary

This book constitutes the refereed proceedings of the 16th International Conference on Tools and Algorithms for the Construction and Analysis of Systems, TACAS 2010, held in Paphos, Cyprus, in March 2010, as part of ETAPS 2010, the European Joint Conferences on Theory and Practice of Software.The 35 papers presented were carefully reviewed and selected from 134 submissions. The topics covered are probabilistic systems and optimization, decision procedures, tools, automata theory, liveness, software verification, real time and information flow, and testing.

Table of Contents

Invited Talks
Embedded Systems Design - Scientific Challenges and Work Directions (Abstract)	p. 1
Antichain Algorithms for Finite Automata	p. 2
Probabilistic Systems and Optimization
Assume-Guarantee Verification for Probabilistic Systems	p. 23
Simple O(m log n) Time Markov Chain Lumping	p. 38
Model Checking Interactive Markov Chains	p. 53
Approximating the Pareto Front of Multi-criteria Optimization Problems	p. 69
Decision Procedures
An Alternative to SAT-Based Approaches for Bit-Vectors	p. 84
Satisfiability Modulo the Theory of Costs: Foundations and Applications	p. 99
Optimal Tableau Algorithms for Coalgebraic Logics	p. 114
Blocked Clause Elimination	p. 129
Tools I
BOOM: Taking Boolean Program Model Checking One Step Further	p. 145
The OpenSMT Solver	p. 150
STRANGER: An Automata-Based String Analysis Tool for PHP	p. 154
Automata Theory
When Simulation Meets Antichains: On Checking Language Inclusion of Nondeterministic Finite (Tree) Automata	p. 158
On Weak Modal Compatibility, Refinement, and the MIO Workbench	p. 175
Rational Synthesis	p. 190
Efficient Büchi University Checking	p. 205
Liveness
Automated Termination Analysis for Programs with Second-Order Recursion	p. 221
Ranking Function Synthesis for Bit-Vector Relations	p. 236
Fairness for Dynamic Control	p. 251
Tools II
JTorX: A Tool for On-Line Model-Driven Test Derivation and Execution	p. 266
SLAB: A Certifying Model Checker for Infinite-State Concurrent Systems	p. 271
Tracking Heaps That Hop with Heap-Hop	p. 275
Software Verification
Automatic Analysis of Scratch-Pad Memory Code for Heterogeneous Multicore Processors	p. 280
Simplifying Linearizability Proofs with Reduction and Abstraction	p. 296
A Polymorphic Intermediate Verification Language: Design and Logical Encoding	p. 312
Trace-Based Symbolic Analysis for Atomicity Violations	p. 328
Tools III
ACS: Automatic Converter Synthesis for SoC Bus Protocols	p. 343
AlPiNA: An Algebraic Petri Net Analyzer	p. 349
PASS: Abstraction Refinement for Infinite Probabilistic Models	p. 353
Real Time and Information Flow
Arrival Curves for Real-Time Calculus: The Causality Problem and Its Solutions	p. 358
Computing the Leakage of Information-Hiding Systems	p. 373
Statistical Measurement of Information Leakage	p. 390
SAT Based Bounded Model Checking with Partial Order Semantics for Timed Automata	p. 405
Testing
Preemption Sealing for Efficient Concurrency Testing	p. 420
Code Mutation in Verification and Automatic Code Correction	p. 435
Efficient Detection of Errors in Java Components Using Random Environment and Restarts	p. 451
Author Index	p. 467
Table of Contents provided by Ingram. All Rights Reserved.