3 citations · 5 across the 9 of their papers we have counts for
4 papers · 1 filter
S2TD: a Separation Logic Verifier that Supports Reasoning of the Absence and Presence of Bugs
Quang Loc Le, Jun Sun, Long H. Pham +1
Heap-manipulating programs are known to be challenging to reason about. We present a novel verifier for heap-manipulating programs called S2TD, which encodes programs systematicall…
Compositional Verification of Heap-Manipulating Programs through Property-Guided Learning
Long H. Pham, Jun Sun, Quang Loc Le
Analyzing and verifying heap-manipulating programs automatically is challenging. A key for fighting the complexity is to develop compositional methods. For instance, many existing…
Concolic Testing Heap-Manipulating Programs
Long H. Pham, Quang Loc Le, Quoc-Sang Phan +1
Concolic testing is a test generation technique which works effectively by integrating random testing generation and symbolic execution. Existing concolic testing engines focus on…
Enhancing Inductive Entailment Proofs in Separation Logic with Lemma Synthesis
Quang Loc Le
This paper presents an approach to lemma synthesis to support advanced inductive entailment procedures based on separation logic. We first propose a mechanism where lemmas are auto…