Enhancing Compositional Static Analysis with Dynamic Analysis

In this paper we introduce a novel method for improving static analysis of real code by using dynamic analysis. We have implemented our technique to enhance the Infer static analyzer [6] for Erlang by supplementing its analysis with data obtained by FAUSTA [24] dynamic analysis. We present the techn...

Full description

Saved in:
Bibliographic Details
Main Authors: Distefano, Dino, Marescotti, Matteo, Ahs, Cons, Cela, Sopot, Sampaio, Gabriela Cunha, Grigore, Radu, Hajdu, Akos, Kapus, Timotej, Mao, Ke, Suzanne, Thibault
Format: Conference Proceeding
Language:English
Subjects:
Codes
Defect detection
Freeware
General and reference
General and reference > Cross-computing tools and techniques
General and reference > Cross-computing tools and techniques > Verification
Heuristic algorithms
Internet telephony
Privacy
Servers
Software algorithms
Software and its engineering
Software and its engineering > Software creation and management
Software and its engineering > Software creation and management > Software verification and validation
Software and its engineering > Software creation and management > Software verification and validation > Software defect analysis
Software and its engineering > Software creation and management > Software verification and validation > Software defect analysis > Software testing and debugging
Software and its engineering > Software organization and properties
Software and its engineering > Software organization and properties > Software functional properties
Software and its engineering > Software organization and properties > Software functional properties > Formal methods
Software engineering
Static analysis
Theory of computation
Theory of computation > Semantics and reasoning
Theory of computation > Semantics and reasoning > Program reasoning
Online Access:Request full text
Tags: Add Tag
No Tags, Be the first to tag this record!
Description
Summary:In this paper we introduce a novel method for improving static analysis of real code by using dynamic analysis. We have implemented our technique to enhance the Infer static analyzer [6] for Erlang by supplementing its analysis with data obtained by FAUSTA [24] dynamic analysis. We present the technical details of the algorithm combining static and dynamic analysis and a case study on its evaluation on WhatsApp's Erlang code to detect software defects. Results show an increase in detected bugs in 76% of the runs when data from dynamic analysis is used. In particular, on average, data provided by dynamic analysis for 1 function enables static analysis of 2.1 additional functions. Moreover, dynamic data enabled analysis of a property not verifiable using static analysis alone.
ISSN:2643-1572
DOI:10.1145/3691620.3695599