A new technique for verifying and correcting logic programs

DOI10.1023/A:1005878609884MaRDI QIDQ1373300zbMATH OpenFDO

Authors Ricardo Caferra, Nicolas Peltier

Publication date 18 November 1997

Published in Journal of Automated Reasoning (Search for Journal in Brave)

zbMATH Keywords

formal specificationsmodel-building method

Mathematics Subject Classification ID

Logic programming (68N17) Specification and verification (program logics, model checking, etc.) (68Q60)

Recommendations

• Verification of logic programs
• Logic programs as specifications in the inductive verification of logic programs
• scientific article; zbMATH DE number 4037276
• scientific article; zbMATH DE number 868104
• Inductive assertion method for logic pograms

Cited in

(10)

• Error diagnosis in logic programming an adaptation of E.Y. Shapiro's method
• A Datalog hammer for supervisor verification conditions modulo simple linear arithmetic
• Verifying Tight Logic Programs with anthem and vampire
• Accepting/rejecting propositions from accepted/rejected propositions: A unifying overview
• scientific article; zbMATH DE number 1540615 (Why is no real title available?)
• Kima: An automated error correction system for concurrent logic programs
• A new machine-checked proof of strong normalisation for display logic
• scientific article; zbMATH DE number 1617312 (Why is no real title available?)
• Proving Programs Incorrect Using a Sequent Calculus for Java Dynamic Logic
• Combining enumeration and deductive techniques in order to increase the class of constructible infinite models

This page was built for publication: A new technique for verifying and correcting logic programs

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