Tools and Algorithms for the Construction and Analysis of Systems: 14th International Conference, TACAS 2008, Held as Part of the Joint European Conferences on Theory and Practice of Software, ETAPS 2008, Budapest, Hungary, March 29-April 6, 2008, Proceedings

Front Cover
Springer Science & Business Media, Mar 18, 2008 - Computers - 518 pages
ETAPS2008wasthe11thinstanceoftheEuropeanJointConferencesonTheory and Practice of Software. ETAPS is an annual federated conference that was established in 1998 by combining a number of existing and new conferences. This yearit comprised?ve conferences (CC, ESOP, FASE, FOSSACS, TACAS), 22satelliteworkshops(ACCAT, AVIS, Bytecode, CMCS, COCV, DCC, FESCA, FIT, FORMED, GaLoP, GT-VMT, LDTA, MBT, MOMPES, PDMC, QAPL, RV, SafeCert, SC, SLA++P, WGT, andWRLA), ninetutorials, andseveninvited lectures (excluding those that were speci?c to the satellite events). The ?ve main conferences received 571 submissions, 147 of which were accepted, giving an overall acceptance rate of less than 26%, with each conference below 27%. Congratulationsthereforetoallthe authorswhomadeittothe ?nalprogramme! I hope that most of the other authors will still have found a way of participating in this exciting event, and that you will all continue submitting to ETAPS and contributing to make of it the best conference in the area. The events that comprise ETAPS address various aspects of the system - velopment process, including speci?cation, design, implementation, analysis and improvement. The languages, methodologies and tools which support these - tivities are all well within its scope. Di?erent blends of theory and practice are represented, with an inclination towards theory with a practical motivation on the one hand and soundly based practice on the other. Many of the issues involved in software design apply to systems in general, including hardware s- tems, and the emphasis on software is not intended to be exclusive.
 

What people are saying - Write a review

We haven't found any reviews in the usual places.

Contents

Techniques Methodology and Solutions
1
Extending Automated Compositional Verification to the Full Class of OmegaRegular Languages
2
Graph Grammar Modeling and Verification of Ad Hoc Routing Protocols
18
The Environment Abstraction Framework for Model Checking Concurrent Systems
33
Revisiting Resistance Speeds Up IOEfficient LTL Model Checking
48
Alternative Algorithms for LTL Satisfiability and ModelChecking
63
OntheFly Techniques for GameBased Software Model Checking
78
Computing Simulations over Tree Automata Efficient Techniques for Reducing Tree Automata
93
On Verifying Fault Tolerance of Distributed Protocols
315
The RealTime Maude Tool
332
An Efficient SMT Solver
337
Computation and Visualisation of Phase Portraits for Model Checking SPDIs
341
Towards a Research Tool for Omega Automata and Temporal Logic
346
Attacking Path Explosion in ConstraintBased Test Generation
351
DemandDriven Compositional Symbolic Execution
367
Peephole Partial Order Reduction
382

Formal Pervasive Verification of a Paging Mechanism
109
Analyzing Stripped DeviceDriver Executables
124
Model CheckingBased Genetic Programming with an Application to Mutual Exclusion
141
Conditional Probabilities over Probabilistic and Nondeterministic Systems
157
On Automated Verification of Probabilistic Programs
173
Symbolic Model Checking of Hybrid Systems Using Template Polyhedra
188
Fast Directed Model Checking Via Russian Doll Abstraction
203
A SATBased Approach to Size Change Termination with Global Ranking Functions
218
Efficient Automatic STE Refinement Using Responsibility
233
Reasoning Algebraically About PSolvable Loops
249
On Local Reasoning in Verification
265
Interprocedural Analysis of Concurrent Programs Under a Context Bound
282
ContextBounded Analysis of Concurrent Queue Systems
299
Efficient Interpolant Generation in Satisfiability Modulo Theories
397
Quantified Invariant Generation Using an Interpolating Saturation Prover
413
Accelerating InterpolationBased ModelChecking
428
Automatically Refining Abstract Interpretations
443
Symbolic Verification of Symmetric Systems
459
Requirement Synthesis for Compositional Model Checking
463
A Tool for the Analysis of SystemC Models
467
Trusted Source Translation of a Total Function Language
471
RocketFast Proof Checking for SMT Solvers
486
A Reputation System Based on SDSI
501
Author Index
517
Copyright

Other editions - View all

Common terms and phrases

Bibliographic information