Memorias de investigación
Communications at congresses:
Reducing the Overhead of Assertion Run-time Checks via Static Analysis
Year:2016

Research Areas
  • Information technology and adata processing

Information
Abstract
In order to aid in the process of detecting incorrect program behaviors, a number of approaches have been proposed which include a combination of language-level constructs (such as procedure-level assertions/contracts, program-point assertions, gradual types, etc.) and associated tools (such as code analyzers and run-time verification frameworks). However, it is often the case that these constructs and tools are not used to their full extent in practice due to a number of limitations such as excessive run-time overhead and/or limited expressiveness. Verification frameworks that combine static and dynamic techniques offer the potential to bridge this gap. In this paper we explore the effectiveness of abstract interpretation in detecting parts of program specifications that can be statically simplified to true or false, as well as the impact of such analysis in reducing the cost of the run-time checks required for the remaining parts of these specifications. Starting with a semantics for programs with assertion checking, and for assertion simplification based on static analysis information, we propose and study a number of practical assertion checking modes, each of which represents a trade-off between code annotation depth, execu- tion time slowdown, and program safety. We also propose techniques for taking advantage of the run-time checking semantics to improve the precision of the analysis. Finally, we study experimentally the performance of these techniques. Our experiments illustrate the benefits and costs of each of the assertion checking modes proposed as well as the benefit of analysis for these scenarios.
International
Si
Congress
18th International Symposium on Principles and Practice of Declarative Programming
960
Place
School of Informatics, University of Edinburgh, UK
Reviewers
Si
ISBN/ISSN
978-1-4503-4148-6
10.1145/2967973.2968597
Start Date
05/09/2016
End Date
07/09/2016
From page
90
To page
103
Reducing the Overhead of Assertion Run-time Checks via Static Analysis
Participants

Research Group, Departaments and Institutes related
  • Creador: Grupo de Investigación: Computación lógica, Lenguajes, Implementación y Paralelismo (CLIP)
  • Departamento: Inteligencia Artificial