Reducing the overhead of assertion run-time checks via static analysis

Stulova, Nataliia and Morales Caballero, José Francisco and Hermenegildo, Manuel V. (2016). Reducing the overhead of assertion run-time checks via static analysis. In: "18th International Symposium on Principles and Practice of Declarative Programming (PPDP'16)", 05-07 Sep 2016, Edimburgo, Reino Unido. ISBN 978-1-4503-4148-6. pp. 90-103. https://doi.org/10.1145/2967973.2968597.

Description

Title: Reducing the overhead of assertion run-time checks via static analysis
Author/s:
  • Stulova, Nataliia
  • Morales Caballero, José Francisco
  • Hermenegildo, Manuel V.
Item Type: Presentation at Congress or Conference (Unspecified)
Event Title: 18th International Symposium on Principles and Practice of Declarative Programming (PPDP'16)
Event Dates: 05-07 Sep 2016
Event Location: Edimburgo, Reino Unido
Title of Book: PPDP '16: proceedings of the 18th International Symposium on Principles and Practice of Declarative Programming
Date: 2016
ISBN: 978-1-4503-4148-6
Volume: 1
Subjects:
Freetext Keywords: Abstract Interpretation; Assertions; 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

In order to aid in the process of detecting incorrect pro- gram 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). How- ever, 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 com- bine 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 speci- fications 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 rep- resents 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 se- mantics 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 scenario.

More information

Item ID: 52861
DC Identifier: http://oa.upm.es/52861/
OAI Identifier: oai:oa.upm.es:52861
DOI: 10.1145/2967973.2968597
Official URL: https://dl.acm.org/citation.cfm?id=2968597
Deposited by: Biblioteca Facultad de Informatica
Deposited on: 29 Oct 2018 16:47
Last Modified: 29 Oct 2018 16:47
  • 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