[Colloq] Thesis Defense: Interactive Non-theorem Disproving Speaker: Harsh Raju Chamarthi Date: Thursday, October 27 Time: 3:00pm-4:00pm

[CCIS Operations Team]

Topic: Thesis Defense
Title: Interactive Non-theorem Disproving
Speaker: Harsh Raju Chamarthi
Date: Thursday, October 27
Time: 3:00pm-4:00pm

Location: 225 Richards Hall

Abstract:
We present a framework for interactively disproving non-theorems.  It is designed as an extension to existing interactive theorem provers, adding semi-automated support for counterexample generation. This capability increases the utility and effectiveness of theorem provers because it provides automated support for what users spend most of their time doing: debugging flawed models, invariants, interfaces and conjectures. The method used is based on concrete construction and executability; it makes essential use of user-specified enumerative characterization of constraints, combining property-based testing with proof-based deduction. We present various disproving techniques and discuss an implementation and evaluation of the framework using ACL2s.

Committee:
Panagiotis Manolios (Advisor)
Karl Lieberherr
Olin Shivers
Matt Kaufmann (University of Texas at Austin)