Horn clauses as an intermediate representation for program analysis and transformation

DOI10.1017/S1471068415000204zbMath1379.68089arXiv1507.05762WikidataQ57664991 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 transformation; program analysis; compilers; SSA; intermediate representation; control flow graphs

Mathematics Subject Classification ID

68N20: Theory of compilers and interpreters

68N17: Logic programming

Related Items

Introduction to the special issue on computational logic for verification, Anti-unification in Constraint Logic Programming, Concolic Testing in CLP, A complete refinement procedure for regular separability of context-free languages

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