On the verification of finite failure

DOI10.1016/j.jcss.2005.06.001zbMath1105.68016MaRDI QIDQ2575838

Giorgio Levi, Roberta Gori

Publication date: 7 December 2005

Published in: Journal of Computer and System Sciences (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1016/j.jcss.2005.06.001

zbMATH Keywords

Logic programming; Abstract interpretation; Program verification; Finite failure

Mathematics Subject Classification ID

68Q60: Specification and verification (program logics, model checking, etc.)

68N17: Logic programming

Related Items

S-semantics for logic programming: a retrospective look

Cites Work

• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Inductive assertion method for logic pograms
• Compositionality properties of SLD-derivations
• Reasoning about prolog programs: From modes through types to assertions
• Enumeration of success patterns in logic programs
• A first-order language for expressing sharing and type properties of logic programs
• An abstract interpretation framework to reason on finite failure and other properties of finite and infinite computations.
• Error diagnosis in logic programming an adaptation of E.Y. Shapiro's method
• Contributions to the Theory of Logic Programming
• Abstract interpretation and application to logic programs
• The s-semantics approach: Theory and applications
• Finite failure is and-compositional
• Abstract diagnosis
• Systematic design of program transformation frameworks by abstract interpretation