Assertion based inductive verification methods for logic programs

DOI10.1016/S1571-0661(05)80036-2MaRDI QIDQ4923368zbMATH OpenOpenAlexFDO

Authors Roberta Gori, Marco Comini, Giorgio Levi

Publication date 6 June 2013

Published in Electronic Notes in Theoretical Computer Science (Search for Journal in Brave)

Full work available at URL https://doi.org/10.1016/s1571-0661(05)80036-2

zbMATH Keywords

abstract interpretationassertion languageinductive verificationtransformation of logic programs

Mathematics Subject Classification ID

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

Recommendations

• Abstract interpretation based verification of logic programs
• Logic programs as specifications in the inductive verification of logic programs
• scientific article; zbMATH DE number 1497823
• scientific article; zbMATH DE number 4037276
• scientific article; zbMATH DE number 1222416

Cites work

• Abstract diagnosis
• Error diagnosis in logic programming an adaptation of E.Y. Shapiro's method
• scientific article; zbMATH DE number 1615258 (Why is no real title available?)
• scientific article; zbMATH DE number 3872640 (Why is no real title available?)
• scientific article; zbMATH DE number 1222416 (Why is no real title available?)
• scientific article; zbMATH DE number 1158762 (Why is no real title available?)
• scientific article; zbMATH DE number 1497823 (Why is no real title available?)
• scientific article; zbMATH DE number 1761902 (Why is no real title available?)
• scientific article; zbMATH DE number 2086611 (Why is no real title available?)
• Prime factorizations of abstract domains using first-order logic
• Proof methods of declarative properties of definite programs
• Synthesis and transformation of logic programs using unfold/fold proofs

Cited in

(16)

• Inductive assertion method for logic pograms
• Verifying programs in the calculus of inductive constructions
• Abstract interpretation based verification of logic programs
• A dynamic logic for unstructured programs with embedded assertions
• scientific article; zbMATH DE number 4037276 (Why is no real title available?)
• scientific article; zbMATH DE number 1222416 (Why is no real title available?)
• scientific article; zbMATH DE number 1497823 (Why is no real title available?)
• Logic programs as specifications in the inductive verification of logic programs
• Verifying Tight Logic Programs with anthem and vampire
• Logic Programming
• Verification from Declarative Specifications Using Logic Programming
• Inductive assertions and operational semantics
• Deductive verification in decidable fragments with Ivy
• An integrated framework for the diagnosis and correction of rule-based programs
• ``A la Burstall intermittent assertions induction principles for proving inevitability properties of programs
• Inductive expansion: A calculus for verifying and synthesizing functional and logic programs

This page was built for publication: Assertion based inductive verification methods for logic programs

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