University of Sussex
Browse

File(s) under permanent embargo

Necessary and sufficient preconditions via eager abstraction

chapter
posted on 2023-06-09, 00:30 authored by Mohamed Nassim Seghir, Peter Schrammel
The precondition for safe execution of a procedure is useful for understanding, verifying and debugging programs. We have previously presented a cegar-based approach for inferring necessary and sufficient preconditions based on the iterative abstraction-refinement of the set of safe and unsafe states until they become disjoint. A drawback of that approach is that safe and unsafe traces are explored separately and each time they are built entirely before being checked for consistency. In this paper, we present an eager approach that explores shared prefixes between safe and unsafe traces conjointly. As a result, individual state sets, by construction, fulfil the property of separation between safe and unsafe states without requiring any refinement. Experiments using our implementation of this technique in the precondition generator P-Gen show a significant improvement compared to our previous cegar-based method. In some cases the running time drops from several minutes to several seconds.

History

Publication status

  • Published

File Version

  • Published version

Publisher

Springer

Issue

8858

Page range

236-254

Event name

Programming Languages and Systems, APLAS 2014

Book title

Programming languages and systems : 12th Asian Symposium, APLAS 2014, Singapore, Singapore, November 17-19, 2014, Proceedings

ISBN

9783319127354

Series

Lecture notes in computer science

Department affiliated with

  • Informatics Publications

Full text available

  • No

Peer reviewed?

  • Yes

Editors

Jacques Garrigue

Legacy Posted Date

2016-05-09

First Compliant Deposit (FCD) Date

2016-05-09

Usage metrics

    University of Sussex (Publications)

    Categories

    No categories selected

    Exports

    RefWorks
    BibTeX
    Ref. manager
    Endnote
    DataCite
    NLM
    DC