Integrating testing and interactive theorem proving

DOI10.4204/eptcs.70.1zbMATH Open1542.68209MaRDI QIDQ6586529FDOQ6586529

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

Publication date: 13 August 2024

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

Mathematics Subject Classification ID

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

Cites Work

• Testing can be formal, too
• Title not available (Why is that?)
• Termination Analysis with Calling Context Graphs
• Formal Approaches to Software Testing
• ACL2s: ``the ACL2 sedan
• A framework for verifying bit-level pipelined machines based on automated deduction and decision procedures
• Functional Testing in the Focal Environment

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)