Verification of logic programs
Copyright policy )Verification of logic programs
Summary: We present a proof method in the style of Hoare's logic, aimed at providing a unifying framework for the verification of total correctness of logic and Prolog programs. The method, which relies on purely declarative reasoning, has been designed as a trade-off between expressiveness and ease of use. On the basis of a few simple principles, we reason uniformly on several properties of logic and Prolog programs, including partial correctness, call patterns, absence of run-time errors, safe omission of the occur-check, computed instances, termination and modular program development. We finally generalize the method to general programs.
- Università degli studi di Salerno Italy
- University of Pisa Italy
Specification and verification (program logics, model checking, etc.), Logic, Proof theory, Verification, Logic programming, Partial correctness, Prolog programs, Logic programs, Prolog, Correctness, Total correctness
Specification and verification (program logics, model checking, etc.), Logic, Proof theory, Verification, Logic programming, Partial correctness, Prolog programs, Logic programs, Prolog, Correctness, Total correctness
citations This is an alternative to the "Influence" indicator, which also reflects the overall/total impact of an article in the research community at large, based on the underlying citation network (diachronically).15 popularity This indicator reflects the "current" impact/attention (the "hype") of an article in the research community at large, based on the underlying citation network.Average influence This indicator reflects the overall/total impact of an article in the research community at large, based on the underlying citation network (diachronically).Top 10% impulse This indicator reflects the initial momentum of an article directly after its publication, based on the underlying citation network.Top 10%
Citations provided by BIP!Popularity provided by BIP!