PhD Thesis Proposal, Harsh Raju Chamarthi, 2015. [PDF]
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.
Panagiotis (Pete) Manolios, Professor, College of Computer and Information Science, Northeastern University (Advisor)
Karl Lieberherr, Professor, College of Computer and Information Science, Northeastern University
Olin Shivers, Professor, College of Computer and Information Science, Northeastern University
Matt Kaufmann, Senior Research Scientist, Department of Computer Sciences, University of Texas at Austin (External Member)
Karl Lieberherr is an expert on SAT and CSP. Olin Shivers is an expert on Static Analysis. Matt Kaufmann is an expert on interactive theorem proving and logic. He is an author of ACL2, a widely-used interactive theorem prover, for which he won the ACM Software System award. -- Pete