APLAS 2023
Sun 26 - Wed 29 November 2023 Taipei, Taiwan
Tue 28 Nov 2023 16:30 - 17:00 at Room 106 & 107, IIS - Verification Chair(s): Zhong Shao

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 Nov

Displayed time zone: Beijing, Chongqing, Hong Kong, Urumqi change

15:30 - 17:00
VerificationAPLAS 2023 at Room 106 & 107, IIS
Chair(s): Zhong Shao Yale University
15:30
30m
Talk
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
30m
Talk
Transport via Partial Galois Connections and Equivalences
APLAS 2023
Kevin Kappelmann Technical University of Munich
16:30
30m
Talk
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