Finding Fix Locations for CFL-Reachability Analyses via Minimum Cuts
| Autor: | Martin Vechev, Manu Sridharan, Satish Chandra, Andrei Marian Dan, Jean-Baptiste Jeannin |
|---|---|
| Rok vydání: | 2017 |
| Předmět: |
Optimization problem
Computer science 020207 software engineering Static program analysis 02 engineering and technology Static analysis Small set Set (abstract data type) Reachability 020204 information systems Maximum satisfiability problem 0202 electrical engineering electronic engineering information engineering Graph (abstract data type) Algorithm |
| Zdroj: | Computer Aided Verification ISBN: 9783319633893 CAV (2) |
| DOI: | 10.1007/978-3-319-63390-9_27 |
| Popis: | Static analysis tools are increasingly important for ensuring code quality. Ideally, all warnings from a static analysis would be addressed, but the volume of warnings and false positives usually makes this effort prohibitive. We present techniques for finding fix locations, a small set of program locations where fixes can be applied to address all static analysis warnings. We focus on analyses expressible as context-free-language reachability, where a set of fix locations is naturally expressed as a min-cut of the CFL graph. We show, surprisingly, that computing such a CFL min-cut is NP-hard. We then phrase the problem of finding CFL min-cuts as an optimization problem which allows us to trade-off the size of the cut vs. the preservation of computed information. We then show how to solve the optimization problem via a MaxSAT encoding. |
| Databáze: | OpenAIRE |
| Externí odkaz: |
|