Integrating testing and interactive theorem proving

DOI10.4204/eptcs.70.1MaRDI QIDQ6586529zbMATH OpenFDO

Authors Harsh Raju Chamarthi, Peter C. Dillinger, Matt Kaufmann, Panagiotis Manolios

Publication date 13 August 2024

Mathematics Subject Classification ID

Theorem proving (automated and interactive theorem provers, deduction, resolution, etc.) (68V15)

Recommendations

• The ACL2 Sedan theorem proving system
• On theorem prover-based testing
• scientific article; zbMATH DE number 1552511
• Smart testing of functional programs in Isabelle
• ACL2s: ``the ACL2 sedan

Cites work

• scientific article; zbMATH DE number 3702108 (Why is no real title available?)
• A framework for verifying bit-level pipelined machines based on automated deduction and decision procedures
• ACL2s: ``the ACL2 sedan
• Formal Approaches to Software Testing
• Functional Testing in the Focal Environment
• Termination Analysis with Calling Context Graphs
• Testing can be formal, too

Cited in

(1)

• How can I do that with ACL2? Recent enhancements to ACL2

This page was built for publication: Integrating testing and interactive theorem proving

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q6586529)