| 09:00-10:00 |
SAT-Guided Gröbner Basis Methods for Arithmetic Circuit Verification (abstract) 60 min
1 TU Wien
|
| 10:00-10:30 |
An Eager Encoding of Array Summation Constraints (abstract) 30 min
1 University of Regensburg
2 Uppsala University, University of Regensburg
ABSTRACT. The theory of arrays with select and store plays an important role in software verification and is therefore supported by virtually all state-of-the-art SMT solvers. There are many extensions, for instance by constant arrays, element-wise function applications, counting, or projections, that have been shown to preserve decidability. In recent work, a theory of arrays extended by constant arrays and sum predicates, called summation array logic (SAL), has been introduced and proven to be decidable in non-deterministic polynomial time. In SAL, it is possible to state assertions about the sum of all entries in a (finite or infinite) array of integers. This paper provides an eager approach to the satisfiability problem in SAL. The approach transforms a SAL formula to an equi-satisfiable formula in the theory of extensional arrays (extended with constant array operator), which can then be decided by an off-the-shelf SMT solver. The transformation produces a formula at most quadratic in the size of the input formula. Since there are no standard array benchmarks with sum constraints yet, the paper presents a new set of such benchmarks obtained by mutating existing SMT-LIB array benchmarks. The experiments show that the transformation-based decision procedure incurs only a relatively small overhead in terms of solving time. |
SMT — PROGRAM FOR FRIDAY, 24 JULY 2026
Friday, 24 July 2026
08:45-09:00
Welcome
SMT
Location:
C1.04
09:00-10:30
Invited Talk + Encodings
SMT
Location:
C1.04
10:00-11:00
Coffee Break
SMT
Location:
C1.04
11:00-12:30
MCSat & Nonlinear Arithmetic
SMT
Location:
C1.04
12:00-14:00
Lunch
SMT
Location:
C1.04
14:00-15:30
Decision Procedures & Automation
SMT
Location:
C1.04
15:30-16:30
Coffee Break
SMT
Location:
C1.04
16:00-17:30
Learning, LLMs & Counting
SMT
Location:
C1.04
Designed and Developed by EventKey | Copyright 2026 EventKey
Last updated: