ADCL: Acceleration Driven Clause Learning for Constrained Horn Clauses
Constrained Horn Clauses (CHCs) are often used in automated program verification. Thus, techniques for (dis-)proving satisfiability of CHCs are a very active field of research. On the other hand, acceleration techniques for computing formulas that characterize the N-fold closure of loops have successfully been used for static program analysis. We show how to use acceleration to avoid repeated derivations with recursive CHCs in resolution proofs, which reduces the length of the proofs drastically. This idea gives rise to a novel calculus for (dis)proving satisfiability of CHCs, called Acceleration Driven Clause Learning (ADCL). We implemented this new calculus in the tool LoAT and evaluate it empirically in comparison to other state-of-the-art tools.
Tue 24 OctDisplayed time zone: Lisbon change
09:00 - 10:30 | Cost/precision trade-offs and accelerationSAS 2023 at Room I Chair(s): Xavier Rival Inria; ENS; CNRS; PSL University | ||
09:00 30mTalk | ADCL: Acceleration Driven Clause Learning for Constrained Horn Clauses SAS 2023 Pre-print | ||
09:30 30mTalk | Unconstrained Variable Oracles for Faster Static Analyses SAS 2023 Vincenzo Arceri University of Parma, Italy, Greta Dolcetti University of Parma - Department of Mathematical, Physical, and Computer Sciences, Enea Zaffanella University of Parma, Italy Pre-print | ||
10:00 30mTalk | Modular Optimization-Based Roundoff Error Analysis of Floating-Point Programs SAS 2023 Pre-print |