Horn clauses as an intermediate representation for program analysis and transformation

DOI10.1017/S1471068415000204zbMath1379.68089arXiv1507.05762OpenAlexW3098190183WikidataQ57664991 ScholiaQ57664991MaRDI QIDQ4592995

Graeme Gange, Peter J. Stuckey, Peter Schachte, Harald Søndergaard, Jorge A. Navas

Publication date: 9 November 2017

Published in: Theory and Practice of Logic Programming (Search for Journal in Brave)

Full work available at URL: https://arxiv.org/abs/1507.05762

zbMATH Keywords

program transformationprogram analysiscompilersSSAintermediate representationcontrol flow graphs

Mathematics Subject Classification ID

Theory of compilers and interpreters (68N20) Logic programming (68N17)

Related Items

A complete refinement procedure for regular separability of context-free languages, Generalization-Driven Semantic Clone Detection in CLP, Analysis and Transformation of Constrained Horn Clauses for Program Verification, Anti-unification in Constraint Logic Programming, Unnamed Item, Concolic Testing in CLP, Introduction to the special issue on computational logic for verification

Uses Software

• Mercury
• TRACER
• UFO
• Threader
• VeriMAP

Cites Work

• Unnamed Item
• Computer aided verification. 24th international conference, CAV 2012, Berkeley, CA, USA, July 7--13, 2012. Proceedings
• Computer aided verification. 23rd international conference, CAV 2011, Snowbird, UT, USA, July 14--20, 2011. Proceedings
• Cost analysis of object-oriented bytecode programs
• The octagon abstract domain
• Static analysis. 5th international symposium, SAS '98, Pisa, Italy, September 14--16, 1998. 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
• The execution algorithm of mercury, an efficient purely declarative logic programming language
• Programming Languages and Systems