Sat 17 Jun 2023 09:00 - 09:30 at Magnolia 18 - SOAP: Session 1 - Static Analysis Chair(s): Vincenzo Arceri

E-graphs are a data structure that compactly represents equivalent expressions. They are constructed via the repeated application of rewrite rules. Often in practical applications, conditional rewrite rules are crucial, but their application requires the detection – at the time the e-graph is being built – that a condition is valid in the domain of application. Detecting condition validity amounts to proving a property of the program. Abstract interpretation is a general method to learn such properties, traditionally used in static analysis tools. We demonstrate that abstract interpretation and e-graph analysis naturally reinforce each other through a tight integration because (i) the e-graph clustering of equivalent expressions induces natural precision refinement of abstractions and (ii) precise abstractions allow the application of deeper rewrite rules (and hence potentially even greater precision). We develop the theory behind this intuition and present an exemplar interval arithmetic implementation, which we apply to the FPBench suite.

Sat 17 Jun

Displayed time zone: Eastern Time (US & Canada) change

09:00 - 11:00
SOAP: Session 1 - Static AnalysisSOAP at Magnolia 18
Chair(s): Vincenzo Arceri University of Parma, Italy

#soap-sat-magnolia18 Discord icon small YouTube icon small

09:00
30m
Talk
Combining E-Graphs with Abstract Interpretation
SOAP
Samuel Coward Imperial College London, UK / Intel Corporation, George A. Constantinides Imperial College London, UK, Theo Drane Intel Corporation, USA
DOI
09:30
30m
Talk
Static Analysis of Data Transformations in Jupyter Notebooks (Virtual)
SOAP
Luca Negrini Ca’ Foscari University of Venice, Corvallis S.r.l., Guruprerana Shabadi École Polytechnique, Institut Polytechnique de Paris, Caterina Urban INRIA & École Normale Supérieure | Université PSL
DOI
10:00
30m
Talk
Speeding up Static Analysis with the Split Operator
SOAP
Vincenzo Arceri University of Parma, Italy, Greta Dolcetti University of Parma - Department of Mathematical, Physical, and Computer Sciences, Enea Zaffanella University of Parma, Italy
DOI
10:30
30m
Talk
When Long Jumps Fall Short: Control-Flow Tracking and Misuse Detection for Non-local Jumps in C
SOAP
Michael Schwarz Technische Universität München, Julian Erhard Technical University of Munich, Vesal Vojdani University of Tartu, Simmo Saan University of Tartu, Estonia, Helmut Seidl Technische Universität München
DOI Media Attached