CAV A*

55 papers

YearTitle / Authors
1998A Comparison of Presburger Engines for EFSM Reachability.
Thomas R. Shiple, James H. Kukula, Rajeev K. Ranjan
1998A Formal Method Experience at Secure Computing Corporation.
John Hoffman, Charlie Payne
1998A General Approach to Partial Order Reductions in Symbolic Verification (Extended Abstract).
Parosh Aziz Abdulla, Bengt Jonsson, Mats Kindahl, Doron A. Peled
1998A Machine-Checked Proof of the Optimality of a Real-Time Scheduling Policy.
Matthew Wilding
1998A Role for Theorem Proving in Multi-Processor Design.
Albert John Camilleri
1998A Toolset for Message Sequence Charts.
Doron A. Peled
1998An ACL2 Proof of Write Invalidate Cache Coherence.
J Strother Moore
1998An Experiment in Parallelizing an Application Using Formal Methods.
Raphaël Couturier, Dominique Méry
1998BDD Based Procedures for a Theory of Equality with Uninterpreted Functions.
Anuj Goel, Khurram Sajid, Hai Zhou, Adnan Aziz, Vigyan Singhal
1998Computer Aided Verification, 10th International Conference, CAV '98, Vancouver, BC, Canada, June 28 - July 2, 1998, Proceedings
Alan J. Hu, Moshe Y. Vardi
1998Computing Abstractions of Infinite State Systems Compositionally and Automatically.
Saddek Bensalem, Yassine Lakhnech, Sam Owre
1998Computing Reachable Control States of Systems Modeled with Uninterpreted Functions and Infinite Memory.
Adrian J. Isles, Ramin Hojati, Robert K. Brayton
1998Correctness of the Concurrent Approach to Symbolic Verification of Interleaved Models.
Felice Balarin
1998Decomposing the Proof of Correctness of pipelined Microprocessors.
Ravi Hosabettu, Mandayam K. Srivas, Ganesh Gopalakrishnan
1998Design Constraints in Symbolic Model Checking.
Matt Kaufmann, Andrew Martin, Carl Pixley
1998Efficient Symbolic Detection of Global Properties in Distributed Systems.
Scott D. Stoller, Yanhong A. Liu
1998Finite-State Analysis of Security Protocols.
John C. Mitchell
1998Formal Methods in an Industrial Environment.
Jorge Cuéllar
1998Formal Verification of Out-of-Order Execution Using Incremental Flushing.
Jens U. Skakkebæk, Robert B. Jones, David L. Dill
1998From
Thomas A. Henzinger, Orna Kupferman, Shaz Qadeer
1998Generating Finite-State Abstractions of Reactive Systems Using Decision Procedures.
Michael Colón, Tomás E. Uribe
1998InVeST: A Tool for the Verification of Invariants.
Saddek Bensalem, Yassine Lakhnech, Sam Owre
1998Integrating Proof-Based and Model-Checking Techniques for the Formal Verification of Cryptographic Protocols.
Dominique Bolignano
1998Kronos: A Model-Checking Tool for Real-Time Systems.
Marius Bozga, Conrado Daws, Oded Maler, Alfredo Olivero, Stavros Tripakis, Sergio Yovine
1998MOCHA: Modularity in Model Checking.
Rajeev Alur, Thomas A. Henzinger, Freddy Y. C. Mang, Shaz Qadeer, Sriram K. Rajamani, Serdar Tasiran
1998MONA 1.x: New Techniques for WS1S and WS2S.
Jacob Elgaard, Nils Klarlund, Anders Møller
1998Mechanising BAN Kerberos by the Inductive Method.
Giampaolo Bella, Lawrence C. Paulson
1998Model Checking LTL Using Net Unforldings.
Frank Wallner
1998Model Checking for a First-Order Temporal Logic Using Multiway Decision Graphs.
Ying Xu, Eduard Cerny, Xiaoyu Song, Francisco Corella, Otmane Aït Mohamed
1998Multiple Counters Automata, Safety Analysis and Presburger Arithmetic.
Hubert Comon, Yan Jurski
1998Normed Simulations.
W. O. David Griffioen, Frits W. Vaandrager
1998On Checking Model Checkers.
Gerard J. Holzmann
1998On the Limitations of Ordered Representations of Functions.
Jayram S. Thathachar
1998On-the-Fly Analysis of Systems with Unbounded, Lossy FIFO Channels.
Parosh Aziz Abdulla, Ahmed Bouajjani, Bengt Jonsson
1998On-the-Fly Model Checking of RCTL Formulas.
Ilan Beer, Shoham Ben-David, Avner Landver
1998Optikron: A Tool Suite for Enhancing Model-Checking of Real-Time Systems.
Conrado Daws
1998Processor Verification with Precise Exeptions and Speculative Execution.
Jun Sawada, Warren A. Hunt Jr.
1998Protocol Verification in Nuprl.
Amy P. Felty, Douglas J. Howe, Frank A. Stomp
1998Real-Time Verification of Statemate Designs.
Udo Brockmeyer, Gunnar Wittich
1998SCR*: A Toolset for Specifying and Analyzing Software Requirements.
Constance L. Heitmeyer, James Kirby, Bruce G. Labaw, Ramesh Bharadwaj
1998Structural Symmetry and Model Checking.
Gurmeet Singh Manku, Ramin Hojati, Robert K. Brayton
1998Symmetry Reductions in Model Checking.
Edmund M. Clarke, E. Allen Emerson, Somesh Jha, A. Prasad Sistla
1998Synchronous Programming of Reactive Systems.
Nicolas Halbwachs
1998Ten Years of Partial Order Reduction.
Doron A. Peled
1998The 'Test Model-Checking' Approach to the Verification of Formal Memory Models of Multiprocessors.
Ratan Nalumasu, Rajnish Ghughal, Abdelillah Mokkedem, Ganesh Gopalakrishnan
1998Transforming the Theorem Prover into a Digital Design Tool: From Concept Car to Off-Road Vehicle.
David S. Hardin, Matthew Wilding, David A. Greve
1998Using Magnatic Disk Instead of Main Memory in the Mur
Ulrich Stern, David L. Dill
1998Verification of Floating-Point Adders.
Yirng-An Chen, Randal E. Bryant
1998Verification of Parameterized Bus Arbitration Protocol.
E. Allen Emerson, Kedar S. Namjoshi
1998Verification of Timed Systems Using POSETs.
Wendy Belluomini, Chris J. Myers
1998Verification of an Implementation of Tomasulo's Algorithm by Compositional Model Checking.
Kenneth L. McMillan
1998Verifying Mobile Processes in the HAL Environment.
Gian-Luigi Ferrari, Stefania Gnesi, Ugo Montanari, Marco Pistore, Gioia Ristori
1998Verifying Systems with Infinite but Regular State Spaces.
Pierre Wolper, Bernard Boigelot
1998XEVE, an ESTEREL Verification Environment.
Amar Bouali
1998You Assume, We Guarantee: Methodology and Case Studies.
Thomas A. Henzinger, Shaz Qadeer, Sriram K. Rajamani