An engine for logic program analysis

Author(s):  
N. Heintze ◽  
J. Jaffar
1998 ◽  
Vol 35 (1) ◽  
pp. 1-37 ◽  
Author(s):  
Maria García de la Banda ◽  
Kim Marriott ◽  
Peter Stuckey ◽  
Harald Søndergaard

2015 ◽  
Vol 15 (4-5) ◽  
pp. 526-542 ◽  
Author(s):  
GRAEME GANGE ◽  
JORGE A. NAVAS ◽  
PETER SCHACHTE ◽  
HARALD SØNDERGAARD ◽  
PETER J. STUCKEY

AbstractMany recent analyses for conventional imperative programs begin by transforming programs into logic programs, capitalising on existing LP analyses and simple LP semantics. We propose using logic programs as an intermediate program representation throughout the compilation process. With restrictions ensuring determinism and single-modedness, a logic program can easily be transformed to machine language or other low-level language, while maintaining the simple semantics that makes it suitable as a language for program analysis and transformation. We present a simple LP language that enforces determinism and single-modedness, and show that it makes a convenient program representation for analysis and transformation.


2013 ◽  
Vol 14 (6) ◽  
pp. 803-840 ◽  
Author(s):  
LEE NAISH ◽  
HARALD SØNDERGAARD

AbstractThe semantics of logic programs was originally described in terms of two-valued logic. Soon, however, it was realised that three-valued logic had some natural advantages, as it provides distinct values not only for truth and falsehood but also for “undefined”. The three-valued semantics proposed by Fitting (Fitting, M. 1985. A Kripke–Kleene semantics for logic programs. Journal of Logic Programming 2, 4, 295–312) and Kunen (Kunen, K. 1987. Negation in logic programming. Journal of Logic Programming 4, 4, 289–308) are closely related to what is computed by a logic program, the third truth value being associated with non-termination. A different three-valued semantics, proposed by Naish, shared much with those of Fitting and Kunen but incorporated allowances for programmer intent, the third truth value being associated with underspecification. Naish used an (apparently) novel “arrow” operator to relate the intended meaning of left and right sides of predicate definitions. In this paper we suggest that the additional truth values of Fitting/Kunen and Naish are best viewed as duals. We use Belnap's four-valued logic (Belnap, N. D. 1977. A useful four-valued logic. In Modern Uses of Multiple-Valued Logic, J. M. Dunn and G. Epstein, Eds. D. Reidel, Dordrecht, Netherlands, 8–37), also used elsewhere by Fitting, to unify the two three-valued approaches. The truth values are arranged in a bilattice, which supports the classical ordering on truth values as well as the “information ordering”. We note that the “arrow” operator of Naish (and our four-valued extension) is essentially the information ordering, whereas the classical arrow denotes the truth ordering. This allows us to shed new light on many aspects of logic programming, including program analysis, type and mode systems, declarative debugging and the relationships between specifications and programs, and successive execution states of a program.


2001 ◽  
Vol 1 (5) ◽  
pp. 631-632
Author(s):  
Michael Leuschel ◽  
Andreas Podelski ◽  
C. R. Ramakrishnan ◽  
Ulrich Ultes-Nitsche

Submission deadline: January 10, 2002The past decade has seen dramatic growth in the application of model checking techniques to the validation and verification of correctness properties of hardware, and more recently software systems. One of the methods is to model a hardware or software system as a finite, labelled transition system which is then exhaustively explored to decide whether a given temporal specification holds. Recently, there has been increasing interest in applying logic programming techniques to model checking in particular and verification in general. For example, table-based logic programming can be used as an efficient means of performing explicit model checking. Other research has successfully exploited set-based logic program analysis, constraint logic programming, and logic program transformation techniques.The aim of this special issue is to attract high-quality research papers on the interplay between verification techniques (e.g. model checking, reduction and abstraction) and logic programming techniques (e.g. constraints, abstract interpretation, program transformation).


Sign in / Sign up

Export Citation Format

Share Document