[Colloq] MS Thesis Defense Today, Monday, March 7 - 3pm

[Rachel Kalweit]

The College of Computer and Information Science presents: 




MS Thesis Defense : 
Zoe (Yue ZHANG) 

When: Monday, March 7th, 2011 
Time: 3:00pm 
166 West Village H 

Thesis title: An Attempted Proof with Modular ACL2: Soundness of the Racket Bytecode Verifier 

Abstract: 

ACL2 is a theorem prover for a Common LISP-based programming language. It is widely used in industry for verifying computer systems such as virtual machines. Modular ACL2, which extends ACL2 with interfaces and modules, is designed for verification of large programs by allowing programmers to reason separately about individual components. This thesis presents an in-depth case study of Modular ACL2 and provides new conclusions about it. 


Thesis committee: 

Matthias Felleisen (Advisor) 


Panagiotis Manolios 



Carl Eastlund