Time: | 3.-6. Nov 1998 |

Place: | Palo Alto, CA, USA |

Proceedings: | Springer, LNCS 1522 |

Attendance: | ca. 150 international Science/Industry |

from BRICS: | M. Oliver Möller: Paper Presentation (Solving Bit-Vector Equations) |

Special interest in formal methods and verification [not part of BRICS conference groups S, A, B]

Some interesting talks, showing case examples of applying formal methods to complex designs; no breakthrough. High attendence of prominent and interesting people.

- Asgeir Thor Eiriksson (proc.p.49), Silicon Graphics showed a catching case study of designing+verifying the most complex part of a 1M-gase ASIC (that was only possible as a one-man-project!)
- Mary Sheeran (p.82) gave an tutorial on Stålmarks SAT-method, in efficiency in practical applications comparable to the Davis-Putnam-Procedure [most approaches tend to be WORSE].
- Randal E. Bryant et al. (p.255) developed an interesting comparison of 6 mayor BDD packages.
- Henzinger et al. (p. 421) came up with a refinement condition that might turn out to be fairly powerful in state reduction.

- to verification via symbolic simulation [conf. e.g. Moore's example using ACL2]
- away from expensive BDD representation to alternative >>lazy<< and non-canonical forms

*I seem to work with unknowns all the time.*[Carl-Johan H. Seger]*Don't optimize the wrong area!*[Carl-Johan H. Seger]*If you use formal verification as a black box, it is pretty useless most of the time.*[Carl-Johan H. Seger]*The intersection of the people doing formal methods and the people doing graphics is empty.*[J. Strother Moore]*Utilize forgetfulness!*[Amir Pnueli]*It's exponential all over the place...*[Amir Pnueli]*It worked. But maybe, I just got lucky.*[James Kukula]