2015/12/06 by Alexei Lisitsa, Alexei P. Lisitsa, Andrei P. Nemytykh · 2 citations
Computer Science · #Algorithm #Artificial intelligence #Computer science #Consistency (knowledge bases) #Formal Methods in Verification #Formal methods #Model checking #Model transformation #Operational semantics #Partial evaluation #Program analysis #Program transformation #Programming language #Reachability #Security and Verification in Computing #Semantics (computer science) #Software Reliability and Analysis Research #Theoretical computer science #Transformation (genetics) #cs.PL #cs.SE
paper · pdf · doi:10.4204/eptcs.199.2
published in Electronic Proceedings in Theoretical Computer Science 199, 15-32 (Open Publishing Association) · In Proceedings VPT 2015, arXiv:1512.02215
openalex publication_date 2015/12/06 · arxiv created 2015/12/12 · arxiv updated 2015/12/15 · openalex created_date 2025/10/10 · openalex updated_date 2026/08/05
Both automatic program verification and program transformation are based on program analysis. In the past decade a number of approaches using various automatic general-purpose program transformation techniques (partial deduction, specialization, supercompilation) for verification of unreachability properties of computing systems were introduced and demonstrated. On the other hand, the semantics based unfold-fold program transformation methods pose themselves diverse kinds of reachability tasks and try to solve them, aiming at improving the semantics tree of the program being transformed. That means some general-purpose verification methods may be used for strengthening program transformation techniques. This paper considers the question how finite countermodels for safety verification method might be used in Turchin's supercompilation method. We extract a number of supercompilation sub-algorithms trying to solve reachability problems and demonstrate use of an external countermodel finder for solving some of the problems.