Publications
Book Chapters
-
"ACL2."
In The Seventeen Provers of the World, Wiedijk,
Lecture Notes in Artificial Intelligence, 2006.
-
"Continuity and Differentiability in ACL2."
In Computer-Aided Reasoning: ACL2 Case Studies, Kluwer
Academic Press, 2000.
-
"Inventory Control,"
with D. Chimenti.
In A Logical Language for Data and Knowledge Bases,
Naqvi and Tsur, Computer Science Press, 1989.
-
"Resource Allocation and Deallocation,"
with D. Chimenti.
In A Logical Language for Data and Knowledge Bases,
Naqvi and Tsur, Computer Science Press, 1989.
Refereed Journals
Refereed Conferences
-
"Using a First Order Logic to Verify That Some Set of Reals Has No Lebesgue Measure,"
with J. Cowles.
Presented in 1st International Conference on Interactive Theorem Proving (ITP 2010), Edinburgh, UK, 2010.
-
"Inverse Functions in ACL2(r),"
with J. Cowles.
Presented in ACL2 Workshop, Boston, 2009.
-
"Solving Triangles = Squares,"
with J. Cowles.
Presented in ACL2 Workshop, Boston, 2009.
-
"The Chain Rule and Friends in ACL2(r)" (rump talk), with J. Cowles. Presented in ACL2 Workshop, Boston, 2009.
-
"Enumerating Rationals without Repetitions" (rump talk), with J. Caldwell and J. Cowles. Presented in ACL2 Workshop, Boston, 2009.
-
"Extending Dynamic Constraint Detection with
Disjunctive Constraints,"
with N. Kuzmina, J. Paul, and J. Caldwell.
Presented in 6th International Workshop on Dynamic Analysis (WODA), Seattle,
2008.
-
"Toward a Formal Evaluation of Refactorings,"
with J. Paul, N. Kuzmina, and J. Caldwell.
Presented in 6th NASA Langley Formal Methods Workshop (LFM 2008), Newport News,
VA, 2008.
-
"Red-Black Trees for DrACuLa" (rump talk). Presented in ACL2 Workshop, Austin, 2007.
-
"Extending Dynamic Constraint Detection with Polymorphic
Analysis," with N. Kuzmina. Presented in
5th International Workshop on Dynamic Analysis
(WODA), Minneapolis, 2007.
-
"Dynamic Constraint Detection for Polymorphic Behavior" (poster),
with N. Kuzmina. Presented in OOPSLA, Portland, 2006.
-
"Unique Factorization in
ACL2: Euclidean Domains," with J. Cowles. Presented
in ACL2 Workshop 2006, Seattle, 2006.
-
"Implementing a Cost-Aware Evaluator
for ACL2 Expressions," with J. Cowles. Presented
in ACL2 Workshop 2006, Seattle, 2006.
-
"A Mechanical Proof of the Cook-Levin Theorem,"
with J. Cowles.
In Proceedings of the 17th International
Conference on Theorem Proving and Higher Order Logics
(TPHOLs), Park City, Utah, 2004.
-
"Curve-Based Representation of Moving Object Trajectories,"
with B. Yu, S.H. Kim, and T. Bailey.
In Proceedings of the International Database Engineering and
Applications Symposium (IDEAS), Portugal, 2004.
-
"Axiomatic Events in ACL2(r): A
Story of defun, defun-std, and encapsulate," with J. Cowles
and N. Kuzmina.
Presented in ACL2 Workshop 2004, Austin, 2004.
-
"Contributions to the Theory of Tail Recursive
Functions," with J. Cowles.
Presented in ACL2 Workshop 2004, Austin, 2004.
-
"On the Verification of Synthesized Kalman Filters,"
with J. Cowles and J. Van Baalen.
Presented in ACL2 Workshop 2003, Boulder, 2003.
-
"Using ACL2 Arrays to Formalize Matrix Algebra,"
with J. Cowles and J. Van Baalen.
Presented in ACL2 Workshop 2003, Boulder, 2003.
-
"Writing Literate Proofs with XML Tools."
Presented in ACL2 Workshop 2003, Boulder, 2003.
-
"Polymorphism in ACL2,"
with M. Patterson.
Presented in ACL2 Workshop 2003, Boulder, 2003.
-
"Mechanical Verification of a Square Root Algorithm using Taylor's Theorem,"
with J. Sawada.
In Proceedings of the Fourth International Conference on Formal Methods in Computer-Aided Design (FMCAD), Portland, 2002.
-
"Taylor's Formula with Remainder,"
with B. Middleton.
Presented in ACL2 Workshop 2002, Grenoble, France, 2002.
-
"Abstract Machine for LDL,"
with D. Chimenti and R. Krishnamurthy.
In Proceedings of the 2nd Conference on Extending Database
Technology (EDBT), Venice, 1990.
-
"Towards an Open Architecture for LDL,"
with D. Chimenti and R. Krishnamurthy.
In Proceedings of the 15th Conference on Very Large
Databases (VLDB), Amsterdam, 1989.
Technical Reports