APLAS 2023 (series) / The 21st Asian Symposium on Programming Languages and Systems /
Argument Reduction of Constrained Horn Clauses Using Equality Constraints
Constrained Horn Clauses (CHCs) have recently been studied extensively studied as a common, uniform foundation for automated program verification. Various program verification problems have been shown to be reducible to CHC solving, and accordingly, CHC solvers have been developed by several research groups. We propose a new optimization method for CHC solving, which reduces the number of predicate arguments by finding (conditional) equality constraints among the predicate arguments. The optimization is especially effective for data-driven CHC solvers such as HoIce, as it significantly reduces the number of data required to infer a solution for CHCs. We have implemented our method and confirmed its effectiveness through experiments.
Tue 28 NovDisplayed time zone: Beijing, Chongqing, Hong Kong, Urumqi change
Tue 28 Nov
Displayed time zone: Beijing, Chongqing, Hong Kong, Urumqi change
15:30 - 17:00 | |||
15:30 30mTalk | Towards a Framework for Developing Verified Assemblers for the ELF Format APLAS 2023 Jinhua Wu Shanghai Jiao Tong University, Yuting Wang Shanghai Jiao Tong University, Meng Sun Shanghai Jiao Tong University, Xiangzhe Xu Purdue University, Yichen Song Shanghai Jiao Tong University DOI File Attached | ||
16:00 30mTalk | Transport via Partial Galois Connections and Equivalences APLAS 2023 Kevin Kappelmann Technical University of Munich | ||
16:30 30mTalk | Argument Reduction of Constrained Horn Clauses Using Equality Constraints APLAS 2023 Ryo Ikeda University of Tokyo, Ryosuke Sato University of Tokyo, Naoki Kobayashi University of Tokyo |