TY - GEN
T1 - Octagons Revisited
T2 - 30th International Symposium on Static Analysis, SAS 2023
AU - Schwarz, Michael
AU - Seidl, Helmut
N1 - Publisher Copyright:
© 2023, The Author(s), under exclusive license to Springer Nature Switzerland AG.
PY - 2023
Y1 - 2023
N2 - Weakly relational domains 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.
AB - Weakly relational domains 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.
KW - 2-decomposable relational domains
KW - Floyd-Warshall algorithm
KW - octagons
KW - weakly relational domains
UR - http://www.scopus.com/inward/record.url?scp=85175954197&partnerID=8YFLogxK
U2 - 10.1007/978-3-031-44245-2_21
DO - 10.1007/978-3-031-44245-2_21
M3 - Conference contribution
AN - SCOPUS:85175954197
SN - 9783031442445
T3 - Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
SP - 485
EP - 507
BT - Static Analysis - 30th International Symposium, SAS 2023, Proceedings
A2 - Hermenegildo, Manuel V.
A2 - Morales, José F.
PB - Springer Science and Business Media Deutschland GmbH
Y2 - 22 October 2023 through 24 October 2023
ER -