Abstract is missing.
- Synchronous Programming of Reactive SystemsNicolas Halbwachs. 1-16
- Ten Years of Partial Order ReductionDoron Peled. 17-28
- An ACL2 Proof of Write Invalidate Cache CoherenceJ. Strother Moore. 29-38
- Transforming the Theorem Prover into a Digital Design Tool: From Concept Car to Off-Road VehicleDavid Hardin, Matthew Wilding, David A. Greve. 39-44
- A Role for Theorem Proving in Multi-Processor DesignAlbert John Camilleri. 45-48
- A Formal Method Experience at Secure Computing CorporationJohn Hoffman, Charlie Payne. 49-56
- Formal Methods in an Industrial EnvironmentJorge Cuéllar. 57-60
- On Checking Model CheckersGerard J. Holzmann. 61-70
- Finite-State Analysis of Security ProtocolsJohn C. Mitchell. 71-76
- Integrating Proof-Based and Model-Checking Techniques for the Formal Verification of Cryptographic ProtocolsDominique Bolignano. 77-87
- Verifying Systems with Infinite but Regular State SpacesPierre Wolper, Bernard Boigelot. 88-97
- Formal Verification of Out-of-Order Execution Using Incremental FlushingJens U. Skakkebæk, Robert B. Jones, David L. Dill. 98-109
- Verification of an Implementation of Tomasulo s Algorithm by Compositional Model CheckingKenneth L. McMillan. 110-121
- Decomposing the Proof of Correctness of pipelined MicroprocessorsRavi Hosabettu, Mandayam K. Srivas, Ganesh Gopalakrishnan. 122-134
- Processor Verification with Precise Exeptions and Speculative ExecutionJun Sawada, Warren A. Hunt Jr.. 135-146
- Symmetry Reductions inModel CheckingEdmund M. Clarke, E. Allen Emerson, Somesh Jha, A. Prasad Sistla. 147-158
- Structural Symmetry and Model CheckingGurmeet Singh Manku, Ramin Hojati, Robert K. Brayton. 159-171
- Using Magnatic Disk Instead of Main Memory in the Mur::::phi:::: VerifierUlrich Stern, David L. Dill. 172-183
- On-the-Fly Model Checking of RCTL FormulasIlan Beer, Shoham Ben-David, Avner Landver. 184-194
- From ::::Pre::::-historic to ::::Post::::-modern Symbolic Model CheckingThomas A. Henzinger, Orna Kupferman, Shaz Qadeer. 195-206
- Model Checking LTL Using Net UnforldingsFrank Wallner. 207-218
- Model Checking for a First-Order Temporal Logic Using Multiway Decision GraphsYing Xu, Eduard Cerny, Xiaoyu Song, Francisco Corella, Otmane Aït Mohamed. 219-231
- On the Limitations of Ordered Representations of FunctionsJayram S. Thathachar. 232-243
- BDD Based Procedures for a Theory of Equality with Uninterpreted FunctionsAnuj Goel, Khurram Sajid, Hai Zhou, Adnan Aziz, Vigyan Singhal. 244-255
- Computing Reachable Control States of Systems Modeled with Uninterpreted Functions and Infinite MemoryAdrian J. Isles, Ramin Hojati, Robert K. Brayton. 256-267
- Multiple Counters Automata, Safety Analysis and Presburger ArithmeticHubert Comon, Yan Jurski. 268-279
- A Comparison of Presburger Engines for EFSM ReachabilityThomas R. Shiple, James H. Kukula, Rajeev K. Ranjan. 280-292
- Generating Finite-State Abstractions of Reactive Systems Using Decision ProceduresMichael Colón, Tomás E. Uribe. 293-304
- On-the-Fly Analysis of Systems with Unbounded, Lossy FIFO ChannelsParosh Aziz Abdulla, Ahmed Bouajjani, Bengt Jonsson. 305-318
- Computing Abstractions of Infinite State Systems Compositionally and AutomaticallySaddek Bensalem, Yassine Lakhnech, Sam Owre. 319-331
- Normed SimulationsW. O. David Griffioen, Frits W. Vaandrager. 332-344
- An Experiment in Parallelizing an Application Using Formal MethodsRaphaël Couturier, Dominique Méry. 345-356
- Efficient Symbolic Detection of Global Properties in Distributed SystemsScott D. Stoller, Yanhong A. Liu. 357-368
- A Machine-Checked Proof of the Optimality of a Real-Time Scheduling PolicyMatthew Wilding. 369-378
- A General Approach to Partial Order Reductions in Symbolic Verification (Extended Abstract)Parosh Aziz Abdulla, Bengt Jonsson, Mats Kindahl, Doron Peled. 379-390
- Correctness of the Concurrent Approach to Symbolic Verification of Interleaved ModelsFelice Balarin. 391-402
- Verification of Timed Systems Using POSETsWendy Belluomini, Chris J. Myers. 403-415
- Mechanising BAN Kerberos by the Inductive MethodGiampaolo Bella, Lawrence C. Paulson. 416-427
- Protocol Verification in NuprlAmy P. Felty, Douglas J. Howe, Frank A. Stomp. 428-439
- You Assume, We Guarantee: Methodology and Case StudiesThomas A. Henzinger, Shaz Qadeer, Sriram K. Rajamani. 440-451
- Verification of Parameterized Bus Arbitration ProtocolE. Allen Emerson, Kedar S. Namjoshi. 452-463
- The Test Model-Checking Approach to the Verification of Formal Memory Models of MultiprocessorsRatan Nalumasu, Rajnish Ghughal, Abdelillah Mokkedem, Ganesh Gopalakrishnan. 464-476
- Design Constraints in Symbolic Model CheckingMatt Kaufmann, Andrew Martin, Carl Pixley. 477-487
- Verification of Floating-Point AddersYirng-An Chen, Randal E. Bryant. 488-499
- XEVE, an ESTEREL Verification EnvironmentAmar Bouali. 500-504
- InVeST: A Tool for the Verification of InvariantsSaddek Bensalem, Yassine Lakhnech, Sam Owre. 505-510
- Verifying Mobile Processes in the HAL EnvironmentGian Luigi Ferrari, Stefania Gnesi, Ugo Montanari, Marco Pistore, Gioia Ristori. 511-515
- MONA 1.x: New Techniques for WS1S and WS2SJacob Elgaard, Nils Klarlund, Anders Møller. 516-520
- MOCHA: Modularity in Model CheckingRajeev Alur, Thomas A. Henzinger, Freddy Y. C. Mang, Shaz Qadeer, Sriram K. Rajamani, Serdar Tasiran. 521-525
- SCR*: A Toolset for Specifying and Analyzing Software RequirementsConstance L. Heitmeyer, James Kirby, Bruce G. Labaw, Ramesh Bharadwaj. 526-531
- A Toolset for Message Sequence ChartsDoron Peled. 532-536
- Real-Time Verification of Statemate DesignsUdo Brockmeyer, Gunnar Wittich. 537-541
- Optikron: A Tool Suite for Enhancing Model-Checking of Real-Time SystemsConrado Daws. 542-545
- Kronos: A Model-Checking Tool for Real-Time SystemsMarius Bozga, Conrado Daws, Oded Maler, Alfredo Olivero, Stavros Tripakis, Sergio Yovine. 546-550