CAV '98
International Conference on Computer-Aided Verification
June 28 - July 2, 1998
University of British Columbia, Vancouver, Canada
Advance Program
For information, registration, and accommodations, please see:
http://www.cs.ubc.ca/conferences/CAV98/index.html
This schedule is tentative and may change.
Sunday, June 28, 1998
9:00-10:30
Invited Tutorial Session 1:
Model Checking for Beginners: A Tutorial Introduction to
Finite-State Verification
Bob Kurshan (Bell Labs), Ken McMillan (Cadence Berkeley Labs)
Break
11:00-12:30
Invited Tutorial Session 2:
Continuation of Introductory Tutorial
Lunch
2:00-3:30
Invited Tutorial Session 3:
Synchronous Programming of Reactive Systems
Nicolas Halbwachs (VERIMAG)
Break
4:00-5:30
Invited Tutorial Session 4:
Ten Years of Partial Order Reduction
Doron Peled (Bell Labs)
Monday, June 29, 1998
8:30-10:00
Invited Session 1A: Industrial Application of Theorem Proving
"Ongoing Commercial Applications of the ACL2 Theorem Prover"
J Strother Moore (Univ. Texas Austin)
"Transforming the Theorem Prover into a Digital Design Tool:
From Concept Car to Off-Road Vehicle"
David Hardin, Matthew Wilding, David Greve (Rockwell Collins)
"A Role for Theorem Proving in Multi-Processor Design"
Albert Camilleri (Hewlett-Packard)
Break
10:30-12:00
Invited Session 1B: Industrial Application of Theorem Proving (cont'd)
"A Formal Experience at Secure Computing Corporation"
John Hoffman, Charlie Payne (Secure Computing)
"Formal Methods in an Industrial Environment"
Jorge Cuellar (Siemens)
Discussion
Lunch
1:15-3:15
Session 1C: Microprocessor Verification
"Formal Verification of Out-of-Order Execution Using
Incremental Flushing"
J. U. Skakkebaek, R. B. Jones, D. L. Dill
"Verification of an Implementation of Tomasulo's Algorithm
by Compositional Model Checking"
K. L. McMillan
"Decomposing the Proof of Correctness of Pipelined Microprocessors"
R. Hosabettu, M. Srivas, G. Gopalakrishnan
"Processor Verification with Precise Exceptions and
Speculative Execution"
J. Sawada, W. A. Hunt
Break
3:45-5:15
Session 1D: Combatting State Explosion
"Symmetry Reductions in Model Checking"
E. M. Clarke, E. A. Emerson, S. Jha, A. P. Sistla
"Structural Symmetry and Model Checking"
G. S. Manku, R. Hojati, R. K. Brayton
"Using Magnetic Disk Instead of Main Memory in the
Murphi Verifier"
U. Stern, D. L. Dill
Mini-Break
5:30-6:10
Session 1E: Tool Presentations
"XEVE, an Esterel Verification Environment"
A. Bouali
"InVeSt: A tool for the Verification of Invariants"
S. Bensalem, Y. Lakhnech, S. Owre
6:15-7:30
Demos and Hors d'Oeuvres
Tuesday, June 30, 1998
8:30-9:45
Session 2A: Invited Speaker -- Gerard J. Holzmann (Bell Labs)
"On Checking Model Checkers"
Break
10:15-11:45
Session 2B: Model Checking
"On-the-Fly Model Checking of RCTL Formulas"
I. Beer, S. Ben-David, A. Landver
"From Pre-historic to Post-modern Symbolic Model Checking"
T. A. Henzinger, O. Kupferman, S. Qadeer
"Model Checking LTL Using Net Unfoldings"
F. Wallner
Lunch
1:00-2:30
Session 2C: Decision Diagrams
"Model Checking for a First-Order Temporal Logic Using
Multiway Decision Graphs"
Y. Xu, E. Cerny, X. Song, F. Corella, O. Ait Mohamed
"On the Limitations of Ordered Representations of Functions"
J. S. Thathachar
"BDD Based Procedures for a Theory of Equality with
Uninterpreted Functions"
A. Goel, K. Sajid, H. Zhou, A. Aziz, V. Singhal
Break
3:00-5:00
Session 2D: Invited Tutorial -- Verification of Security Protocols
"Finite State Analysis of Security Protocols"
John. C. Mitchell
"Integrating Proof-based and Model-checking Techniques for
the Formal Verification of Cryptographic Protocols"
Dominique Bolignano
Mini-Break
5:15-6:15
Session 2E: Tool Presentations
"Verifying Mobile Processes in the HAL Environment"
G. Ferrari, S. Gnesi, U. Montanari, M. Pistore, G. Ristori
"MONA 1.x: New Techniques for WS1S and WS2S"
J. Elgaard, N. Klarlund, A. Moller
"MOCHA: Modularity in Model Checking"
R. Alur, T. Henzinger, F. Mang, S. Qadeer,
S. Rajamani, S. Tasiran
6:15-7:30
Demos and Hors d'Oeuvres
Wednesday, July 1, 1998
8:30-9:45
Session 3A: Invited Speaker -- Pierre Wolper (University of Liege)
"Verifying Systems with Infinite but Regular State Spaces"
Pierre Wolper, Bernard Boigelot
Break
10:15-11:45
Session 3B: Extended Finite-State Machines
"Computing Reachable Control States of Systems Modeled with
Uninterpreted Functions and Infinite Memory"
A. J. Isles, R. Hojati, R. K. Brayton
"Multiple Counters Automata, Safety Analysis,
and Presburger Arithmetic"
H. Comon, Y. Jurski
"A Comparison of Presburger Engines for EFSM Reachability"
T. R. Shiple, J. H. Kukula, R. K. Ranjan
Lunch
1:00-3:00
Session 3C: Abstraction and Refinement
"Generating Finite-State Abstractions of Reactive Systems Using
Decision Procedures"
M. A. Colon, T. E. Uribe
"On-the-Fly Analysis of Systems with Unbounded, Lossy FIFO Channels"
P. A. Abdulla, A. Bouajjani, B. Jonsson
"Computing Abstractions of Infinite State Systems Compositionally
and Automatically"
S. Bensalem, Y. Lakhnech, S. Owre
"Normed Simulations"
D. Griffioen, F. Vaandrager
Break
3:30-5:00
Session 3D: Formal Methods and Software Systems
"An Experiment in Parallelizing an Application Using Formal Methods"
R. Couturier, D. Mery
"Efficient Symbolic Detection of Global Properties in
Distributed Systems"
S. D. Stoller, Y. A. Liu
"A Machine-Checked Proof of the Optimality of a Real-Time
Scheduling Policy"
M. Wilding
Mini-Break
5:10-5:50
Session 3E: Tool Presentations
"The SCR Toolset for Specifying and Analyzing Software Requirements"
C. Heitmeyer, J. Kirby, B. Labaw, R. Bharadwaj
"A Toolset for Message Sequence Charts"
D. Peled
6:00-7:15
Demos and Drinks
7:30-?
Salmon BBQ Banquet
Thursday, July 2, 1998
8:30-9:45
Session 4A: Invited Speaker -- Carl Seger (Intel)
"Combining Theorem Proving and Model Checking: How Much
Theorem Proving Is Needed?"
Break
10:15-11:45
Session 4B: Partial Order
"A General Approach to Partial Order Reductions in
Symbolic Verification"
P. A. Abdulla, B. Jonsson, M. Kindahl, D. Peled
"Correctness of the Concurrent Approach to Symbolic Verification
of Interleaved Models"
F. Balarin
"Verification of Timed Systems Using POSETS"
W. Belluomini, C. J. Myers
Lunch
1:00-3:00
Session 4C: Case Studies
"Mechanising BAN Kerberos by the Inductive Method"
G. Bella, L. C. Paulson
"Protocol Verification in Nuprl"
A. P. Felty, D. J. Howe, F. A. Stomp
"You Assume, We Guarantee: Methodology and Case Studies"
T. A. Henzinger, S. Qadeer, S. K. Rajamani
"Verification of a Parameterized Bus Arbitration Protocol"
E. A. Emerson, K. S. Namjoshi
Break
3:30-5:00
Session 4D: Hardware Verification
"The `Test Model-Checking' Approach to the Verification of
Formal Memory Models of Multiprocessors"
R. Nalumasu, R. Ghughal, A. Mokkedem, G. Gopalakrishnan
"Design Constraints in Symbolic Model Checking"
M. Kaufmann, A. Martin, C. Pixley
"Verification of Floating-Point Adders"
Y.-A. Chen, R. E. Bryant
Mini-Break
5:15-6:15
Session 4E: Tool Presentations
"Real-Time Verification of STATEMATE Designs"
U. Brockmeyer, G. Wittich
"Optikron: a tool suite for enhancing model-checking
of real-time systems"
C. Daws
"Kronos: a model-checking tool for real-time systems"
M. Bozga, C. Daws, O. Maler, A. Olivero,
S. Tripakis, S. Yovine
6:15-7:30 Demos and Hors d'Oeuvres
End of Conference