52 citations · 71 across the 2 of their papers we have counts for
2 papers
cs.PL2014★ 19 cited
Data Definitions in the ACL2 Sedan
Harsh Raju Chamarthi, Peter C. Dillinger, Panagiotis Manolios
We present a data definition framework that enables the convenient specification of data types in ACL2s, the ACL2 Sedan. Our primary motivation for developing the data definition f…
cs.SE2011★ 52 cited
Integrating Testing and Interactive Theorem Proving
Harsh Raju Chamarthi, Peter C. Dillinger, Matt Kaufmann +1
Using an interactive theorem prover to reason about programs involves a sequence of interactions where the user challenges the theorem prover with conjectures. Invariably, many of…