Verification of Imperative Programs by Constraint Logic Program Transformation

This paper studies the problem of removing unused arguments from logic programs which have been constructed by a schema-based method. Our schema-based method constructs logic programs semi-automatically. These programs have clear structure which depicts the design decisions that have been taken for their construction. On the other hand, these programs have unused arguments. We propose a method that automatically removes the unused arguments from such programs. This method is based on fold-unfold transformations. We have developed a tool which implements our method and evaluates the initial and the transformed programs. This logic program transformation tool is presented as well.

Download Full-text

Speedup of logic programs by binarization and partial deduction

Theory and Practice of Logic Programming ◽

10.1017/s147106840300190x ◽

2004 ◽

Vol 4 (3) ◽

pp. 355-369

Author(s):

JAN HRŮZA ◽

PETER šTĚPÁNEK

Keyword(s):

Program Transformation ◽

Logic Program ◽

Logic Programs ◽

Binary Logic ◽

Partial Deduction ◽

Binary Program ◽

Binary Programs

Binary logic programs can be obtained from ordinary logic programs by a binarizing transformation. In most cases, binary programs obtained this way are less efficient than the original programs. (Demoen, 1992) showed an interesting example of a logic program whose computational behaviour was improved when it was transformed to a binary program and then specialized by partial deduction. The class of B-stratifiable logic programs is defined. It is shown that for every B-stratifiable logic program, binarization and subsequent partial deduction produce a binary program which does not contain variables for continuations introduced by binarization. Such programs usually have a better computational behaviour than the original ones. Both binarization and partial deduction can be easily automated. A comparison with other related approaches to program transformation is given.

Download Full-text

Using call/exit analysis for logic program transformation

Logic Program Synthesis and Transformation — Meta-Programming in Logic - Lecture Notes in Computer Science ◽

10.1007/3-540-58792-6_3 ◽

1994 ◽

pp. 36-50

Author(s):

Dmitri Boulanger ◽

Maurice Bruynooghe

Keyword(s):

Program Transformation ◽

Logic Program ◽

Exit Analysis

Download Full-text

Preservation of stronger equivalence in unfold/fold logic program transformation

Theoretical Computer Science ◽

10.1016/0304-3975(90)90065-p ◽

1990 ◽

Vol 75 (1-2) ◽

pp. 139-156 ◽

Cited By ~ 20

Author(s):

Tadashi Kawamura ◽

Tadashi Kanamori

Keyword(s):

Program Transformation ◽

Logic Program

Download Full-text

Call for Papers Verification and Computational Logic Special Issue of Theory and Practice of Logic Programming

Theory and Practice of Logic Programming ◽

10.1017/s1471068401001089 ◽

2001 ◽

Vol 1 (5) ◽

pp. 631-632

Author(s):

Michael Leuschel ◽

Andreas Podelski ◽

C. R. Ramakrishnan ◽

Ulrich Ultes-Nitsche

Keyword(s):

Model Checking ◽

Logic Programming ◽

Program Analysis ◽

Program Transformation ◽

Logic Program ◽

Theory And Practice ◽

Special Issue ◽

High Quality Research ◽

Programming Techniques ◽

Verification Techniques

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).

Download Full-text