Formal Methods and Computer Aided Design
|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.
Remarks on selected talks:
- 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]
Last modified: Mon Jan 10 15:11:13 2000