Satisfiability modulo heap-based programs

In this work, we present a semi-decision procedure for a fragment of separation logic with user-defined predicates and Presburger arithmetic. To check the satisfiability of a formula, our procedure iteratively unfolds the formula and examines the derived disjuncts. In each iteration, it searches for...

Full description

Saved in:
Bibliographic Details
Main Authors: LE, Quang Loc, SUN, Jun, CHIN, Wei-Ngan
Format: text
Language:English
Published: Institutional Knowledge at Singapore Management University 2016
Subjects:
Online Access:https://ink.library.smu.edu.sg/sis_research/4937
https://ink.library.smu.edu.sg/context/sis_research/article/5940/viewcontent/Satisfiability.pdf
Tags: Add Tag
No Tags, Be the first to tag this record!
Institution: Singapore Management University
Language: English
id sg-smu-ink.sis_research-5940
record_format dspace
spelling sg-smu-ink.sis_research-59402020-02-27T03:27:38Z Satisfiability modulo heap-based programs LE, Quang Loc SUN, Jun CHIN, Wei-Ngan In this work, we present a semi-decision procedure for a fragment of separation logic with user-defined predicates and Presburger arithmetic. To check the satisfiability of a formula, our procedure iteratively unfolds the formula and examines the derived disjuncts. In each iteration, it searches for a proof of either satisfiability or unsatisfiability. Our procedure is further enhanced with automatically inferred invariants as well as detection of cyclic proof. We also identify a syntactically restricted fragment of the logic for which our procedure is terminating and thus complete. This decidable fragment is relatively expressive as it can capture a range of sophisticated data structures with non-trivial pure properties, such as size, sortedness and near-balanced. We have implemented the proposed solver and a new system for verifying heap-based programs. We have evaluated our system on benchmark programs from a software verification competition. 2016-07-01T07:00:00Z text application/pdf https://ink.library.smu.edu.sg/sis_research/4937 info:doi/10.1007/978-3-319-41528-4_21 https://ink.library.smu.edu.sg/context/sis_research/article/5940/viewcontent/Satisfiability.pdf http://creativecommons.org/licenses/by-nc-nd/4.0/ Research Collection School Of Computing and Information Systems eng Institutional Knowledge at Singapore Management University Decision procedures Satisfiability Separation logic Inductive predicates Cyclic proofs Programming Languages and Compilers Software Engineering
institution Singapore Management University
building SMU Libraries
continent Asia
country Singapore
Singapore
content_provider SMU Libraries
collection InK@SMU
language English
topic Decision procedures
Satisfiability
Separation logic
Inductive predicates
Cyclic proofs
Programming Languages and Compilers
Software Engineering
spellingShingle Decision procedures
Satisfiability
Separation logic
Inductive predicates
Cyclic proofs
Programming Languages and Compilers
Software Engineering
LE, Quang Loc
SUN, Jun
CHIN, Wei-Ngan
Satisfiability modulo heap-based programs
description In this work, we present a semi-decision procedure for a fragment of separation logic with user-defined predicates and Presburger arithmetic. To check the satisfiability of a formula, our procedure iteratively unfolds the formula and examines the derived disjuncts. In each iteration, it searches for a proof of either satisfiability or unsatisfiability. Our procedure is further enhanced with automatically inferred invariants as well as detection of cyclic proof. We also identify a syntactically restricted fragment of the logic for which our procedure is terminating and thus complete. This decidable fragment is relatively expressive as it can capture a range of sophisticated data structures with non-trivial pure properties, such as size, sortedness and near-balanced. We have implemented the proposed solver and a new system for verifying heap-based programs. We have evaluated our system on benchmark programs from a software verification competition.
format text
author LE, Quang Loc
SUN, Jun
CHIN, Wei-Ngan
author_facet LE, Quang Loc
SUN, Jun
CHIN, Wei-Ngan
author_sort LE, Quang Loc
title Satisfiability modulo heap-based programs
title_short Satisfiability modulo heap-based programs
title_full Satisfiability modulo heap-based programs
title_fullStr Satisfiability modulo heap-based programs
title_full_unstemmed Satisfiability modulo heap-based programs
title_sort satisfiability modulo heap-based programs
publisher Institutional Knowledge at Singapore Management University
publishDate 2016
url https://ink.library.smu.edu.sg/sis_research/4937
https://ink.library.smu.edu.sg/context/sis_research/article/5940/viewcontent/Satisfiability.pdf
_version_ 1770575151633530880