2015/07/01 by GRAEME GANGE, Graeme Gange, JORGE A. NAVAS +7
Computer Science · #Formal Methods in Verification #Horn clause #Logic program #Logic programming #Logic, Reasoning, and Knowledge #Logic, programming, and type systems #Program analysis #Program transformation #Representation (politics) #Semantics (computer science) #Simple (philosophy) #Transformation (genetics) #cs.PL
paper · pdf · doi:10.1017/s1471068415000204
published as Theory and Practice of Logic Programming 15 (2015) 526-542 · To Appear in Theory and Practice of Logic Programming (TPLP), Proceedings of ICLP 2015
openalex publication_date 2015/07/01 · arxiv created 2015/07/21 · openalex created_date 2016/06/24 · arxiv updated 2020/02/19 · openalex updated_date 2026/08/05
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.