DIMACS Summer School on Applied Logic
Tutorial on Computer-Aided Verification
Aug. 28 -- Sep. 1, 1995
All talks will be at the DIMACS Center located at Rutgers University,
Busch Campus, in Piscataway, New Jersey.
Session Schedules
All sessions are 90 minutes
Monday, August 28
- Session 1, 10:00AM - 11:30AM (McMillan):
Intro/ History/ Philosophy
- Session 2, 1:00PM -- 2:30PM (Moore): Theorem proving I
- Session 3, 3:00PM -- 4:30PM (Moore): Theorem Proving II
Tuesday, August 29
- Session 1, 10:00AM - 11:30AM (McMillan):
Models of concurrency and communication
- Shared memory (Murphi)
- Synchronous communication
- Simultaneous (s/r, Esterelle)
- Interleaving (CCS, CSP, Petri nets)
- Asynchronous communication (Promela)
- Session 2,1:00PM -- 2:30PM (McMillan): Temporal logic
- Linear/ branching time
- Safety/ liveness/ fairness
- Model checking
- Session 3, 3:00PM -- 4:30PM (Wolper): Automata
- omega-automata and omega-regular languages
- tableau construction
- tree automata
Wednesday, August 30
- Session 1, 10:00AM - 11:30AM (Kurshan): S/R model and COSPAN
- Session 2, 1:00PM -- 2:30PM (Kurshan): Complexity issues
- Session 3, 3:00PM -- 4:30PM (McMillan): Compositional systems
- Equivalances and preorders
- Compositonal Mimization
- Trace conformance
Thursday, August 31
- Session 1, 10:00AM - 11:30AM (Kurshan): Abstraction
- Homomorphic reduction
- Top-down methodology
- Inductive abstractions
- Session 2, 1:00PM -- 2:30PM (McMillan): Symbolic model checking
- Binary decision diagrams
- Symbolic algorithms
- The SMV system
- Session 3, 3:00PM -- 4:30PM (Wolper): Partial order methods
- Traces and partial commutivity
- Partial order reductions
- The SPIN system
Friday, September 1
- Session 1, 10:00AM - 11:30AM (McMillan): Symmetry
- Data independence/ saturation
- Symmetry reductions
- The Murphi system
- Session 2, 1:00PM -- 2:30PM (Alur): Real time and hybrid systems
- Timed/Hybrid automata
- Real time COSPAN
- Session 3, 3:00PM -- 4:30PM (Kurshan): Continuous dynamical systems