A formal framework for synthesis and verification of logic programs

DOI10.1007/3-540-45142-0_1MaRDI QIDQ4421867zbMATH OpenFDO

Authors Alessandro Avellone, Mauro Ferrari, Camillo Fiorentini

Publication date 1 September 2003

Published in Lecture Notes in Computer Science (Search for Journal in Brave)

Full work available at URL http://link.springer.de/link/service/series/0558/bibs/2042/20420001.htm

Mathematics Subject Classification ID

Logic programming (68N17) Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.) (68N30)

Recommendations

• Proofs and programs: A naïve approach to program extraction
• scientific article; zbMATH DE number 4187141
• Logic program synthesis from incomplete specifications
• Program extraction in simply-typed higher order logic
• scientific article; zbMATH DE number 4147469

Cited in

(14)

• Synthesis of positive logic programs for checking a class of definitions with infinite quantification
• Extracting information from intermediate semiconstructive HA-systems -- extended abstract
• Logics and automata for verification: Expressiveness and decidability issues
• On verification in logic database languages
• scientific article; zbMATH DE number 5850099 (Why is no real title available?)
• scientific article; zbMATH DE number 4180832 (Why is no real title available?)
• scientific article; zbMATH DE number 4139316 (Why is no real title available?)
• scientific article; zbMATH DE number 5718039 (Why is no real title available?)
• scientific article; zbMATH DE number 877748 (Why is no real title available?)
• scientific article; zbMATH DE number 1406236 (Why is no real title available?)
• Verifying Tight Logic Programs with anthem and vampire
• Verification from Declarative Specifications Using Logic Programming
• scientific article; zbMATH DE number 4187141 (Why is no real title available?)
• A verified VCGen based on dynamic logic: an exercise in meta-verification with Why3

This page was built for publication: A formal framework for synthesis and verification of logic programs

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