The Systematic Design of Responsibility Analysis by Abstract Interpretation

Chaoqiang Deng, Patrick Cousot

Research output: Contribution to journalArticlepeer-review

Abstract

Given a behavior of interest, automatically determining the corresponding responsible entity (i.e., the root cause) is a task of critical importance in program static analysis. In this article, a novel definition of responsibility based on the abstraction of trace semantics is proposed, which takes into account the cognizance of observer, which, to the best of our knowledge, is a new innovative idea in program analysis. Compared to current dependency and causality analysis methods, the responsibility analysis is demonstrated to be more precise on various examples.However, the concrete trace semantics used in defining responsibility is uncomputable in general, which makes the corresponding concrete responsibility analysis undecidable. To solve this problem, the article proposes a sound framework of abstract responsibility analysis, which allows a balance between cost and precision. Essentially, the abstract analysis builds a trace partitioning automaton by an iteration of over-approximating forward reachability analysis with trace partitioning and under/over-approximating backward impossible failure accessibility analysis, and determines the bounds of potentially responsible entities along paths in the automaton. Unlike the concrete responsibility analysis that identifies exactly a single action as the responsible entity along every concrete trace, the abstract analysis may lose some precision and find multiple actions potentially responsible along each automaton path. However, the soundness is preserved, and every responsible entity in the concrete is guaranteed to be also found responsible in the abstract.

Original languageEnglish (US)
Article number3484938
JournalACM Transactions on Programming Languages and Systems
Volume44
Issue number1
DOIs
StatePublished - Mar 2022

Keywords

  • Responsibility analysis
  • abstract interpretation
  • backward accessibility analysis
  • causality
  • cognizance
  • dependency
  • forward reachability analysis
  • trace partitioning

ASJC Scopus subject areas

  • Software

Fingerprint

Dive into the research topics of 'The Systematic Design of Responsibility Analysis by Abstract Interpretation'. Together they form a unique fingerprint.

Cite this