EECS Main
>
Events
Event Details
|
Graduate Research Seminar: Casey KleinNoon
August 17, 2009
| Casey Klein, "The MzScheme machine and bytecode verifier" | Abstract: In the spirit of VLISP, the Scheme implementation verified by Wand et al., we have formalized the MzScheme virtual machine and its bytecode verifier in PLT Redex. Rather than trying to prove it correct, however, we have applied QuickCheck-style randomized testing to try to find bugs. We were able to state and test two properties: that no program accepted by the verifier could crash the machine, and that a few of the machine's optimizations cannot change the meaning of programs. Both of these properties turned out to be false, and we were able to find several counterexamples automatically.
We also report on the utility of randomized testing for formal specifications. In short, the technique is remarkably cheap and can easily find a certain class of bugs. Some bugs, however, are quite difficult to find automatically, and thus, our experience suggests that randomized testing should be attempted before trying to prove anything, but that it does replace (machine-assisted) proof. |
|
