A new technique for verifying and correcting logic programs

DOI10.1023/A:1005878609884zbMATH Open0884.68033MaRDI QIDQ1373300FDOQ1373300

Authors: Ricardo Caferra, Nicolas Peltier 

Publication date: 18 November 1997

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

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

zbMATH Keywords

formal specificationsmodel-building method

Mathematics Subject Classification ID

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

Cited In (10)

• 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
• Title not available (Why is that?)
• Kima: An automated error correction system for concurrent logic programs
• A new machine-checked proof of strong normalisation for display logic
• Title not available (Why is that?)
• 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
• Error diagnosis in logic programming an adaptation of E.Y. Shapiro's method

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)