product iamge

Tools and Algorithms for the Construction and Analysis of Systems: 10th International Conference, TACAS 2004, Held as Part of the Joint European Conferences on Theory and Practice of Software, ETAPS 2004, Barcelona, Spain, March 29 - April 2, 2004. Proceedings

This document was uploaded by one of our users. The uploader already confirmed that they had the permission to publish it. If you are author/publisher or own the copyright of this documents, please report to us by using this DMCA report form.

Download
Search on Amazon

Simply click on the Download Book button.

Yes, Book downloads on Ebookily are 100% Free.

Sometimes the book is free on Amazon As well, so go ahead and hit "Search on Amazon"

This volume contains the proceedings of the 10th International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS 2004). TACAS 2004 took place in Barcelona, Spain, from March 29th to April 2nd, as part of the 7th European Joint Conferences on Theory and Practice of Software (ETAPS 2004), whose aims, organization, and history are detailed in a foreword by the ETAPS Steering Committee Chair, Jos´ e Luiz Fiadeiro. TACAS is a forum for researchers, developers, and users interested in ri- rously based tools for the construction and analysis of systems. The conference serves to bridge the gaps between di?erent communities including, but not - mited to, those devoted to formal methods, software and hardware veri?cation, static analysis, programming languages, software engineering, real-time systems, and communication protocols that share common interests in, and techniques for, tool development. In particular, by providing a venue for the discussion of common problems, heuristics, algorithms, data structures, and methodologies, TACAS aims to support researchers in their quest to improve the utility, rel- bility, ?exibility, and e?ciency of tools for building systems. TACASseekstheoreticalpaperswithaclearlinktotoolconstruction,papers describingrelevantalgorithmsandpracticalaspectsoftheirimplementation,- pers giving descriptions of tools and associated methodologies, and case studies with a conceptual message.

Author(s): Shuvendu K. Lahiri, Randal E. Bryant, Amit Goel, Muralidhar Talupur (auth.), Kurt Jensen, Andreas Podelski (eds.)
Series: Lecture Notes in Computer Science 2988
Edition: 1
Publisher: Springer-Verlag Berlin Heidelberg
Year: 2004

Language: English
Pages: 614
Tags: Logics and Meanings of Programs; Software Engineering; Computer Communication Networks; Algorithm Analysis and Problem Complexity

Front Matter....Pages -
Revisiting Positive Equality....Pages 1-15
An Interpolating Theorem Prover....Pages 16-30
Minimal Assignments for Bounded Model Checking....Pages 31-45
Numerical vs. Statistical Probabilistic Model Checking: An Empirical Study....Pages 46-60
Efficient Computation of Time-Bounded Reachability Probabilities in Uniform Continuous-Time Markov Decision Processes....Pages 61-76
Model Checking Discounted Temporal Properties....Pages 77-92
Automatic Creation of Environment Models via Training....Pages 93-107
Error Explanation with Distance Metrics....Pages 108-122
Online Efficient Predictive Safety Analysis of Multithreaded Programs....Pages 123-138
Vooduu: Verification of Object-Oriented Designs Using UPPAAL....Pages 139-143
CoPS – Checker of Persistent Security....Pages 144-152
Tampere Verification Tool....Pages 153-157
SyncGen: An Aspect-Oriented Framework for Synchronization....Pages 158-162
MetaGame: An Animation Tool for Model-Checking Games....Pages 163-167
A Tool for Checking ANSI-C Programs....Pages 168-176
Obtaining Memory-Efficient Reachability Graph Representations Using the Sweep-Line Method....Pages 177-191
Automated Generation of a Progress Measure for the Sweep-Line Method....Pages 192-204
Tarjan’s Algorithm Makes On-the-Fly LTL Verification More Efficient....Pages 205-219
Resource-Optimal Scheduling Using Priced Timed Automata....Pages 220-235
Decidable and Undecidable Problems in Schedulability Analysis Using Timed Automata....Pages 236-250
The Succinct Solver Suite....Pages 251-265
Binding-Time Analysis for MetaML via Type Inference and Constraint Solving....Pages 266-279
A Class of Polynomially Solvable Range Constraints for Interval Analysis without Widenings and Narrowings....Pages 280-295
A Partial Order Semantics Approach to the Clock Explosion Problem of Timed Automata....Pages 296-311
Lower and Upper Bounds in Zone Based Abstractions of Timed Automata....Pages 312-326
A Scalable Incomplete Test for the Boundedness of UML RT Models....Pages 327-341
Automatic Verification of Time Sensitive Cryptographic Protocols....Pages 342-356
Simulation-Based Verification of Autonomous Controllers via Livingstone PathFinder....Pages 357-371
Automatic Parametric Verification of a Root Contention Protocol Based on Abstract State Machines and First Order Timed Logic....Pages 372-387
Refining Approximations in Software Predicate Abstraction....Pages 388-403
Checking Strong Specifications Using an Extensible Software Model Checking Framework....Pages 404-420
Applying Game Semantics to Compositional Software Modeling and Verification....Pages 421-435
Solving Disjunctive/Conjunctive Boolean Equation Systems with Alternating Fixed Points....Pages 436-450
How Vacuous Is Vacuous?....Pages 451-466
A Temporal Logic of Nested Calls and Returns....Pages 467-481
Liveness with Incomprehensible Ranking....Pages 482-496
Guided Invariant Model Checking Based on Abstraction and Symbolic Pattern Databases....Pages 497-511
Numeric Domains with Summarized Dimensions....Pages 512-529
Symbolically Computing Most-Precise Abstract Operations for Shape Analysis....Pages 530-545
Monotonic Abstraction-Refinement for CTL....Pages 546-560
Omega-Regular Model Checking....Pages 561-575
FASTer Acceleration of Counter Automata in Practice....Pages 576-590
From Complementation to Certification....Pages 591-606
Back Matter....Pages -