default search action
10th CAV 1998: Vancouver, BC, Canada
- Alan J. Hu, Moshe Y. Vardi:
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
- Nicolas Halbwachs:
Synchronous Programming of Reactive Systems. 1-16 - Doron A. Peled:
Ten Years of Partial Order Reduction. 17-28 - J Strother Moore:
An ACL2 Proof of Write Invalidate Cache Coherence. 29-38 - David S. Hardin, Matthew Wilding, David A. Greve:
Transforming the Theorem Prover into a Digital Design Tool: From Concept Car to Off-Road Vehicle. 39-44 - Albert John Camilleri:
A Role for Theorem Proving in Multi-Processor Design. 45-48 - John Hoffman, Charlie Payne:
A Formal Method Experience at Secure Computing Corporation. 49-56 - Jorge Cuéllar:
Formal Methods in an Industrial Environment. 57-60 - Gerard J. Holzmann:
On Checking Model Checkers. 61-70 - John C. Mitchell:
Finite-State Analysis of Security Protocols. 71-76 - Dominique Bolignano:
Integrating Proof-Based and Model-Checking Techniques for the Formal Verification of Cryptographic Protocols. 77-87 - Pierre Wolper
, Bernard Boigelot:
Verifying Systems with Infinite but Regular State Spaces. 88-97
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 in Model 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 A. 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
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 A. 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
manage site settings
To protect your privacy, all features that rely on external API calls from your browser are turned off by default. You need to opt-in for them to become active. All settings here will be stored as cookies with your web browser. For more information see our F.A.Q.
last updated on 2024-11-21 20:17 CET by the dblp team
all metadata released as open data under CC0 1.0 license
see also: Terms of Use | Privacy Policy | Imprint
dblp was originally created in 1993 at:
since 2018, dblp has been operated and maintained by:
the dblp computer science bibliography is funded and supported by: