Horn clauses as an intermediate representation for program analysis and transformation
From MaRDI portal
(Redirected from Publication:4592995)
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.
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
- scientific article; zbMATH DE number 1956554 (Why is no real title available?)
- Computer aided verification. 23rd international conference, CAV 2011, Snowbird, UT, USA, July 14--20, 2011. Proceedings
- Computer aided verification. 24th international conference, CAV 2012, Berkeley, CA, USA, July 7--13, 2012. Proceedings
- Cost analysis of object-oriented bytecode programs
- Programming Languages and Systems
- Static analysis. 5th international symposium, SAS '98, Pisa, Italy, September 14--16, 1998. Proceedings
- The execution algorithm of mercury, an efficient purely declarative logic programming language
- The octagon abstract domain
- 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
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
- Analysis and Transformation of Constrained Horn Clauses for Program Verification
- A Flexible, (C)LP-Based Approach to the Analysis of Object-Oriented Programs
- Concolic testing in CLP
- scientific article; zbMATH DE number 7453190 (Why is no real title available?)
- Introduction to the special issue on computational logic for verification
- Language-independent generation of logic representations for programs
- Anti-unification in constraint logic programming
- Symbolic Model Construction for Saturated Constrained Horn Clauses
- A compositional semantic basis for the analysis of equational Horn programs
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)
