Logic programs as specifications in the inductive verification of logic programs

DOI10.1016/S1571-0661(04)00153-7MaRDI QIDQ4923522zbMATH OpenOpenAlexFDO

Authors Roberta Gori, Marco Comini, Giorgio Levi

Publication date 24 May 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(04)00153-7

zbMATH Keywords

abstract interpretationinductive verificationtransformation of logic programs

Mathematics Subject Classification ID

Logic programming (68N17) Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.) (68N30) Specification and verification (program logics, model checking, etc.) (68Q60)

Recommendations

• Assertion based inductive verification methods for logic programs
• scientific article; zbMATH DE number 4037276
• Inductive assertion method for logic pograms
• Verification of logic programs
• Abstract interpretation based verification of logic programs

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 1222406 (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?)
• Synthesis and transformation of logic programs using unfold/fold proofs
• Systematic design of program transformation frameworks by abstract interpretation

Cited in

(26)

• Inductive assertion method for logic pograms
• Weak second order characterizations of various program verification systems
• Verifying programs in the calculus of inductive constructions
• A new technique for verifying and correcting logic programs
• A new approach to program verification
• Automatic constrained rewriting induction towards verifying procedural programs
• Inductive completeness of logics of programs
• Declarative debugging of functional logic programs
• A dynamic logic for unstructured programs with embedded assertions
• scientific article; zbMATH DE number 1822431 (Why is no real title available?)
• A complete proof for the correctness of programs with new specification language
• scientific article; zbMATH DE number 4037276 (Why is no real title available?)
• scientific article; zbMATH DE number 4047053 (Why is no real title available?)
• Verification of logic programs
• scientific article; zbMATH DE number 1867306 (Why is no real title available?)
• Assertion based inductive verification methods for logic programs
• Verification of imperative programs by constraint logic program transformation
• Modules and specifications
• Verifying procedural programs via constrained rewriting induction
• scientific article; zbMATH DE number 5263431 (Why is no real title available?)
• Verification from Declarative Specifications Using Logic Programming
• Inductive assertions and operational semantics
• Integrated Formal Methods
• Inductive expansion: A calculus for verifying and synthesizing functional and logic programs
• Proving program inclusion using Hoare's logic
• Verification conditions are code

This page was built for publication: Logic programs as specifications in the inductive verification of logic programs

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