SAS 2023
Sun 22 - Tue 24 October 2023 Cascais, Portugal
co-located with SPLASH 2023
Mon 23 Oct 2023 12:00 - 12:30 at Room I - Modular arithmetic and numeric analysis Chair(s): Daniel Kaestner

Weakly relational domains such as the Octagon domain have enjoyed tremendous success in the area of program analysis, since they offer a decent compromise between precision and efficiency. Octagons, in particular, have widely been studied to obtain efficient algorithms which, however, come with intricate correctness arguments. Here, we provide simplified cubic time algorithms for computing the closure of Octagon abstract relations both over the rationals and the integers which avoid introducing auxiliary variables. They are based on a more general formulation by means of 2-projective domains which allows for an elegant short correctness proof. The notion of 2-projectivity also lends itself to efficient algorithms for incremental normalization. For the Octagon domain, we also provide an improved construction for linear programming based best abstract transformers for affine assignments.

Mon 23 Oct

Displayed time zone: Lisbon change

11:00 - 12:30
Modular arithmetic and numeric analysisSAS 2023 at Room I
Chair(s): Daniel Kaestner AbsInt
11:00
30m
Talk
Symbolic transformation of expressions in modular arithmetic
SAS 2023
Jérôme Boillot École Normale Supérieure, PSL University & INRIA, Jerome Feret INRIA Paris
Pre-print
11:30
30m
Talk
Polynomial Analysis of Modular Arithmetic
SAS 2023
Thomas Seed University of Kent, Andy King Kent, Neil Evans AWE, Chris Coppins University of Kent
Pre-print
12:00
30m
Talk
Octagons Revisited - Elegant Proofs and Simplified Algorithms
SAS 2023
Michael Schwarz Technische Universität München, Helmut Seidl Technische Universität München
Pre-print