# 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