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

[Walker, Lashauna]

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)


Thank You.

LaShauna Walker
Events and Project Coordinator
College of Computer and Information Science
Northeastern University
617-373-2763
Facebook | Instagram | LinkedIn | Twitter