Horn clauses as an intermediate representation for program analysis and transformation
From MaRDI portal
Publication:4592995
DOI10.1017/S1471068415000204zbMATH Open1379.68089arXiv1507.05762OpenAlexW3098190183WikidataQ57664991 ScholiaQ57664991MaRDI QIDQ4592995FDOQ4592995
Authors: Graeme Gange, Jorge Navas, Peter Schachte, Harald Søndergaard, Peter J. Stuckey 
Publication date: 9 November 2017
Published in: Theory and Practice of Logic Programming (Search for Journal in Brave)
Abstract: Many 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.
Full work available at URL: https://arxiv.org/abs/1507.05762
Recommendations
- Analysis and Transformation of Constrained Horn Clauses for Program Verification
- Horn clause solvers for program verification
- scientific article; zbMATH DE number 1761889
- A compositional semantic basis for the analysis of equational Horn programs
- HORNLOG: A graph-based interpreter for general Horn clauses
- Combining forward and backward abstract interpretation of Horn clauses
- Approximating Term Rewriting Systems: A Horn Clause Specification and Its Implementation
- Horn clause programs with polymorphic types: Semantics and resolution
- scientific article; zbMATH DE number 1761432
Cites Work
- The octagon abstract domain
- Computer aided verification. 24th international conference, CAV 2012, Berkeley, CA, USA, July 7--13, 2012. Proceedings
- Tools and algorithms for the construction and analysis of systems. 20th international conference, TACAS 2014, held as part of the European joint conferences on theory and practice of software, ETAPS 2014, Grenoble, France, April 5--13, 2014. Proceedings
- Cost analysis of object-oriented bytecode programs
- Computer aided verification. 23rd international conference, CAV 2011, Snowbird, UT, USA, July 14--20, 2011. Proceedings
- The execution algorithm of mercury, an efficient purely declarative logic programming language
- Static analysis. 5th international symposium, SAS '98, Pisa, Italy, September 14--16, 1998. Proceedings
- Title not available (Why is that?)
- Programming Languages and Systems
Cited In (12)
- A complete refinement procedure for regular separability of context-free languages
- Generalization-Driven Semantic Clone Detection in CLP
- Case-free programs: An abstraction of definite horn programs
- Concolic Testing in CLP
- Analysis and Transformation of Constrained Horn Clauses for Program Verification
- Anti-unification in Constraint Logic Programming
- A Flexible, (C)LP-Based Approach to the Analysis of Object-Oriented Programs
- Title not available (Why is that?)
- Introduction to the special issue on computational logic for verification
- Language-independent generation of logic representations for programs
- Symbolic Model Construction for Saturated Constrained Horn Clauses
- A compositional semantic basis for the analysis of equational Horn programs
Uses Software
This page was built for publication: Horn clauses as an intermediate representation for program analysis and transformation
Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q4592995)
