Practical run-time checking via unobtrusive property caching

DOI10.1017/S1471068415000344MaRDI QIDQ4593012zbMATH OpenOpenAlexFDO

Authors Nataliia Stulova, Manuel Hermenegildo, J. F. Morales

Publication date 9 November 2017

Published in Theory and Practice of Logic Programming (Search for Journal in Brave)

Full work available at URL https://arxiv.org/abs/1507.05986

Mathematics Subject Classification ID

Theory of software (68N99)

Abstract: The use of annotations, referred to as assertions or contracts, to describe program properties for which run-time tests are to be generated, has become frequent in dynamic programing languages. However, the frameworks proposed to support such run-time testing generally incur high time and/or space overheads over standard program execution. We present an approach for reducing this overhead that is based on the use of memoization to cache intermediate results of check evaluation, avoiding repeated checking of previously verified properties. Compared to approaches that reduce checking frequency, our proposal has the advantage of being exhaustive (i.e., all tests are checked at all points) while still being much more efficient than standard run-time checking. Compared to the limited previous work on memoization, it performs the task without requiring modifications to data structure representation or checking code. While the approach is general and system-independent, we present it for concreteness in the context of the Ciao run-time checking framework, which allows us to provide an operational semantics with checks and caching. We also report on a prototype implementation and provide some experimental results that support that using a relatively small cache leads to significant decreases in run-time checking overhead.

Recommendations

• scientific article; zbMATH DE number 3978353
• Verified runtime assertion checking for memory properties
• Runtime Checking for Separation Logic
• Run-time checking multi-threaded Java programs
• Provably correct runtime monitoring

Cites work

• An overview of Ciao and its design philosophy
• Compile-time derivation of variable dependency using abstract interpretation
• Contracts for higher-order functions
• Efficient tabling of structured data with enhanced hash-consing
• scientific article; zbMATH DE number 1615263 (Why is no real title available?)
• scientific article; zbMATH DE number 1368925 (Why is no real title available?)
• Special issue: Selected papers based on the presentation at the 10th inernational static analysis symposium (SAS 2003), San Diego, CA, USA, June 11--13, 2003.
• Specification and verification challenges for sequential object-oriented programs
• Static contract checking with abstract interpretation
• The design and implementation of Typed Scheme
• XSB: extending Prolog with tabled logic programming

Cited in

(2)

• Testing your (static analysis) truths
• Parallel Logic Programming: A Sequel

Describes a project that uses

Uses Software

• CiaoPP
• XSB
• Ciao

This page was built for publication: Practical run-time checking via unobtrusive property caching

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q4593012)