Horn clauses as an intermediate representation for program analysis and transformation
From MaRDI portal
Publication:4592995
DOI10.1017/S1471068415000204zbMATH Open1379.68089arXiv1507.05762OpenAlexW3098190183WikidataQ57664991 ScholiaQ57664991MaRDI QIDQ4592995FDOQ4592995
Graeme Gange, Peter J. Stuckey, Peter Schachte, Harald Søndergaard, Jorge Navas
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
Cites Work
- Title not available (Why is that?)
- 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
- Programming Languages and Systems
Cited In (10)
- 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
- Title not available (Why is that?)
- Introduction to the special issue on computational logic for verification
- Symbolic Model Construction for Saturated Constrained Horn Clauses
- A compositional semantic basis for the analysis of equational Horn programs
Uses Software
Recommendations
- Title not available (Why is that?) 👍 👎
- Title not available (Why is that?) 👍 👎
- HORNLOG: A graph-based interpreter for general Horn clauses 👍 👎
- A compositional semantic basis for the analysis of equational Horn programs 👍 👎
- Horn clause programs with polymorphic types: Semantics and resolution 👍 👎
- Horn Clause Solvers for Program Verification 👍 👎
- Combining Forward and Backward Abstract Interpretation of Horn Clauses 👍 👎
- Approximating Term Rewriting Systems: A Horn Clause Specification and Its Implementation 👍 👎
- Analysis and Transformation of Constrained Horn Clauses for Program Verification 👍 👎
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)
