University of Sussex
Browse
paper.pdf (272.15 kB)

Compositional safety refutation techniques

Download (272.15 kB)
conference contribution
posted on 2023-06-09, 07:30 authored by Madhukar Kumar, Peter Schrammel, Srivas Mandayam
One of the most successful techniques for refuting safety properties is to find counterexamples by bounded model checking. However, for large programs, bounded model checking instances often exceed the limits of resources available. Generating such counterexamples in a modular way could speed up refutation, but it is challenging because of the inherently non-compositional nature of these counterexamples. We start from the monolithic safety verification problem and present a step-by-step derivation of the compositional safety refutation problem. We give three algorithms that solve this problem, discuss their properties with respect to efficiency and completeness, and evaluate them experimentally.

History

Publication status

  • Published

File Version

  • Accepted version

Journal

Automated Technology for Verification and Analysis

Publisher

Springer

Page range

164-183

Event name

15th International Symposium on Automated Technology for Verification and Analysis

Event location

Pune, India

Event type

conference

Event date

3-6 October 2017

ISBN

9783319681665

Series

Lecture notes in computer science

Department affiliated with

  • Informatics Publications

Full text available

  • Yes

Peer reviewed?

  • Yes

Legacy Posted Date

2017-08-02

First Open Access (FOA) Date

2017-10-13

First Compliant Deposit (FCD) Date

2017-08-01

Usage metrics

    University of Sussex (Publications)

    Categories

    No categories selected

    Exports

    RefWorks
    BibTeX
    Ref. manager
    Endnote
    DataCite
    NLM
    DC