SAS 2023
Sun 22 - Tue 24 October 2023 Cascais, Portugal
co-located with SPLASH 2023
Tue 24 Oct 2023 09:00 - 09:30 at Room I - Cost/precision trade-offs and acceleration Chair(s): Xavier Rival

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 Oct

Displayed 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
30m
Talk
ADCL: Acceleration Driven Clause Learning for Constrained Horn Clauses
SAS 2023
Florian Frohn RWTH Aachen University, Jürgen Giesl RWTH Aachen University
Pre-print
09:30
30m
Talk
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
30m
Talk
Modular Optimization-Based Roundoff Error Analysis of Floating-Point Programs
SAS 2023
Rosa Abbasi Boroujeni Max Planck Institute for Software Systems, Eva Darulova Uppsala University
Pre-print