scholarly journals Horn clauses as an intermediate representation for program analysis and transformation

2015 ◽  
Vol 15 (4-5) ◽  
pp. 526-542 ◽  
Author(s):  
GRAEME GANGE ◽  
JORGE A. NAVAS ◽  
PETER SCHACHTE ◽  
HARALD SØNDERGAARD ◽  
PETER J. STUCKEY
Keyword(s):  
Program Analysis ◽  
Logic Program ◽  
Machine Language ◽  
Intermediate Representation ◽  
Logic Programs ◽  
Low Level ◽  
Horn Clauses ◽  
Program Representation ◽  
Compilation Process

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.

scholarly journals Effects of Program Representation on Pointer Analyses — An Empirical Study

2021 ◽  
pp. 240-261
Author(s):  
Jyoti Prakash ◽  
Abhishek Tiwari ◽  
Christian Hammer
Keyword(s):  
Empirical Study ◽  
Static Analysis ◽  
Program Analysis ◽  
Intermediate Representation ◽  
Pointer Analysis ◽  
Class Hierarchy ◽  
Program Representation ◽  
The Impact

AbstractStatic analysis frameworks, such as Soot and Wala, are used by researchers to prototype and compare program analyses. These frameworks vary on heap abstraction, modeling library classes, and underlying intermediate program representation (IR). Often, these variations pose a threat to the validity of the results as the implications of comparing the same analysis implementation in different frameworks are still unexplored. Earlier studies have focused on the precision, soundness, and recall of the algorithms implemented in these frameworks; however, little to no work has been done to evaluate the effects of program representation. In this work, we fill this gap and study the impact of program representation on pointer analysis. Unfortunately, existing metrics are insufficient for such a comparison due to their inability to isolate each aspect of the program representation. Therefore, we define two novel metrics that measure these analyses’ precision after isolating the influence of class-hierarchy and intermediate representation. Our results establish that the minor differences in the class hierarchy and IR do not impact program analysis significantly. Besides, they reveal the sources of unsoundness that aid researchers in developing program analysis.

scholarly journals Truth versus information in logic programming

2013 ◽  
Vol 14 (6) ◽  
pp. 803-840 ◽  
Author(s):  
LEE NAISH ◽  
HARALD SØNDERGAARD
Keyword(s):  
Logic Programming ◽  
Program Analysis ◽  
Logic Program ◽  
Logic Programs ◽  
Intended Meaning ◽  
Truth Values ◽  
The Third ◽  
Multiple Valued Logic ◽  
Truth Value ◽  
Semantics Of Logic Programs

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.

Y-Logic: A Framework for Reasoning About Chameleonic Programs with Inconsistent Completions

1990 ◽  
Vol 13 (4) ◽  
pp. 465-483
Author(s):  
V.S. Subrahmanian
Keyword(s):  
Classical Logic ◽  
Logic Program ◽  
Logic Programs ◽  
Large Subset ◽  
General Logic ◽  
Traditional Sense

Large logic programs are normally designed by teams of individuals, each of whom designs a subprogram. While each of these subprograms may have consistent completions, the logic program obtained by taking the union of these subprograms may not. However, the resulting program still serves a useful purpose, for a (possibly) very large subset of it still has a consistent completion. We argue that “small” inconsistencies may cause a logic program to have no models (in the traditional sense), even though it still serves some useful purpose. A semantics is developed in this paper for general logic programs which ascribes a very reasonable meaning to general logic programs irrespective of whether they have consistent (in the classical logic sense) completions.

scholarly journals Characterization of logic program revision as an extension of propositional revision

2015 ◽  
Vol 16 (1) ◽  
pp. 111-138 ◽  
Author(s):  
NICOLAS SCHWIND ◽  
KATSUMI INOUE
Keyword(s):  
Logic Program ◽  
Nonmonotonic Reasoning ◽  
Knowledge Representation And Reasoning ◽  
Logic Programs ◽  
Characterization Result ◽  
International Conference ◽  
Complete Procedure ◽  
Boolean Lattices ◽  
Computational Properties

