Computer Aided Verification: 7th International Conference, CAV '95, Liege, Belgium, July 3 - 5, 1995. ProceedingsPierre Wolper Springer Science & Business Media, 21/06/1995 - 456 من الصفحات This volume constitutes the proceedings of the 7th International Conference on Computer Aided Verification, CAV '95, held in Liège, Belgium in July 1995. The book contains the 31 refereed full research papers selected for presentation at CAV '95 as well as abstracts or full papers of the three invited presentations. Originally oriented towards finite-state concurrent systems, CAV now covers all styles of verification approaches and a variety of application areas. The papers included range from theoretical issues to concrete applications with a certain emphasis on verification tools and the algorithms and techniques needed for their implementations. Beyond finite-state systems, real-time systems and hybrid systems are an important part of the conference. |
المحتوى
I | 1 |
II | 4 |
III | 16 |
IV | 31 |
V | 42 |
VI | 54 |
IX | 70 |
X | 84 |
XXI | 225 |
XXII | 239 |
XXIII | 253 |
XXIV | 267 |
XXV | 279 |
XXVI | 293 |
XXIX | 309 |
XXX | 325 |
XI | 98 |
XII | 114 |
XIII | 127 |
XIV | 141 |
XV | 142 |
XVI | 155 |
XVII | 166 |
XVIII | 180 |
XIX | 196 |
XX | 211 |
XXXIII | 339 |
XXXV | 353 |
XXXVI | 367 |
XXXVII | 381 |
XXXVIII | 395 |
XXXIX | 409 |
XL | 423 |
XLI | 437 |
طبعات أخرى - عرض جميع المقتطفات
عبارات ومصطلحات مألوفة
abstract algebra algorithm automata behavior binary Binary Decision Diagrams bisimulation Boolean bound Büchi automaton circuits clock translation complexity components Computer Science concurrent condition configuration construction contains corresponding defined definition denote E.M. Clarke edge encoding EQCTL equivalent ESTEREL example existential quantification exists exponential finite-state fixpoint formal formal verification formula function given graph hybrid automaton hybrid systems implementation induction infinite initial input integer invariant Kripke structure labeled language Lemma linear hybrid LNCS Markov processes memory method modal model checking mu-calculus node OBDDs operators output pairs path Petri Petri net player predicate Proc processor proof protocol prove Rabin reachable reactive system relation safety properties satisfies scheduler scsg semantics sequence simple specification Streett symbolic techniques temporal logic Theorem transition relation transition system tree tree automaton unfolding variables verification problem winning strategy
مقاطع مشهورة
الصفحة 450 - Y. Kesten, A. Pnueli, J. Sifakis, and S. Yovine. Integration graphs: a class of decidable hybrid systems.