Integrating testing and interactive theorem proving

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

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)

Cites Work

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

Related Items (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)