AbstractWe address the problem of belief revision of logic programs (LPs), i.e., how to incorporate to a LP P a new LP Q. Based on the structure of SE interpretations, Delgrande et al. (2008. Proc. of the 11th International Conference on Principles of Knowledge Representation and Reasoning (KR'08), 411–421; 2013b. Proc. of the 12th International Conference on Logic Programming and Nonmonotonic Reasoning (LPNMR'13), 264–276) adapted the well-known AGM framework (Alchourrón et al. 1985. Journal of Symbolic Logic 50, 2, 510–530) to LP revision. They identified the rational behavior of LP revision and introduced some specific operators. In this paper, a constructive characterization of all rational LP revision operators is given in terms of orderings over propositional interpretations with some further conditions specific to SE interpretations. It provides an intuitive, complete procedure for the construction of all rational LP revision operators and makes easier the comprehension of their semantic and computational properties. We give a particular consideration to LPs of very general form, i.e., the generalized logic programs (GLPs). We show that every rational GLP revision operator is derived from a propositional revision operator satisfying the original AGM postulates. Interestingly, the further conditions specific to GLP revision are independent from the propositional revision operator on which a GLP revision operator is based. Taking advantage of our characterization result, we embed the GLP revision operators into structures of Boolean lattices, that allow us to bring to light some potential weaknesses in the adapted AGM postulates. To illustrate our claim, we introduce and characterize axiomatically two specific classes of (rational) GLP revision operators which arguably have a drastic behavior. We additionally consider two more restricted forms of LPs, i.e., the disjunctive logic programs (DLPs) and the normal logic programs (NLPs) and adapt our characterization result to disjunctive logic program and normal logic program revision operators.

Chapter 20. Software Verification

2021 ◽  
Author(s):  
Daniel Kroening
Keyword(s):  
Program Analysis ◽  
Software Verification ◽  
Embedded Software ◽  
Propositional Satisfiability ◽  
Low Level

This chapter covers an application of propositional satisfiability to program analysis. We focus on the discovery of programming flaws in low-level programs, such as embedded software. The loops in the program are unwound together with a property to form a formula, which is then converted into CNF. The method supports low-level programming constructs such as bit-wise operators or pointer arithmetic.

scholarly journals A backward analysis for constraint logic programs

2002 ◽  
Vol 2 (4-5) ◽  
pp. 517-547 ◽  
Author(s):  
ANDY KING ◽  
LUNJIN LU
Keyword(s):  
Ad Hoc ◽  
Abstract Interpretation ◽  
Logic Program ◽  
Control Flow ◽  
Third Party ◽  
Logic Programs ◽  
Abstract Domains ◽  
Constraint Logic Programs ◽  
Backward Analysis ◽  
Computational Properties

One recurring problem in program development is that of understanding how to re-use code developed by a third party. In the context of (constraint) logic programming, part of this problem reduces to figuring out how to query a program. If the logic program does not come with any documentation, then the programmer is forced to either experiment with queries in an ad hoc fashion or trace the control-flow of the program (backward) to infer the modes in which a predicate must be called so as to avoid an instantiation error. This paper presents an abstract interpretation scheme that automates the latter technique. The analysis presented in this paper can infer moding properties which if satisfied by the initial query, come with the guarantee that the program and query can never generate any moding or instantiation errors. Other applications of the analysis are discussed. The paper explains how abstract domains with certain computational properties (they condense) can be used to trace control-flow backward (right-to-left) to infer useful properties of initial queries. A correctness argument is presented and an implementation is reported.

scholarly journals Logic + control: On program construction and verification

2017 ◽  
Vol 18 (1) ◽  
pp. 1-29
Author(s):  
WŁODZIMIERZ DRABENT
Keyword(s):  
Logic Program ◽  
Practical Importance ◽  
Operational Semantics ◽  
Program Transformations ◽  
Logic Programs ◽  
Formal Reasoning ◽  
Prolog Program ◽  
Logic Control ◽  
Sat Solver ◽  
Program Construction

AbstractThis paper presents an example of formal reasoning about the semantics of a Prolog program of practical importance (the SAT solver of Howe and King). The program is treated as a definite clause logic program with added control. The logic program is constructed by means of stepwise refinement, hand in hand with its correctness and completeness proofs. The proofs are declarative – they do not refer to any operational semantics. Each step of the logic program construction follows a systematic approach to constructing programs which are provably correct and complete. We also prove that correctness and completeness of the logic program is preserved in the final Prolog program. Additionally, we prove termination, occur-check freedom and non-floundering.Our example shows how dealing with “logic” and with “control” can be separated. Most of the proofs can be done at the “logic” level, abstracting from any operational semantics.The example employs approximate specifications; they are crucial in simplifying reasoning about logic programs. It also shows that the paradigm of semantics-preserving program transformations may be not sufficient. We suggest considering transformations which preserve correctness and completeness with respect to an approximate specification.

Sign in / Sign up

Export Citation Format

Share Document