Some trade-offs in reducing the overhead of assertion run-time checks via static analysis

Stulova, Nataliia and Morales Caballero, José Francisco and Hermenegildo, Manuel V. (2018). Some trade-offs in reducing the overhead of assertion run-time checks via static analysis. "Science of Computer Programming", v. 155 ; pp. 3-26. ISSN 0167-6423. https://doi.org/10.1016/j.scico.2017.12.006.

Description

Title: Some trade-offs in reducing the overhead of assertion run-time checks via static analysis
Author/s:
  • Stulova, Nataliia
  • Morales Caballero, José Francisco
  • Hermenegildo, Manuel V.
Item Type: Article
Título de Revista/Publicación: Science of Computer Programming
Date: 2018
ISSN: 0167-6423
Volume: 155
Subjects:
Freetext Keywords: Abstract interpretation; Run-time checking; Verification; Logic programming; Horn clauses
Faculty: E.T.S. de Ingenieros Informáticos (UPM)
Department: Inteligencia Artificial
Creative Commons Licenses: Recognition - No derivative works - Non commercial

Full text

[img]
Preview
PDF - Requires a PDF viewer, such as GSview, Xpdf or Adobe Acrobat Reader
Download (2MB) | Preview

Abstract

A number of approaches for helping programmers detect incorrect program behaviors are based on combining language-level constructs (such as procedure-level assertions/contracts, program-point assertions, or gradual types) with a number of associated tools (such as code analyzers and run-time verification frameworks) that automatically check the validity of such constructs. However, these constructs and tools are often not used to their full extent in practice due to excessive run-time overhead, limited expressiveness, and/or limitations in the effectiveness of the tools. Verification frameworks that combine static and dynamic verification techniques and are based on abstraction 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 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 obtained via abstract interpretation, we propose and study a number of practical assertion checking “modes,” each of which represents a trade-off between code annotation depth, execution time slowdown, and program safety. We then explore these modes in two typical, library-oriented scenarios. We also propose program transformation-based methods 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 benefits obtained from analysis and the proposed transformations in these scenarios

More information

Item ID: 52831
DC Identifier: http://oa.upm.es/52831/
OAI Identifier: oai:oa.upm.es:52831
DOI: 10.1016/j.scico.2017.12.006
Official URL: https://www.sciencedirect.com/science/article/pii/S0167642317302915
Deposited by: Biblioteca Facultad de Informatica
Deposited on: 29 Oct 2018 12:43
Last Modified: 29 Oct 2018 12:43
  • Logo InvestigaM (UPM)
  • Logo GEOUP4
  • Logo Open Access
  • Open Access
  • Logo Sherpa/Romeo
    Check whether the anglo-saxon journal in which you have published an article allows you to also publish it under open access.
  • Logo Dulcinea
    Check whether the spanish journal in which you have published an article allows you to also publish it under open access.
  • Logo de Recolecta
  • Logo del Observatorio I+D+i UPM
  • Logo de OpenCourseWare UPM