ECOOP 2022
Mon 6 June - Thu 7 July 2022 Berlin, Germany
Wed 8 Jun 2022 11:30 - 11:50 at Aurora Borealis 1 - Program Analysis 1 Chair(s): Karim Ali

Imprecision in static program analysis is a direct consequence of sound approximation of undecidable program properties. This corresponds to the release of false alarms and, as all alarming systems, a program analysis tool is credible when few of them are reported. As a consequence, we have to live together with false alarms, but also we need methods to control them. As for all approximation methods, also for abstract interpretation we need to estimate the accumulated imprecision during program analysis. In this talk, we introduce a theory for estimating the error propagation in abstract interpretation, and hence in program analysis. We enrich abstract domains with a weakening of a metric distance. This enriched structure keeps coherence between the standard partial order relating approximated objects by their relative precision and the effective error made in this approximation. An abstract interpretation is precise when it is complete. We introduce the notion of partial completeness as a weakening of precision. In partial completeness the abstract interpreter may produce a bounded number of false alarms. We prove the key recursive properties of the class of programs for which an abstract interpreter is partially complete by answering two foundational questions: Can we implement a partially complete program analysis w.r.t. a given bound of imprecision? Can we prove if a program analysis has bounded imprecision? Finally, we show a proof system for estimating an upper bound of the error accumulated by the abstract interpreter during program analysis.

Wed 8 Jun

Displayed time zone: Amsterdam, Berlin, Bern, Rome, Stockholm, Vienna change

11:00 - 12:30
Program Analysis 1Expert Discussion / Hub Talks / Research Papers at Aurora Borealis 1
Chair(s): Karim Ali University of Alberta
Software verification/program analysisExpert Discussion
Expert Discussion
P: Omer Tripp Amazon, P: Sebastian Erdweg JGU Mainz
Partial (In)Completeness in Abstract Interpretation: Limiting the Imprecision in Program AnalysisHub Talk
Hub Talks
Marco Campion University of Verona, Mila Dalla Preda University of Verona, Roberto Giacobazzi University of Verona
Link to publication DOI
Concolic Execution for WebAssemblyArtifacts Evaluated - ReusableArtifacts Evaluated - FunctionalECOOP 2022
Research Papers
Filipe Marques INESC-ID / Instituto Superior Tecnico, University of Lisbon, José Fragoso Santos INESC-ID/Instituto Superior Técnico, Portugal , Nuno Santos INESC-ID / Instituto Superior Tecnico, University of Lisbon, Pedro Adão IST-ULisboa and Instituto de Telecomunicações
Static Analysis for AWS Best Practices in Python CodeVCOOP 2022ECOOP 2022
Research Papers
Rajdeep Mukherjee Amazon Web Services, Omer Tripp Amazon, Ben Liblit Amazon, Michael Wilson Amazon Web Services