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
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

- Kenneth L. McMillan:
Verification of an Implementation of Tomasulo's Algorithm by Compositional Model Checking.
110-121

- Ravi Hosabettu, Mandayam K. Srivas, Ganesh Gopalakrishnan:
Decomposing the Proof of Correctness of pipelined Microprocessors.
122-134

- Jun Sawada, Warren A. Hunt Jr.:
Processor Verification with Precise Exeptions and Speculative Execution.
135-146

- Edmund M. Clarke, E. Allen Emerson, Somesh Jha, A. Prasad Sistla:
Symmetry Reductions inModel Checking.
147-158

- Gurmeet Singh Manku, Ramin Hojati, Robert K. Brayton:
Structural Symmetry and Model Checking.
159-171

- Ulrich Stern, David L. Dill:
Using Magnatic Disk Instead of Main Memory in the Murphi Verifier.
172-183

- Ilan Beer, Shoham Ben-David, Avner Landver:
On-the-Fly Model Checking of RCTL Formulas.
184-194

- Thomas A. Henzinger, Orna Kupferman, Shaz Qadeer:
From Pre-historic to Post-modern Symbolic Model Checking.
195-206

- Frank Wallner:
Model Checking LTL Using Net Unforldings.
207-218

- 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

- Jayram S. Thathachar:
On the Limitations of Ordered Representations of Functions.
232-243

- Anuj Goel, Khurram Sajid, Hai Zhou, Adnan Aziz, Vigyan Singhal:
BDD Based Procedures for a Theory of Equality with Uninterpreted Functions.
244-255

- Adrian J. Isles, Ramin Hojati, Robert K. Brayton:
Computing Reachable Control States of Systems Modeled with Uninterpreted Functions and Infinite Memory.
256-267

- Hubert Comon, Yan Jurski:
Multiple Counters Automata, Safety Analysis and Presburger Arithmetic.
268-279

- Thomas R. Shiple, James H. Kukula, Rajeev K. Ranjan:
A Comparison of Presburger Engines for EFSM Reachability.
280-292

- Michael Colón, Tomás E. Uribe:
Generating Finite-State Abstractions of Reactive Systems Using Decision Procedures.
293-304

- Parosh Aziz Abdulla, Ahmed Bouajjani, Bengt Jonsson:
On-the-Fly Analysis of Systems with Unbounded, Lossy FIFO Channels.
305-318

- Saddek Bensalem, Yassine Lakhnech, Sam Owre:
Computing Abstractions of Infinite State Systems Compositionally and Automatically.
319-331

- W. O. David Griffioen, Frits W. Vaandrager:
Normed Simulations.
332-344

- Raphaël Couturier, Dominique Méry:
An Experiment in Parallelizing an Application Using Formal Methods.
345-356

- Scott D. Stoller, Yanhong A. Liu:
Efficient Symbolic Detection of Global Properties in Distributed Systems.
357-368

- Matthew Wilding:
A Machine-Checked Proof of the Optimality of a Real-Time Scheduling Policy.
369-378

- Parosh Aziz Abdulla, Bengt Jonsson, Mats Kindahl, Doron Peled:
A General Approach to Partial Order Reductions in Symbolic Verification (Extended Abstract).
379-390

- Felice Balarin:
Correctness of the Concurrent Approach to Symbolic Verification of Interleaved Models.
391-402

- Wendy Belluomini, Chris J. Myers:
Verification of Timed Systems Using POSETs.
403-415

- Giampaolo Bella, Lawrence C. Paulson:
Mechanising BAN Kerberos by the Inductive Method.
416-427

- Amy P. Felty, Douglas J. Howe, Frank A. Stomp:
Protocol Verification in Nuprl.
428-439

- Thomas A. Henzinger, Shaz Qadeer, Sriram K. Rajamani:
You Assume, We Guarantee: Methodology and Case Studies.
440-451

- E. Allen Emerson, Kedar S. Namjoshi:
Verification of Parameterized Bus Arbitration Protocol.
452-463

- Ratan Nalumasu, Rajnish Ghughal, Abdelillah Mokkedem, Ganesh Gopalakrishnan:
The 'Test Model-Checking' Approach to the Verification of Formal Memory Models of Multiprocessors.
464-476

- Matt Kaufmann, Andrew Martin, Carl Pixley:
Design Constraints in Symbolic Model Checking.
477-487

- Yirng-An Chen, Randal E. Bryant:
Verification of Floating-Point Adders.
488-499

Tool Papers
- Amar Bouali:
XEVE, an ESTEREL Verification Environment.
500-504

- Saddek Bensalem, Yassine Lakhnech, Sam Owre:
InVeST: A Tool for the Verification of Invariants.
505-510

- Gian Luigi Ferrari, Stefania Gnesi, Ugo Montanari, Marco Pistore, Gioia Ristori:
Verifying Mobile Processes in the HAL Environment.
511-515

- Jacob Elgaard, Nils Klarlund, Anders Møller:
MONA 1.x: New Techniques for WS1S and WS2S.
516-520

- Rajeev Alur, Thomas A. Henzinger, Freddy Y. C. Mang, Shaz Qadeer, Sriram K. Rajamani, Serdar Tasiran:
MOCHA: Modularity in Model Checking.
521-525

- Constance L. Heitmeyer, James Kirby, Bruce G. Labaw, Ramesh Bharadwaj:
SCR*: A Toolset for Specifying and Analyzing Software Requirements.
526-531

- Doron Peled:
A Toolset for Message Sequence Charts.
532-536

- Udo Brockmeyer, Gunnar Wittich:
Real-Time Verification of Statemate Designs.
537-541

- Conrado Daws:
Optikron: A Tool Suite for Enhancing Model-Checking of Real-Time Systems.
542-545

- Marius Bozga, Conrado Daws, Oded Maler, Alfredo Olivero, Stavros Tripakis, Sergio Yovine:
Kronos: A Model-Checking Tool for Real-Time Systems.
546-550

Last update Tue May 21 16:19:53 2013
CET by the DBLP Team —
Data released under the ODC-BY 1.0 license — See also our legal information page