10. CAV 1998: Vancouver, BC, Canada
Alan J. Hu, Moshe Y. Vardi (Eds.):
Computer Aided Verification, 10th International Conference, CAV '98, Vancouver, BC, Canada, June 28 - July 2, 1998, Proceedings.
Lecture Notes in Computer Science 1427 Springer 1998, ISBN 3-540-64608-6 BibTeX
Invited Papers
Regular Papers
- Jens U. Skakkebæk, Robert B. Jones, David L. Dill:
Formal Verification of Out-of-Order Execution Using Incremental Flushing.
98-109 BibTeX
- Kenneth L. McMillan:
Verification of an Implementation of Tomasulo's Algorithm by Compositional Model Checking.
110-121 BibTeX
- Ravi Hosabettu, Mandayam K. Srivas, Ganesh Gopalakrishnan:
Decomposing the Proof of Correctness of pipelined Microprocessors.
122-134 BibTeX
- Jun Sawada, Warren A. Hunt Jr.:
Processor Verification with Precise Exeptions and Speculative Execution.
135-146 BibTeX
- Edmund M. Clarke, E. Allen Emerson, Somesh Jha, A. Prasad Sistla:
Symmetry Reductions inModel Checking.
147-158 BibTeX
- Gurmeet Singh Manku, Ramin Hojati, Robert K. Brayton:
Structural Symmetry and Model Checking.
159-171 BibTeX
- Ulrich Stern, David L. Dill:
Using Magnatic Disk Instead of Main Memory in the Murphi Verifier.
172-183 BibTeX
- Ilan Beer, Shoham Ben-David, Avner Landver:
On-the-Fly Model Checking of RCTL Formulas.
184-194 BibTeX
- Thomas A. Henzinger, Orna Kupferman, Shaz Qadeer:
From Pre-historic to Post-modern Symbolic Model Checking.
195-206 BibTeX
- Frank Wallner:
Model Checking LTL Using Net Unforldings.
207-218 BibTeX
- Ying Xu, Eduard Cerny, Xiaoyu Song, Francisco Corella, Otmane Aït Mohamed:
Model Checking for a First-Order Temporal Logic Using Multiway Decision Graphs.
219-231 BibTeX
- Jayram S. Thathachar:
On the Limitations of Ordered Representations of Functions.
232-243 BibTeX
- Anuj Goel, Khurram Sajid, Hai Zhou, Adnan Aziz, Vigyan Singhal:
BDD Based Procedures for a Theory of Equality with Uninterpreted Functions.
244-255 BibTeX
- Adrian J. Isles, Ramin Hojati, Robert K. Brayton:
Computing Reachable Control States of Systems Modeled with Uninterpreted Functions and Infinite Memory.
256-267 BibTeX
- Hubert Comon, Yan Jurski:
Multiple Counters Automata, Safety Analysis and Presburger Arithmetic.
268-279 BibTeX
- Thomas R. Shiple, James H. Kukula, Rajeev K. Ranjan:
A Comparison of Presburger Engines for EFSM Reachability.
280-292 BibTeX
- Michael Colón, Tomás E. Uribe:
Generating Finite-State Abstractions of Reactive Systems Using Decision Procedures.
293-304 BibTeX
- Parosh Aziz Abdulla, Ahmed Bouajjani, Bengt Jonsson:
On-the-Fly Analysis of Systems with Unbounded, Lossy FIFO Channels.
305-318 BibTeX
- Saddek Bensalem, Yassine Lakhnech, Sam Owre:
Computing Abstractions of Infinite State Systems Compositionally and Automatically.
319-331 BibTeX
- W. O. David Griffioen, Frits W. Vaandrager:
Normed Simulations.
332-344 BibTeX
- Raphaël Couturier, Dominique Méry:
An Experiment in Parallelizing an Application Using Formal Methods.
345-356 BibTeX
- Scott D. Stoller, Yanhong A. Liu:
Efficient Symbolic Detection of Global Properties in Distributed Systems.
357-368 BibTeX
- Matthew Wilding:
A Machine-Checked Proof of the Optimality of a Real-Time Scheduling Policy.
369-378 BibTeX
- Parosh Aziz Abdulla, Bengt Jonsson, Mats Kindahl, Doron Peled:
A General Approach to Partial Order Reductions in Symbolic Verification (Extended Abstract).
379-390 BibTeX
- Felice Balarin:
Correctness of the Concurrent Approach to Symbolic Verification of Interleaved Models.
391-402 BibTeX
- Wendy Belluomini, Chris J. Myers:
Verification of Timed Systems Using POSETs.
403-415 BibTeX
- Giampaolo Bella, Lawrence C. Paulson:
Mechanising BAN Kerberos by the Inductive Method.
416-427 BibTeX
- Amy P. Felty, Douglas J. Howe, Frank A. Stomp:
Protocol Verification in Nuprl.
428-439 BibTeX
- Thomas A. Henzinger, Shaz Qadeer, Sriram K. Rajamani:
You Assume, We Guarantee: Methodology and Case Studies.
440-451 BibTeX
- E. Allen Emerson, Kedar S. Namjoshi:
Verification of Parameterized Bus Arbitration Protocol.
452-463 BibTeX
- Ratan Nalumasu, Rajnish Ghughal, Abdelillah Mokkedem, Ganesh Gopalakrishnan:
The 'Test Model-Checking' Approach to the Verification of Formal Memory Models of Multiprocessors.
464-476 BibTeX
- Matt Kaufmann, Andrew Martin, Carl Pixley:
Design Constraints in Symbolic Model Checking.
477-487 BibTeX
- Yirng-An Chen, Randal E. Bryant:
Verification of Floating-Point Adders.
488-499 BibTeX
Tool Papers
- Amar Bouali:
XEVE, an ESTEREL Verification Environment.
500-504 BibTeX
- Saddek Bensalem, Yassine Lakhnech, Sam Owre:
InVeST: A Tool for the Verification of Invariants.
505-510 BibTeX
- Gian Luigi Ferrari, Stefania Gnesi, Ugo Montanari, Marco Pistore, Gioia Ristori:
Verifying Mobile Processes in the HAL Environment.
511-515 BibTeX
- Jacob Elgaard, Nils Klarlund, Anders Møller:
MONA 1.x: New Techniques for WS1S and WS2S.
516-520 BibTeX
- Rajeev Alur, Thomas A. Henzinger, Freddy Y. C. Mang, Shaz Qadeer, Sriram K. Rajamani, Serdar Tasiran:
MOCHA: Modularity in Model Checking.
521-525 BibTeX
- Constance L. Heitmeyer, James Kirby, Bruce G. Labaw, Ramesh Bharadwaj:
SCR*: A Toolset for Specifying and Analyzing Software Requirements.
526-531 BibTeX
- Doron Peled:
A Toolset for Message Sequence Charts.
532-536 BibTeX
- Udo Brockmeyer, Gunnar Wittich:
Real-Time Verification of Statemate Designs.
537-541 BibTeX
- Conrado Daws:
Optikron: A Tool Suite for Enhancing Model-Checking of Real-Time Systems.
542-545 BibTeX
- Marius Bozga, Conrado Daws, Oded Maler, Alfredo Olivero, Stavros Tripakis, Sergio Yovine:
Kronos: A Model-Checking Tool for Real-Time Systems.
546-550 BibTeX
Copyright © Sat May 16 23:00:37 2009
by Michael Ley (ley@uni-trier.de)
