Tools and Algorithms for the Construction and Analysis of Systems: 9th International Conference, TACAS 2003, Held as Part of the Joint European Conferences on Theory and Practice of Software, ETAPS 2003, Warsaw, Poland, April 7-11, 2003, Proceedings
Hubert Garavel, John Hatcliff
Springer, May 7, 2003 - System design - 604 pages
This book constitutes the refereed proceedings of the 9th International Conference on Tools and Algorithms for the Construction and Analysis of Systems, TACAS 2003, held in Warsaw, Poland, in April 2003. The 43 revised full papers presented were carefully reviewed and selected from 160 submissions. The papers are organized in topical sections on bounded model checking and SAT-based methods, mu-calculus and temporal logics, verification of parameterized systems, abstractions and counterexamples, real-time and scheduling, security and cryptography, modules and compositional verification, symbolic state spaces and decision diagrams, performance and mobility, state space reductions, constraint solving and decision procedures, and testing and verification.
What people are saying - Write a review
We haven't found any reviews in the usual places.
Bounded Model Checking for Past LTL
Experimental Analysis of Different Techniques for Bounded Model
37 other sections not shown
Other editions - View all
abstract model action algorithm analysis applied approach automata automaton BDD-based behavior benchmarks bisimulation boolean bounded model checking cache cache coherence checker clock components composition Computer Science constraints construction corresponding counterexample cryptographic protocols decision procedure defined Definition denote E.M. Clarke encoding equations equivalent example EXPTIME finite formal formal verification formula framework function given global hybrid systems i-calculus implementation infinite initial input instance integer invariant iteration Kripke structure labeled language Lemma linear LNCS M-net messages method model checking module multiset nodes NuSMV operators optimal output parameterized path performance Petri nets predicates problem Proc proof protocol PSPACE reachable reduction refinement represent rule safety properties SAT solver satisfies scheduling semantics sequence number Software specification spi calculus Springer-Verlag state-space strategy structure successor symbolic model TACAS task techniques temporal logic Theorem tool transition relation tuple variables vector verification