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

Full work available at URL https://doi.org/10.4204/eptcs.70.1

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

• 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
• scientific article; zbMATH DE number 3702108 (Why is no real title available?)
• 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)