Minimal Comparison of Octagonal Abstract Domains Kenny Ballou
Elena Sherman
Computer Science and Engineering California State University San Marcos San Marcos, California, United States [email protected]
Computer Science Boise State University Boise, Idaho, United States [email protected]
arXiv:2606.15582v1 [cs.SE] 14 Jun 2026
Abstract
eliminates cases when an improvement in precision in one statement propagates through the entire computation. For example, in this sequence of statements 1:x = y + 2, 2:z = 2, 3:w = 4 - z using Zones increases precision after statement 1: but for the other two statements, Zones computes the same invariants as Intervals for the 𝑧 and 𝑤 part of abstract states. Yet, comparison of the entire states results in Zones being globally more precise. To effectively apply the minimal change algorithm [3], it is imperative to remove spurious dependencies between variables in a fully closed form of an abstract state. While previous work developed such an algorithm for Zones [3, 4], it cannot, however, be applied to Octagons because of the substantial differences in their state representations. Thus, in this work we present a novel algorithm for removing spurious dependencies for fully closed Octagon abstract states, which we describe in Section 3. Equipped with this new algorithm, we, in Section 4, perform extensive empirical evaluation on how comparing minimal changes of invariants impacts comparison of abstract domains within the context of DFA. We discuss related works in Section 5 and finally conclude with future works in Section 6.
Numerical abstract domains vary in their expressiveness; more expressive domains like Zones yield more precise invariants than Intervals. A comprehensive approach to selecting abstract domains is a minimal comparison of abstract states. However, to be effective, it requires abstract states to be free of spurious constraints. While previous work developed spurious constraint elimination for Zones, this work introduces a novel algorithm for eliminating such constraints for Octagons. We evaluate our approach by comparing the precision of 6,930 invariants from different abstract domains. Our results show that the minimal comparison reclassifies many invariants as equivalent, thus reducing the impact of Octagons’ expressiveness on invariant precision.
1
Introduction
The tradeoff between expressiveness and efficiency of different numerical abstract domains like Zones [23], Octagons [25] or Intervals, requires an understanding of the impact of precision loss when choosing a more efficient, but less expressive abstract domain. While related work [1, 7, 17, 22] establish relations between program structural characteristics and an appropriate abstract domain choice, this information alone is insufficient to comprehensively compare domains. Traditionally comparing two abstract domains, 𝐷 1 and 𝐷 2 , where the former is more precise than the latter, involves comparing their invariants 𝐼 1 and 𝐼 2 at the same program locations. If the invariants of 𝐷 1 dominate in precision then one concludes a high impact on precision gain if 𝐷 1 is selected. Other works [8, 15, 26], create a distance metric to compare states. However, in the context of data-flow analysis (DFA), previous work [3, 4] show that a novel minimal comparison technique gives more insights into the precision gain or loss when choosing 𝐷 1 or 𝐷 2 , respectively. The minimal comparison leverages the fact that at each computational step, DFA applies incremental changes to an abstract state, i.e., a transfer function only modifies a part of an abstract state. While other techniques use incrementality to improve performance [2, 12, 18], the line of work on minimal comparison uses incremental updates to identify the changed portion of the abstract state and hence, compare only the updated parts of the resulting invariants. This
2
Background
2.1
Zones
The Zones domain [23] represent predicates via a strict unit difference formula, extending the intervals domains with the form 𝑥 − 𝑦 ≤ 𝑐, where 𝑥 and 𝑦 are program variables, and 𝑐 is a numerical constant from one of {Z, Q, R}. Interval valued constraints are encoded by adding a special variable, typically denoted 𝑣 0 , such that its value is always zero. Thus, 𝑥 − 𝑣 0 ≤ 𝑏 =⇒ 𝑥 − 0 ≤ 𝑏 =⇒ 𝑥 ≤ 𝑏 and 𝑣 0 − 𝑥 ≤ −𝑎 =⇒ 0 − 𝑥 ≤ −𝑎 =⇒ 𝑥 ≥ 𝑎 are sufficient to encode the interval for 𝑥: 𝑥 ↦→ [𝑎, 𝑏]. Figure 1 depicts the directed weighted graph representation of a Zone domain for the interval constraints 𝑥 ↦→ 𝑡𝑜 [𝑎, 𝑏] ∧ 𝑦 ↦→ 𝑡𝑜 [𝑐, +∞). 2.2
Octagons
The Octagons domain extends the unit difference of Zones [23] by encoding unit constraints over program variables in the forms ±𝑥 ± 𝑦 ≤ 𝑐 and ±𝑥 ≤ 2𝑐. The symbols 𝑥, 𝑦 represent program variables, and 𝑐 is a numerical constant1 . To efficiently manipulate such constraints, researchers proposed 1 Our work focuses on integer constraints, but should easily extend to Q
PL’18, New York, NY, USA 2018.
and R since integers require additional care the others do not. 1
PL’18, January 01–03, 2018, New York, NY, USA
Kenny Ballou and Elena Sherman
b-c + 𝑥𝑖=0
b-a
𝑦 +𝑗=2
𝑦 -2b
b
-a
-a -
b
𝑥
-c
-2a
2b -a -b
𝑣0 𝑥𝚤¯−=1
(a) Fully closed graphical representation of an octagonal state.
Figure 1. Directed weighted graph representation of unitdifference constraints of a Zone abstract state.
+ 𝑥𝑖=0
𝑥+ 𝑥− 𝑦+ 𝑦−
𝑥 − 𝑦 ≤ 𝑐 {𝑥 + − 𝑦 + ≤ 𝑐 ∧ 𝑦 − − 𝑥 − ≤ 𝑐 𝑥 + 𝑦 ≤ 𝑐 {𝑥 + − 𝑦 − ≤ 𝑐 ∧ 𝑦 + − 𝑥 − ≤ 𝑐 −𝑥 − 𝑦 ≤ 𝑐 {𝑥 − − 𝑦 + ≤ 𝑐 ∧ 𝑦 − − 𝑥 + ≤ 𝑐 +
𝑦 𝚥−¯=3
b-a
𝑥𝚤¯−=1
𝑦 +𝑗=2
𝑦 𝚥−¯=3
0 2𝑏 𝑏 − 𝑎 +∞ 0 −𝑎 − 𝑏 +∞ 2𝑏 +∞ +∞ +∞ 0 −𝑎 − 𝑏 𝑏 − 𝑎 −2𝑎 0
(b) Isomorphic difference bounded matrix (DBM) representation of the same octagonal state.
−
𝑥 ≤ 𝑐 {𝑥 − 𝑥 ≤ 2𝑐 𝑥 ≥ 𝑐 {𝑥 − − 𝑥 + ≤ −2𝑐
Figure 3. Fully, strongly closed Octagons represented as a weighted, directed graphs and its equivalent representation as a difference bounded matrix (DBM). The state contains 𝑦 ≥ 𝑎 ∧ 𝑥 = 𝑏 as well as inferred constraints 𝑥 − 𝑦 ≤ 𝑏 + 𝑎 ∧ −𝑥 − 𝑦 ≤ 𝑎 − 𝑏. The double circles denote changed variables, dashed edges denote inferred edges through closure.
Figure 2. Standard encoding rules for converting program variable space predicates and converting them to octagonal variable space.
2.3
Symbolic Predicates Abstract Domain
For evaluating our comparison, we use a so-called symbolic predicate domain to represent an instance of an incomparable domain. The Symbolic Predicates abstract domain extends the well-known Predicates domain with arbitrary inequality formula. These inequalities are automatically inferred through the program’s transfer functions when performing Predicate analysis [28]. Furthermore, since these inequalities are arbitrary, they can add exact, relational information to the predetermined set of predicates. For example, using the Sign domain, interpreting the expression 𝑦 = −2𝑥, with an incoming state of 𝑥 → {−} ∧ 𝑦 → ⊤, becomes 𝑥 → {−} ∧ 𝑦 → {+}. Augmenting with symbolic information, the expression after computing its transfer function becomes 𝑥 → {−} ∧𝑦 → {+} ∧𝑦 = −2𝑥, a precise relational representation of the assignment. We simply use this domain as an instantiation of an incomparable domain to Octagons.
an encoding [9, 12, 25] where variables are translated to a pair of constraint nodes, denoted here as 𝑥 ± and 𝑦 ± , which can be expressed as a directed, weighted graph. The nodes of the graph represent the constraint variables, and the edge weight denotes the difference constraint between the variables. The direction of the edge represents the ordering of the formula. Moreover, the graphical representation has an isomorphic representation as a difference bounded matrix (DBM), denoted throughout as 𝑀. The standard Octagon encoding rules are shown in Figure 2. For example, consider the code snippet: if (y >= a){ x = b; . . . }, where a, b are constants and x, y are program variables. The graph and DBM in Figure 3 shows the octagonal encoding of the state on the true branch, i.e., 𝑦 ≥ 𝑎 { 𝑦 − − 𝑦 + ≤ −2𝑎 and 𝑥 = 𝑏 { 𝑥 + − 𝑥 − ≤ 2𝑏 ∧ 𝑥 − − 𝑥 + ≤ −2𝑏. After processing x = b, DFA modifies the state in Figure 3a, with the newly added constraints depicted in the highlighted box. We collect these newly added edges into a set, 𝑑𝑒, which represents the changed edges as it relates to the abstract state. In this case, the set 𝑑𝑒 is equal to the following {(𝑥 +, 𝑥 − , 2𝑏), (𝑥 − , 𝑥 +, −2𝑏)}, which is equivalent to the logical expression, 𝑥 + − 𝑥 − ≤ 2𝑏 ∧ 𝑥 − − 𝑥 + ≤ −2𝑏.
2.4
Additional Notations
While we use some common notation throughout this work, we define some of the notation for clarity. When using the matrix notation for DBMs, we often use index variables 𝑖, 𝑗, 𝚤¯, 𝚥¯. Previous work has used the latter two, to represent the “negative” dual of the former [9]. That is, we denote 2
Minimal Comparison of Octagonal Abstract Domains
PL’18, January 01–03, 2018, New York, NY, USA
variable pairs within the octagonal encoding using 𝑖 and 𝚤¯ for each real program variable such that 𝑖 ⊕ 𝚤¯ ≡ 1, where ⊕ is the exclusive or operator. Furthermore, we can recover any index’s pair by flipping operands: 𝑖 ⊕ 1 ≡ 𝚤¯. Thus, an edge between 𝑖 and 𝚤¯ represents the interval edges between a variable within an Octagon constraint system. Moreover, these notations are equivalent to the even/odd 2𝑖𝑥 and 2𝑖𝑥 +1, encoding described by Miné et al. [25]. 2.5
Algorithm 1 Identify minimally changed variables within an Octagon. Require: 𝑀 is strongly closed and 𝑑𝑒 be the set of changed arrows within 𝑀. 1: 𝑑𝑣 ← {} 2: for (𝑖, 𝑗) ∈ 𝑑𝑒 do 3: if 𝑖 ≡ 𝑗 ∨ IsIntervalValued (𝑖, 𝑗) then 4: 𝑑𝑣 ← 𝑑𝑣 ∪ {𝑖, 𝑗 } 5: else 6: 𝑑𝑣 ← 𝑑𝑣 ∪ {𝑖} 7: end if 8: end for 9: Δvars ← 𝑑𝑣 10: for 𝑣 ∈ 𝑑𝑣 do 11: Δvars ← Δvars ∪ {𝑖 |𝑖 ∈ {0 . . . 2𝑁 } ∧ 𝑀𝑣,𝑖 < +∞} {Select forward reachable variables} 12: Δvars ← Δvars ∪ {𝑖 |𝑖 ∈ {0 . . . 2𝑁 } ∧ 𝑀𝑖,𝑣 < +∞} {Select backward reachable variables} 13: end for
Spurious Constraints
The critical step of finding a minimal state change is to precisely identify all variables, Δ𝑣𝑎𝑟𝑠, affected by the newly added constraint 𝑑𝑒. To do so, previous work by Ballou and Sherman explores the neighborhood of the changed variables 𝑑𝑣 of 𝑑𝑒 within the graph [3]. In our example, the gray box includes all affected variables Δ𝑣𝑎𝑟𝑠, which in this case is only the changed variables 𝑑𝑣 since there are no edges connecting them to 𝑦 + and 𝑦 − . However, when an abstract state is in a canonical, fully closed form, those variables become connected through implicit constraints shown as dashed edges in Figure 3a, hence marking the variables 𝑦 ± as changed too. We call these edges spurious since they do not further constrain the bounded region, but also decrease the precision of finding a minimal state change. Since the fully closed form is imperative for running DFA, e.g., for comparing states, we propose a new algorithm for removing such spurious constraints in Octagon abstract states.
3
14: 15: return Δvars
Algorithm 2 Constraint reduction algorithm for Octagons Require: 𝑀 ≡ C(𝑀): 𝑀 is a fully closed Octagon matrix Ensure: (C ◦ R) (𝑀) ≡ 𝑀: The closure of the reduction is equivalent to 𝑀. 1: for all 𝑖 ∈ {0, . . . , 2𝑁 } do 2: for all 𝑗 ∈ {0, . . . , 2𝑁 } do 3: if 𝑖 ≡ 𝑗 ∨ IsIntervalValued (𝑖, 𝑗) then 4: continue 5: end if 𝑀 +𝑀 6: if 𝑀𝑖,𝑗 ≥ 𝑖,¯𝚤 2 𝚥¯,𝑗 then 7: 𝑀𝑖,𝑗 ← +∞ 8: end if 9: end for 10: end for
Minimal Comparison
Algorithm 1 extends the algorithm from previous work [3] to identify minimally changed variables Δvars when an abstract state 𝑀 ′ is updated to a new state 𝑀 after processing a set of constraints 𝑑𝑒, where each constraint contains a triple of variables (𝑖, 𝑗, 𝑤). After Δvars are identified, then only constraints containing those variables are selected for comparison. Thus, the smaller the set of changed variables that Algorithm 1 returns the more accurate the comparison. The algorithm takes the updated fully closed state encoded as a DBM 𝑀 and the constraint set 𝑑𝑒 associated with the update, where 𝑑𝑒 is the set of incoming, modified constraints. First, on lines 2–8, the algorithm iterates over each constraint to determine whether 𝑖 or 𝑗 indeed changed. Next, on lines 10–13, the algorithm finds variables that are affected by the directly updated variables 𝑑𝑣. Since 𝑀 is fully closed, it requires only one “forward” step and one “backward” step in the graph’s representation of 𝑀. Here 𝑁 denotes the number of program variables and |𝑀 | = 2𝑁 × 2𝑁 , as per standard Octagon encoding that doubles the variable space [25]. However, when applied to fully closed states, Algorithm 1 is ineffective in identifying minimal changes because such states contain many spurious constraints for variables that
encode interval values, similar to 𝑥 and 𝑦 from our example in Figure 3. That is, as part of the closure operation and necessary operation, many variables become spuriously connected. In our example, 𝑥 becomes spuriously coupled with 𝑦 in the constraint 𝑥 − 𝑦 ≤ 𝑏 + 𝑎. Algorithm 1 identifies 𝑥 and 𝑦 as part of the Δvars set and uses both for comparison, instead of just 𝑥. Therefore, we need a technique which removes these spurious constraints in 𝑀 before passing this DBM to Algorithm 1. We define a spurious constraint as a redundant constraint coupling variables within a DBM 𝑀. A positive-negative pair 3
PL’18, January 01–03, 2018, New York, NY, USA
Kenny Ballou and Elena Sherman
Table 1. Intervals and Zones vs Octagons invariants comparison
of variables within the octagonal DBM represent the interval bounds of a program variable, e.g., (𝑥𝑖+, 𝑥𝚤¯− , 2𝑏) ≡ 𝑥 ≤ 𝑏, where 𝑖 ⊕ 𝚤¯ ≡ 1; dually for the other direction. Due to the closure operations, pairs of variables become coupled in a constraint. However, if a constraint is a result of these interval constraint closures, then we label it as spurious. Formally, a constraint 𝑀𝑖,𝑗 in an Octagon matrix 𝑀 is spurious when the following two conditions hold:
Technique
𝐼 ≡𝑂
𝐼 ≺𝑂
𝑍 ≡𝑂
𝑍 ≺𝑂
Full Comparison
1523
5407
5138
1792
MN
3894
3036
6183
747
MN + Reduction
4439
2491
6527
403
1. 𝑖 ≠ 𝑗 ∧ 𝑖 ⊕ 𝑗 ≡1, and 2. 𝑀𝑖,𝑗 ≥ 𝑀𝑖,¯𝚤 + 𝑀 𝚥¯,𝑗 /2.
Table 2. Octagons and Symbolic Predicates
The first condition ensures that it is not itself an interval constraint. For example, we do not consider constraints such as 𝑀𝑖,¯𝚤 . The second condition checks that a constraint over two variables is less or equally constraining than its strong closure [25]. If this constraint is stronger, it is more restrictive than the interval values alone. Our novel Algorithm 2 removes spurious constraints for fully closed Octagons states, i.e., it removes all recoverable constraints. To do so, the algorithm iterates over all indices of the closed DBM 𝑀, lines 1–2, skipping interval valued constraints, line 3. Here, as before, 𝑁 is the number of program variables. In lines 6–7, if the constraint is spurious, the algorithm sets its value to +∞. The runtime for Algorithm 2 is 𝑂 (𝑁 2 ). Since the for loops are definite with increasing indices, assuredly the algorithm terminates. Furthermore, the correctness of the algorithm is given by its post-condition where all removed constraints are recoverable by reapplying (strong) closure.
4
Comparison 𝑂 ≡ 𝑃
𝑂 ≺𝑃
𝑂 ≻𝑃
𝑂 ≺≻ 𝑃
𝑂 ?𝑃
Full
1179
3082
499
2159
11
MN + Reduc
3768
2514
280
368
0
symbolic component derived by the analyzer, the Predicates domain already includes highly precise information. Each experiment uses subject programs consisting of 192 Java methods from previous research [6, 28], each exhibiting various levels of complexity. The total number of invariants is 6, 930 compared in eight different configurations. We used a supercomputer and an existing DFA framework [5, 27] to compute all analyses. 4.1
Comparable Domains
Table 1 shows the results of comparing Octagons (𝑂) against Zones (𝑍 ) and Intervals (𝐼 ). Since the domains are ordered, an invariant of 𝐼 or 𝑍 can only be as precise (≡ 𝑂) or less precise than Octagons (≺ 𝑂). The table includes the counts of each comparison classification for each comparison technique. The data shows that using full comparison, 86% of Octagon invariants are more precise than Interval invariants. However, using only minimization, the proportion reduces to 44%. In MN+Reduction this proportion drops to 36%. A similar trend occurs when comparing octagonal invariants to zonal invariants: 26% to 11% to 6%, respectively.
Experiments and Results
To evaluate the effectiveness of the spurious constraint reduction algorithm for Octagons, we compared the precision of invariants, via logical implication, computed by DFA using Octagons against those from other abstract domains. To establish the baseline data, we compare entire invariants, i.e., full state comparison or Full Comparison (FC). Next, we minimally compare invariants using Minimal Neighbors (MN) by selecting only the constraints of changed variables by leveraging Algorithm 1. Lastly we apply MN on invariants that underwent the spurious constraint reduction as described in Algorithm 2 (MN + Reduction). We divide experiments into comparisons of Octagons with Zones and Intervals, i.e, comparable numerical domains and an incomparable Symbolic Predicates domain. The Symbolic Predicates domain [28] used in this study includes the following initial disjoint predicate elements: {(−∞, −5], (−5, −2], −1, 0, 1, [2, 5), [5, +∞)}. This predicate domain was derived from values identified from a previous empirical study [10]. While specialized predicates for each program would likely improve precision for the symbolic Predicates domain, we chose a generic domain since our interest lies in the trends within the logical entailment results between domain instances. Moreover, since our comparison study includes the
4.2
Incomparable Domains
Table 2 shows the comparison results between Symbolic Predicate and Octagon invariants. Since these domains are incomparable, the table has three additional classifications: 𝑂 ≻ 𝑃, Octagons less precise than Symbolic Predicates, and 𝑂 ≺≻ 𝑃, where both invariants are incomparable. A third column, 𝑂 ? 𝑃, represents instances where our solver, Z3 [11], returned UNKNOWN. For this experiment, we used the iterative algorithm from previous work [4] for comparing incomparable domains and omit data for 𝑀𝑁 experiment. The data reveals that the number of equivalent invariants went up from 17% to 54%. The trends from other classifications are decreasing: from 44% to 36% for Symbolic Predicates more precise, from 7% to 4% for Octagons more precise, 4
Minimal Comparison of Octagonal Abstract Domains
PL’18, January 01–03, 2018, New York, NY, USA
from 31% to simply 5% for incomparable. Critically, minimal comparison resolved all 11 queries that previously returned UNKNOWN, a direct result of the reduced query size. 4.3
reducing the number of comparisons needed to determine subsumption or equality between Octagon states during the fixed point computation.
Discussion
References
The data from the tables suggests that the spurious reduction technique allows for more comprehensive comparison between abstract domains. That is, our reduced and minimal technique of comparison of invariants demonstrates a finer granularity of precision performance, especially for Symbolic Predicates. Evaluations show that the impact of Octagons on invariant precision might not be that significant. These findings substantiate arguments from previous work about weakly-relational domains computing predominately interval invariants [12, 13].
5
[1] Sven Apel, Dirk Beyer, Karlheinz Friedberger, Franco Raimondi, and Alexander von Rhein. 2013. Domain Types: Abstract-Domain Selection Based on Variable Usage. Lecture Notes in Computer Science (2013), 262–278. doi:10.1007/978-3-319-03077-7_18 [2] Kenny Ballou and Elena Sherman. 2022. Incremental Transitive Closure for Zonal Abstract Domain. In NASA Formal Methods, Jyotirmoy V. Deshmukh, Klaus Havelund, and Ivan Perez (Eds.). Springer International Publishing, Cham, 800–808. doi:10.1007/978-3-031-06773-0_43 [3] Kenny Ballou and Elena Sherman. 2023. Identifying Minimal Changes in the Zone Abstract Domain. In Theoretical Aspects of Software Engineering, Cristina David and Meng Sun (Eds.). Springer Nature Switzerland, Cham, 221–239. doi:10.1007/978-3-031-35257-7_13 [4] Kenny Ballou and Elena Sherman. 2023. Minimally Comparing Relational Abstract Domains. In Automated Technology for Verification and Analysis, Étienne André and Jun Sun (Eds.). Springer Nature Switzerland, Cham, 159–175. doi:10.1007/978-3-031-45332-8_8 [5] Kenny Ballou and Elena Sherman. 2025. StaticIcedTea. doi:10.5281/ ZENODO.16693791 [6] Kenny Ballou and Elena Sherman. 2026. Java Benchmark Artifacts. doi:10.5281/ZENODO.18166810 [7] Eric Bodden. 2018. Self-adaptive static analysis. Proceedings of the 40th International Conference on Software Engineering: New Ideas and Emerging Results (5 2018). doi:10.1145/3183399.3183401 [8] Ignacio Casso, José F. Morales, Pedro López-García, Roberto Giacobazzi, and Manuel V. Hermenegildo. 2020. Computing Abstract Distances in Logic Programs. Lecture Notes in Computer Science (2020), 57–72. doi:10.1007/978-3-030-45260-5_4 [9] Aziem Chawdhary, Ed Robbins, and Andy King. 2018. Incrementally Closing Octagons. Formal Methods in System Design 54, 2 (1 2018), 232–277. doi:10.1007/s10703-017-0314-7 [10] Christian Collberg, Ginger Myles, and Michael Stepp. 2007. An Empirical Study of Java Bytecode Programs. Software: Practice and Experience 37, 6 (2007), 581–641. doi:10.1002/spe.776 [11] Leonardo de Moura and Nikolaj Bjørner. 2008. Z3: An Efficient SMT Solver. In Tools and Algorithms for the Construction and Analysis of Systems, C. R. Ramakrishnan and Jakob Rehof (Eds.). Springer Berlin Heidelberg, Berlin, Heidelberg, 337–340. [12] Graeme Gange, Zequn Ma, Jorge A. Navas, Peter Schachte, Harald Søndergaard, and Peter J. Stuckey. 2021. A Fresh Look at Zones and Octagons. ACM Transactions on Programming Languages and Systems 43, 3 (9 2021), 1–51. doi:10.1145/3457885 [13] Graeme Gange, Jorge A. Navas, Peter Schachte, Harald Søndergaard, and Peter J. Stuckey. 2016. Exploiting Sparsity in Difference-Bound Matrices. Lecture Notes in Computer Science (2016), 189–211. doi:10. 1007/978-3-662-53413-7_10 [14] Roberto Giacobazzi and Isabella Mastroeni. 2002. Domain Compression for Complete Abstractions. Verification, Model Checking, and Abstract Interpretation (12 2002), 146–160. doi:10.1007/3-540-36384-X_14 [15] Roberto Giacobazzi, Isabella Mastroeni, and Elia Perantoni. 2023. How Fitting is Your Abstract Domain? Springer Nature Switzerland, 286–309. doi:10.1007/978-3-031-44245-2_14 [16] Arie Gurfinkel and Sagar Chaki. 2010. Boxes: A Symbolic Abstract Domain of Boxes. Lecture Notes in Computer Science (2010), 287–303. doi:10.1007/978-3-642-15769-1_18 [17] Jacob M. Howe and Andy King. 2009. Logahedra: A New Weakly Relational Domain. Lecture Notes in Computer Science (2009), 306–320. doi:10.1007/978-3-642-04761-9_23
Related Work
Research presenting new techniques or new abstract domains tend to use one of two methods for comparison: either logical entailment [24, 28], or property or invariant capture [12, 16, 17, 21, 22]. Our work fits into the former group of work. However, this work extends previous work [3, 4] work by providing algorithms for identifying minimal subsets of Octagons. In general, we notice an increasing amount of research in measuring and quantifying the differences between various abstract domains [3, 4, 8, 14, 15, 26]. While our work does not make any substantive arguments about distance between Intervals, Zones, and Octagons, we do present several techniques which we believe complement the current research.
6
Conclusion
In this work, we presented a reduction algorithm for Octagons that leverages the incremental nature of DFA. Combining with previous work on minimally comparing abstract domains, the reduction provides a more granular view of the precision benefits of Octagons compared to other numerical domains. Using real-world programs, we empirically evaluated the invariant precision of Octagons to Zones, Intervals, and Symbolic Predicates. The results show that a significant majority of invariants computed by Octagons are intervalvalued, experimentally confirming anecdotal comments of other previous work [12]. As noted previously, the reduction algorithm combined with work from Larsen et al. [19, 20] would complement each other well in a model-checking context. Furthermore, an interesting future direction of this work would be exploring the interaction of the techniques for identifying minimal changes within weakly-relational domains complements research attempting to create metrics around domain precision. Finally, it remains an open question whether the set of minimal changes can be used to improve the efficiency of DFA, by 5
PL’18, January 01–03, 2018, New York, NY, USA
Kenny Ballou and Elena Sherman [24] Antoine Miné. 2004. Weakly Relational Numerical Abstract Domains. https://pastel.archives-ouvertes.fr/tel-00136630 [25] Antoine Miné. 2006. The Octagon Abstract Domain. Higher-Order and Symbolic Computation 19, 1 (3 2006), 31–100. doi:10.1007/s10990-0068609-1 [26] Michael Schwarz, Simmo Saan, Helmut Seidl, Julian Erhard, and Vesal Vojdani. 2023. Clustered Relational Thread-Modular Abstract Interpretation with Local Traces. Springer Nature Switzerland, 28–58. doi:10.1007/978-3-031-30044-8_2 [27] Elena Sherman. 2018. Redesigning Soot’s Data-Flow Analysis Framework for Abstract Interpretation. In Companion Proceedings for the ISSTA/ECOOP 2018 Workshops (Amsterdam, Netherlands) (ISSTA ’18). Association for Computing Machinery, New York, NY, USA, 78–84. doi:10.1145/3236454.3236506 [28] Elena Sherman and Matthew B. Dwyer. 2015. Exploiting Domain and Program Structure to Synthesize Efficient and Precise Data Flow Analyses (T). 2015 30th IEEE/ACM International Conference on Automated Software Engineering (ASE) (11 2015). doi:10.1109/ase.2015.41 [29] Ole Tange. 2024. GNU Parallel 20240322 (’Sweden’). doi:10.5281/zenodo. 10901541 GNU Parallel is a general parallelizer to run multiple serial command line programs in parallel without changing them..
[18] Jacques-Henri Jourdan. 2017. Sparsity Preserving Algorithms for Octagons. Electronic Notes in Theoretical Computer Science 331 (3 2017), 57–70. doi:10.1016/j.entcs.2017.02.004 [19] K.G. Larsen, F. Larsson, P. Pettersson, and W. Yi. 1997. Efficient Verification of Real-Time Systems: Compact Data Structure and State-Space Reduction. In Proceedings Real-Time Systems Symposium. IEEE Comput. Soc, 14–24. doi:10.1109/real.1997.641265 [20] Kim G. Larsen, Fredrik Larsson, Paul Pettersson, and Wang Yi. 2003. Compact Data Structures and State-Space Reduction for Model Checking Real-Time Systems. Real-Time Systems 25, 2/3 (2003), 255–275. doi:10.1023/a:1025132427497 [21] Vincent Laviron and Francesco Logozzo. 2008. SubPolyhedra: A (More) Scalable Approach to Infer Linear Inequalities. Verification, Model Checking, and Abstract Interpretation (2008), 229–244. doi:10.1007/9783-540-93900-9_20 [22] Francesco Logozzo and Manuel Fähndrich. 2010. Pentagons: A Weakly Relational Abstract Domain for the Efficient Validation of Array Accesses. Science of Computer Programming 75, 9 (9 2010), 796–807. doi:10.1016/j.scico.2009.04.004 [23] Antoine Miné. 2001. A New Numerical Abstract Domain Based on Difference-Bound Matrices. Lecture Notes in Computer Science (2001), 155–172. doi:10.1007/3-540-44978-7_10
6