Multivariant Assertion-based Guidance in Abstract Interpretation
| Autor: | José F. Morales, Manuel V. Hermenegildo, Isabel Garcia-Contreras |
|---|---|
| Rok vydání: | 2018 |
| Předmět: |
Soundness
Informática FOS: Computer and information sciences Computer Science - Logic in Computer Science Computer Science - Programming Languages Computer science Programming language Semantics (computer science) Assertion 020207 software engineering 02 engineering and technology Static analysis 16. Peace & justice Abstract interpretation computer.software_genre Logic in Computer Science (cs.LO) Set (abstract data type) Program analysis 0202 electrical engineering electronic engineering information engineering 020201 artificial intelligence & image processing computer Compile time Programming Languages (cs.PL) |
| Zdroj: | LOPSTR 2018: 28th International Symposium on Logic-Based Program Synthesis and Transformation | 28th International Symposium on Logic-Based Program Synthesis and Transformation (LOPSTR 2018) | 4-6 Sep 2018 | Frankfurt, Alemania Archivo Digital UPM Universidad Politécnica de Madrid Logic-Based Program Synthesis and Transformation ISBN: 9783030138370 LOPSTR |
| DOI: | 10.48550/arxiv.1808.05197 |
| Popis: | Approximations during program analysis are a necessary evil, as they ensure essential properties, such as soundness and termination of the analysis, but they also imply not always producing useful results. Automatic techniques have been studied to prevent precision loss, typically at the expense of larger resource consumption. In both cases (i.e., when analysis produces inaccurate results and when resource consumption is too high), it is necessary to have some means for users to provide information to guide analysis and thus improve precision and/or performance. We present techniques for supporting within an abstract interpretation framework a rich set of assertions that can deal with multivariance/context-sensitivity, and can handle different run-time semantics for those assertions that cannot be discharged at compile time. We show how the proposed approach can be applied to both improving precision and accelerating analysis. We also provide some formal results on the effects of such assertions on the analysis results. Comment: Pre-proceedings paper presented at the 28th International Symposium on Logic-Based Program Synthesis and Transformation (LOPSTR 2018), Frankfurt am Main, Germany, 4-6 September 2018 (arXiv:1808.03326) |
| Databáze: | OpenAIRE |
| Externí odkaz: |
|