University of Sussex
Browse
paper.pdf (47.28 kB)

Challenges in decomposing encodings of verification problems

Download (47.28 kB)
Version 2 2023-06-12, 06:39
Version 1 2023-06-09, 01:09
journal contribution
posted on 2023-06-12, 06:39 authored by Peter Schrammel
Modern program verifiers use logic-based encodings of the verification problem that are discharged by a back end reasoning engine. However, instances of such encodings for large programs can quickly overwhelm these back end solvers. Hence, we need techniques to make the solving process scale to large systems, such as partitioning (divide-and-conquer) and abstraction. In recent work, we showed how decomposing the formula encoding of a termination analysis can significantly increase efficiency. The analysis generates a sequence of logical formulas with existentially quantified predicates that are solved by a synthesis-based program analysis engine. However, decomposition introduces abstractions in addition to those required for finding the unknown predicates in the formula, and can hence deteriorate precision. We discuss the challenges associated with such decompositions and their interdependencies with the solving process.

History

Publication status

  • Published

File Version

  • Published version

Journal

Electronic Proceedings in Theoretical Computer Science

ISSN

2075-2180

Publisher

Electronic Proceedings in Theoretical Computer Science (EPTCS)

Volume

219

Page range

29-32

Book title

Proceedings 3rd Workshop on Horn Clauses for Verification and Synthesis (HCVS2016)

ISBN

2075-2180

Series

Electronic Proceedings in Theoretical Computer Science

Department affiliated with

  • Informatics Publications

Notes

Proceedings of the 3rd Workshop on Horn Clauses for Verification and Synthesis (HCVSS2016), Eindhoven, The Netherlands, 3rd April 2016.

Full text available

  • Yes

Peer reviewed?

  • Yes

Editors

Philipp Rümmer, John P Gallagher

Legacy Posted Date

2016-08-04

First Open Access (FOA) Date

2016-08-04

First Compliant Deposit (FCD) Date

2016-08-04

Usage metrics

    University of Sussex (Publications)

    Categories

    No categories selected

    Licence

    Exports

    RefWorks
    BibTeX
    Ref. manager
    Endnote
    DataCite
    NLM
    DC