9. CAV 1997:
Haifa,
Israel
Orna Grumberg (Ed.):
Computer Aided Verification, 9th International Conference, CAV '97, Haifa, Israel, June 22-25, 1997, Proceedings.
Lecture Notes in Computer Science 1254 Springer 1997, ISBN 3-540-63166-6 BibTeX
@proceedings{DBLP:conf/cav/1997,
editor = {Orna Grumberg},
title = {Computer Aided Verification, 9th International Conference, CAV
'97, Haifa, Israel, June 22-25, 1997, Proceedings},
booktitle = {CAV},
publisher = {Springer},
series = {Lecture Notes in Computer Science},
volume = {1254},
year = {1997},
isbn = {3-540-63166-6},
bibsource = {DBLP, http://dblp.uni-trier.de}
}
- F. Erich Marschner:
Practical Challenges for Industrial Formal Verification Tools.
1-2 BibTeX
- Roger B. Hughes:
Formal Verification of Digital Systems, from ASICs to HW/SW Codesign - a Pragmatic Approach.
3-6 BibTeX
- Arne Borälv:
The Industrial Success of Verification Tools Based on Stålmarck's Method.
7-10 BibTeX
- Martin Rowe:
Formal Verification - Applications & Case Studies.
11 BibTeX
- Abelardo Pardo, Gary D. Hachtel:
Automatic Abstraction Techniques for Propositional µ-calculus Model Checking.
12-23 BibTeX
- Kenneth L. McMillan:
A Compositional Rule for Hardware Design Refinement.
24-35 BibTeX
- Orna Kupferman, Moshe Y. Vardi:
Model Checking Revisited.
36-47 BibTeX
- Roope Kaivola:
Using Compositional Preorders in the Verification of Sliding Window Protocal.
48-59 BibTeX
- David Cyrluk, M. Oliver Möller, Harald Rueß:
An Efficient Decision Procedure for the Theory of Fixed-Sized Bit-Vectors.
60-71 BibTeX
- Susanne Graf, Hassen Saïdi:
Construction of Abstract State Graphs with PVS.
72-83 BibTeX
- Adam L. Turk, Scott T. Probst, Gary J. Powers:
Verification of a Chemical Process Leak Test Procedure.
84-94 BibTeX
- Gila Kamhi, Osnat Weissberg, Limor Fix:
Automatic Datapath Extraction for Efficient Usage of HDD.
95-106 BibTeX
- Nils Klarlund:
An n log n Algorithm for Online BDD Refinement.
107-118 BibTeX
- Christel Baier, Holger Hermanns:
Weak Bisimulation for Fully Probabilistic Processes.
119-130 BibTeX
- Dominique Bolignano:
Towards a Mechanization of Cryptographic Protocal Verification.
131-142 BibTeX
- Y. S. Ramakrishna, C. R. Ramakrishnan, I. V. Ramakrishnan, Scott A. Smolka, Terrance Swift, David Scott Warren:
Efficient Model Checking Using Tabled Resolution.
143-154 BibTeX
- Kathi Fisler:
Containing of Regular Languages in Non-Regular Timing Diagram Languages is Decidable.
155-166 BibTeX
- Bernard Boigelot, Louis Bronne, Stéphane Rassart:
An Improved Reachability Analysis Method for Strongly Linear Hybrid Systems (Extended Abstract).
167-178 BibTeX
- Marius Bozga, Oded Maler, Amir Pnueli, Sergio Yovine:
Some Progress in the Symbolic Verification of Timed Automata.
179-190 BibTeX
- Serdar Tasiran, Robert K. Brayton:
STARI: A Case Study in Compositional and Hierarchical Timing Verification.
191-201 BibTeX
- Alessandro Cimatti, Fausto Giunchiglia, Paolo Pecchiari, Bruno Pietra, Joe Profeta, Dario Romano, Paolo Traverso, Bing Yu:
A Provably Correct Embedded Verifier for the Certification of Safety Critical Software.
202-213 BibTeX
- Geoff Barrett, Anthony McIsaac:
Model Checking in a Microprocessor Design Project.
214-225 BibTeX
- David Harel:
Some Thoughts on Statecharts, 13 Years Later.
226-231 BibTeX
- Viktor Gyuris, A. Prasad Sistla:
On-the-Fly Model Checking Under Fairness That Exploits Symmetry.
232-243 BibTeX
- Manish Pandey, Randal E. Bryant:
Exploiting Symmetry When Verifying Transitor-Level Circuits by Symbolic Trajectory Evaluation.
244-255 BibTeX
- Ulrich Stern, David L. Dill:
Parallelizing the Murphi Verifier.
256-278 BibTeX
- Ilan Beer, Shoham Ben-David, Cindy Eisner, Yoav Rodeh:
Efficient Detection of Vacuity in ACTL Formulaas.
279-290 BibTeX
- Neil Immerman, Moshe Y. Vardi:
Model Checking and Transitive-Closure Logic.
291-302 BibTeX
- Gérard Berry:
Boolean and 2-adic Numbers Based Techniques for Verifying Synchronous Design.
303 BibTeX
- Gérard Cécé, Alain Finkel:
Programs with Quasi-Stable Channels are Effectively Recognizable (Extended Abstract).
304-315 BibTeX
- William Chan, Richard J. Anderson, Paul Beame, David Notkin:
Combining Constraint Solving and Symbolic Model Checking for a Class of a Systems with Non-linear Constraints.
316-327 BibTeX
- Ilkka Kokkarinen, Doron Peled, Antti Valmari:
Relaxed Visibility Enhances Partial Order Reduction.
328-339 BibTeX
- Rajeev Alur, Robert K. Brayton, Thomas A. Henzinger, Shaz Qadeer, Sriram K. Rajamani:
Partial-Order Reduction in Symbolic State Space Exploration.
340-351 BibTeX
- Stephan Melzer, Stefan Römer:
Deadlock Checking Using Net Unfoldings.
352-363 BibTeX
- Jun Sawada, Warren A. Hunt Jr.:
Trace Table Based Approach for Pipeline Microprocessor Verification.
364-375 BibTeX
- Jun Yuan, Jian Shen, Jacob A. Abraham, Adnan Aziz:
On Combining Formal and Informal Verification.
376-387 BibTeX
- Miroslav N. Velev, Randal E. Bryant, Alok Jain:
Efficient Modeling of Memory Arrays in Symbolic Simulation.
388-399 BibTeX
- Tevfik Bultan, Richard Gerber, William Pugh:
Symbolic Model Checking of Infinite State Systems Using Presburger Arithmetic.
400-411 BibTeX
- A. Prasad Sistla:
Parametrized Verification of Linear Networks Using Automata as Invariants.
412-423 BibTeX
- Yonit Kesten, Oded Maler, Monica Marcus, Amir Pnueli, Elad Shahar:
Symbolic Model Checking with Rich ssertional Languages.
424-435 BibTeX
Tool Papers
- Hassen Saïdi:
The Invariant Checker: Automated Deductive Verification of Reactive Systems.
436-439 BibTeX
- Bernd Grahlmann:
The PEP Tool.
440-443 BibTeX
- Naomi Lindenstrauss, Yehoshua Sagiv, Alexander Serebrenik:
TermiLog: A System for Checking Termination of Queries to Logic Programs.
444-447 BibTeX
- Peter Kelb, Tiziana Margaria, Michael Mendler, Claudia Gsottberger:
MOSEL: A Sound and Efficient Tool for M2L(Str).
448-451 BibTeX
- Sérgio Vale Aguiar Campos, Edmund M. Clarke, Marius Minea:
The Verus Tool: A Quantitative Approach to the Formal Verification of Real-Time Systems.
452-455 BibTeX
- Kim Guldstrand Larsen, Paul Pettersson, Wang Yi:
UPPAAL: Status & Developments.
456-459 BibTeX
- Thomas A. Henzinger, Pei-Hsin Ho, Howard Wong-Toi:
HYTECH: A Model Checker for Hybrid Systems.
460-463 BibTeX
- A. Prasad Sistla, L. Miliades, Viktor Gyuris:
SMC: A Symmetry Based Model Checker for Verification of Liveness Properties.
464-467 BibTeX
- Armin Biere:
µcke - Efficient µ-Calculus Model Checking.
468-471 BibTeX
- Kimmo Varpaaniemi, Keijo Heljanko, Johan Lilius:
prod 3.2: An Advanced Tool for Efficient Reachability Analysis.
472-475 BibTeX
- Patrice Godefroid:
VeriSoft: A Tool for the Automatic Analysis of Concurrent Reactive Software.
476-479 BibTeX
- Ilan Beer, Shoham Ben-David, Cindy Eisner, Daniel Geist, Leonid Gluhovsky, Tamir Heyman, Avner Landver, P. Paanah, Yoav Rodeh, G. Ronin, Yaron Wolfsthal:
RuleBase: Model Checking at IBM.
480-483 BibTeX
Copyright © Sat May 16 23:00:36 2009
by Michael Ley (ley@uni-trier.de)
