> Details

Estep, Sam [Author]; Wise, Jenna [Author]; Aldrich, Jonathan [Author]; Tanter, Éric [Author]; Bader, Johannes [Author]; Sunshine, Joshua [Author] ; Sam Estep and Jenna Wise and Jonathan Aldrich and Éric Tanter and Johannes Bader and Joshua Sunshine [Contributor]

Gradual Program Analysis for Null Pointers

Reference
management

Bookmarks

Remove from
bookmarks

Share this on Whatsapp

Close

Bookmarks



You can manage bookmarks using lists, please log in to your user account for this.
  • Media type: Text; E-Article; Electronic Conference Proceeding
  • Title: Gradual Program Analysis for Null Pointers
  • Contributor: Estep, Sam [Author]; Wise, Jenna [Author]; Aldrich, Jonathan [Author]; Tanter, Éric [Author]; Bader, Johannes [Author]; Sunshine, Joshua [Author]
  • Published: Schloss Dagstuhl – Leibniz-Zentrum für Informatik, 2021
  • Language: English
  • DOI: https://doi.org/10.4230/LIPIcs.ECOOP.2021.3
  • Keywords: dataflow analysis ; gradual verification ; gradual typing
  • Origination:
  • Footnote: Diese Datenquelle enthält auch Bestandsnachweise, die nicht zu einem Volltext führen.
  • Description: Static analysis tools typically address the problem of excessive false positives by requiring programmers to explicitly annotate their code. However, when faced with incomplete annotations, many analysis tools are either too conservative, yielding false positives, or too optimistic, resulting in unsound analysis results. In order to flexibly and soundly deal with partially-annotated programs, we propose to build upon and adapt the gradual typing approach to abstract-interpretation-based program analyses. Specifically, we focus on null-pointer analysis and demonstrate that a gradual null-pointer analysis hits a sweet spot, by gracefully applying static analysis where possible and relying on dynamic checks where necessary for soundness. In addition to formalizing a gradual null-pointer analysis for a core imperative language, we build a prototype using the Infer static analysis framework, and present preliminary evidence that the gradual null-pointer analysis reduces false positives compared to two existing null-pointer checkers for Infer. Further, we discuss ways in which the gradualization approach used to derive the gradual analysis from its static counterpart can be extended to support more domains. This work thus provides a basis for future analysis tools that can smoothly navigate the tradeoff between human effort and run-time overhead to reduce the number of reported false positives.
  • Access State: Open Access