1 citations · 2 across the 4 of their papers we have counts for
6 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…