On the Construction of Soundness Oracles
One of the inherent advantages of static analysis is that it can create and reason about models of an entire program. However, mainstream languages such as Java use numerous dynamic language features designed to boost programmer productivity, but these features are notoriously difficult to capture by static analysis, leading to unsoundness in practice.
While existing research has focused on providing sound handling for selected language features (mostly reflection) based on anecdotal evidence and case studies, there is little empirical work to investigate the extent to which particular features cause unsoundness of static analysis in practice. In this paper, we (1) discuss language features that may cause unsoundness and (2) discuss a methodology that can be used to check the (un)soundness of a particular static analysis, call-graph construction, based on soundness oracles. These oracles can also be used for hybrid analyses.
Sun 18 JunDisplayed time zone: Amsterdam, Berlin, Bern, Rome, Stockholm, Vienna change
14:45 - 15:30 | |||
14:45 22mTalk | Systematic Approaches for Increasing Soundness and Precision of Static Analyzers SOAP Esben Andreasen Aarhus University, Anders Møller Aarhus University, Benjamin Barslev Nielsen Aarhus University DOI File Attached | ||
15:07 22mTalk | On the Construction of Soundness Oracles SOAP Jens Dietrich Massey University, Li Sui Massey University, New Zealand, Shawn Rasheed Massey University, Amjed Tahir Massey University DOI Media Attached |