Analysis and Transformation of Constrained Horn Clauses for Program Verification

EMANUELE DE ANGELIS; FABIO FIORAVANTI; JOHN P. GALLAGHERMANUEL V. HERMENEGILDOALBERTO PETTOROSSIMAURIZIO PROIETTI

首页> 外文期刊>Theory and practice of logic programming >Analysis and Transformation of Constrained Horn Clauses for Program Verification

【24h】

Analysis and Transformation of Constrained Horn Clauses for Program Verification

机译：Analysis and Transformation of Constrained Horn Clauses for Program Verification

获取原文

掌桥外文数据库（机构版） >>

开具论文收录证明 >>

文献代查 >>

页面导航

摘要
著录项
相关主题

摘要

This paper surveys recent work on applying analysis and transformation techniques that originatein the field of constraint logic programming (CLP) to the problem of verifying softwaresystems. We present specialization-based techniques for translating verification problems for differentprogramming languages, and in general software systems, into satisfiability problems forconstrained Horn clauses (CHCs), a term that has become popular in the verification field to referto CLP programs. Then, we describe static analysis techniques for CHCs that may be used forinferring relevant program properties, such as loop invariants. We also give an overview of sometransformation techniques based on specialization and fold/unfold rules, which are useful forimproving the effectiveness of CHC satisfiability tools. Finally, we discuss future developmentsin applying these techniques.

著录项

来源
《Theory and practice of logic programming》 |2022年第6期|974-1042|共69页
作者
EMANUELE DE ANGELIS; FABIO FIORAVANTI; JOHN P. GALLAGHERMANUEL V. HERMENEGILDOALBERTO PETTOROSSIMAURIZIO PROIETTI;
展开▼
作者单位

CNR-IASI, Rome, Italy;

DEC, University ‘G. d’Annunzio’, Chieti-Pescara, Italy;

Roskilde University, Roskilde, Denmarkand IMDEA Software Institute, Madrid, SpainIMDEA Software Institute, Madrid, Spainand Universidad Politecnica de Madrid (UPM), Madrid, SpainCNR-IASI, Rome, Italyand DICII, University of Rome ‘Tor Vergata’, Rome, Italy;

展开▼
收录信息
原文格式 PDF
正文语种英语
中图分类
关键词
Program verification; program analysis; program transformation; constrained Horn clauses; constraint logic programming;

Analysis and Transformation of Constrained Horn Clauses for Program Verification

摘要

著录项

相关主题

期刊订阅