Computer Aided Verification: 5th International Conference, CAV'93, Elounda, Greece, June 28 - July 1, 1993. ProceedingsCostas Courcoubetis Springer Science & Business Media, 16/06/1993 - 504 من الصفحات This volume contains the proceedings of the Fifth Conference on Computer-Aided Verfication, held in Crete, Greece, in June/July 1993. The objective of the CAV conferences is to bring together researchers and practitioners interested in the development anduse of methods, tools, and theories for the computer-aided verification of concurrent systems. The conferences provide an opportunity for comparing various verfication methods and tools that can be used to assist the applications designer. Emphasis is placed on new research results and the application of existing methods to real verification problems. The volume contains abstracts of three invited lectures and full versions of 37 contributed papers selected from 84 submissions.The contributions are grouped into sections on hardware verification with BDDs, methods and tools, theorem proving, analysis of real-time systems, process algebras and calculi, partial orders, and exploiting symmetry. |
المحتوى
Logic Synthesis and Design Verification | 1 |
Parametric Circuit Representation Using Inductive Boolean Functions | 15 |
An Iterative Approach to Language Containment | 29 |
Methods and Tools | 59 |
Symbolic Equivalence Checking | 85 |
Modular Vec | 110 |
Automatic Generation of Network Invariants for the Verification of Iterative | 123 |
A Graphical Interval Logic Toolset for Verifying Concurrent Systems | 138 |
An Efficient Algorithm for Minimizing RealTime Transition Systems | 210 |
Verification of Timing Properties of VHDL | 225 |
Timed Modal Specification Theory and Tools | 253 |
Theorem Proving 2 | 268 |
The Formal Verification of an Algorithm for Interactive Consistency Under | 292 |
ComputerAssisted Simulation Proofs | 305 |
A Verifier and Timing Analyser for Simple Imperative | 320 |
Delay Analysis in Synchronous Programs | 333 |
Theorem Proving 1 | 154 |
Computing Accumulated Delays in RealTime Systems | 181 |
Reachability Analysis of Planar MultiLinear Systems | 194 |
Verifying Quantitative RealTime Properties of Synchronous Programs | 346 |
طبعات أخرى - عرض جميع المقتطفات
عبارات ومصطلحات مألوفة
A₁ abstraction actions ACTL algorithm atom automata automaton B₁ bad cycle BDD's behavior Binary Decision Diagrams bisimulation Boolean Boolean functions cell circuit clock component Computer Science concurrent configuration conjunction consider constraints construct contains corresponding CSCC CTL formula cycle sets debugger defined Definition denote dependency described E.M. Clarke equivalence example finite formal verification function given graph hash hash functions IEEE implementation induction infinite initial input interval invariant iterative system Kripke structure L-process labeled language Lemma linear method minimal model checking node Nqthm operations output parameter partition path PC(i Petri nets Piton predicate problem processors proof properties Proposition protocol prove refinement representation represented satisfies semantics sequence set of reachable simulation specification step subset symbolic synchronous techniques temporal logic theorem prover trace transition relation transition systems traversal variables vector VHDL