3 citations · 5 across the 9 of their papers we have counts for
9 papers
An Efficient Cyclic Entailment Procedure in a Fragment of Separation Logic
Quang Loc Le, Xuan-Bach D. Le
An efficient entailment proof system is essential to compositional verification using separation logic. Unfortunately, existing decision procedures are either inexpressive or ineff…
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…
Bi-Abduction for Shapes with Ordered Data
Christopher Curry, Quang Loc Le
Shape analysis is of great importance for the verification of the correctness and memory-safety of heap-manipulating programs, yet such analyses have been shown to be highly diffic…
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…
Decidable Logics Combining Word Equations, Regular Expressions and Length Constraints
Quang Loc Le
In this work, we consider the satisfiability problem in a logic that combines word equations over string variables denoting words of unbounded lengths, regular languages to which w…
Enhancing Symbolic Execution of Heap-based Programs with Separation Logic for Test Input Generation
Long H. Pham, Quang Loc Le, Quoc-Sang Phan +2
Symbolic execution is a well established method for test input generation. Despite of having achieved tremendous success over numerical domains, existing symbolic execution techniq…
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…
A Decision Procedure for String Logic with Equations, Regular Membership and Length Constraints
Quang Loc Le
In this paper, we consider the satisfiability problem for string logic with equations, regular membership and Presburger constraints over length functions. The difficulty comes fro…