M. Oliver Möller: Paper Presentation (Solving Bit-Vector Equations)
Relevance:
Special interest in formal methods and verification
[not part of BRICS conference groups S, A, B]
Overall rating:
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.
General trends:
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
Quotes:
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]
Oliver Möller
Last modified: Mon Jan 10 15:11:13 2000