[Colloq] Thesis Proposal - Interactive (Non)Theorem (Dis)Proving - Harsh Raju Chamarthi- Tuesday, September 22, 3-4 pm WVH 366

[DiFazio, Danielle]

Title: Interactive (Non)Theorem (Dis)Proving
Speaker: Harsh Raju Chamarthi
Date: Tuesday, September 22
Time: 3:00pm-4:00pm

Location: 366WVH

Abstract:
We present a framework for interactively disproving non-theorems. Our method can be used to add automated disproving and counterexample generation capabilities to existing interactive theorem provers. 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. We present various disproving techniques and discuss an implementation and evaluation of the framework using ACL2s, the ACL2 Sedan.

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

Proposal Web Page: 
http://www.ccs.neu.edu/home/harshrc/proposal.html