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.
Author(s): Joseph Sifakis (auth.), Javier Esparza, Rupak Majumdar (eds.)
Series: Lecture Notes in Computer Science 6015 : Theoretical Computer Science and General Issues
Edition: 1
Publisher: Springer-Verlag Berlin Heidelberg
Year: 2010
Language: English
Commentary: Correct bookmarks, cover, pagination
Pages: 468
Tags: Software Engineering; Logics and Meanings of Programs; Computer Communication Networks; Programming Languages, Compilers, Interpreters; Artificial Intelligence (incl. Robotics); Programming Techniques
Front Matter....Pages -
Embedded Systems Design — Scientific Challenges and Work Directions....Pages 1-1
Antichain Algorithms for Finite Automata....Pages 2-22
Assume-Guarantee Verification for Probabilistic Systems....Pages 23-37
Simple O ( m log n ) Time Markov Chain Lumping....Pages 38-52
Model Checking Interactive Markov Chains....Pages 53-68
Approximating the Pareto Front of Multi-criteria Optimization Problems....Pages 69-83
An Alternative to SAT-Based Approaches for Bit-Vectors....Pages 84-98
Satisfiability Modulo the Theory of Costs: Foundations and Applications....Pages 99-113
Optimal Tableau Algorithms for Coalgebraic Logics....Pages 114-128
Blocked Clause Elimination....Pages 129-144
Boom : Taking Boolean Program Model Checking One Step Further....Pages 145-149
The OpenSMT Solver....Pages 150-153
Stranger : An Automata-Based String Analysis Tool for PHP....Pages 154-157
When Simulation Meets Antichains....Pages 158-174
On Weak Modal Compatibility, Refinement, and the MIO Workbench....Pages 175-189
Rational Synthesis....Pages 190-204
Efficient Büchi Universality Checking....Pages 205-220
Automated Termination Analysis for Programs with Second-Order Recursion....Pages 221-235
Ranking Function Synthesis for Bit-Vector Relations....Pages 236-250
Fairness for Dynamic Control....Pages 251-265
JTorX: A Tool for On-Line Model-Driven Test Derivation and Execution....Pages 266-270
SLAB: A Certifying Model Checker for Infinite-State Concurrent Systems....Pages 271-274
Tracking Heaps That Hop with Heap-Hop....Pages 275-279
Automatic Analysis of Scratch-Pad Memory Code for Heterogeneous Multicore Processors....Pages 280-295
Simplifying Linearizability Proofs with Reduction and Abstraction....Pages 296-311
A Polymorphic Intermediate Verification Language: Design and Logical Encoding....Pages 312-327
Trace-Based Symbolic Analysis for Atomicity Violations....Pages 328-342
ACS: Automatic Converter Synthesis for SoC Bus Protocols....Pages 343-348
AlPiNA: An Algebraic Petri Net Analyzer....Pages 349-352
PASS : Abstraction Refinement for Infinite Probabilistic Models....Pages 353-357
Arrival Curves for Real-Time Calculus: The Causality Problem and Its Solutions....Pages 358-372
Computing the Leakage of Information-Hiding Systems....Pages 373-389
Statistical Measurement of Information Leakage....Pages 390-404
SAT Based Bounded Model Checking with Partial Order Semantics for Timed Automata....Pages 405-419
Preemption Sealing for Efficient Concurrency Testing....Pages 420-434
Code Mutation in Verification and Automatic Code Correction....Pages 435-450
Efficient Detection of Errors in Java Components Using Random Environment and Restarts....Pages 451-465
Back Matter....Pages -
