Unconstrained Variable Oracles for Faster Static Analyses
In the context of static analysis based on Abstract Interpretation, we propose a lightweight pre-analysis step which is meant to suggest, at each program point, which program variables are likely to be unconstrained for a specific class of abstract properties. Using the outcome of this pre-analysis as an oracle, we simplify the statements of the program being analyzed by propagating this lack of information, aiming at fine-tuning the precision/efficiency trade-off of the analysis. A preliminary experimental evaluation shows that the idea underlying the approach is promising, as it improves the efficiency of the more costly analysis, while having a limited effect on its precision.
Tue 24 OctDisplayed time zone: Lisbon change
09:00 - 10:30
|ADCL: Acceleration Driven Clause Learning for Constrained Horn Clauses|
|Unconstrained Variable Oracles for Faster Static Analyses|
Vincenzo Arceri University of Parma, Italy, Greta Dolcetti University of Parma - Department of Mathematical, Physical, and Computer Sciences, Enea Zaffanella University of Parma, ItalyPre-print
|Modular Optimization-Based Roundoff Error Analysis of Floating-Point Programs|