Chronosymbolic

Abstract

Constrained Horn Clause (CHC) is a universal format for formal verification problems. It is of great importance because it is expressive enough for any imperative programs written in different programming languages and any specifications to verify, and its solution leads to the correctness of the program. There are a plethora of methods that mainly leverages two distinct styles of techniques: symbolic reasoning and data learning (or equivalently, white-box and black-box methods). Symbolic reasoning-based methods are efficient due to many years of heuristic tuning, but struggle to capture the global information of CHCs; data-driven methods, contrarily, excel at making induction from globally collected data, but fail to leverage the abundant prior information. We propose a novel framework for efficient CHC solving, “Chronosymbolic Learning”, which provides fundamentals to unify symbolic-reasoning-based and data-driven approaches synergistically. We also provide an instance of Chronosymbolic Learning. Despite its relative simplicity, experimental results show the efficacy and robustness of our tool.