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
-
"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