43 citations · 61 across the 22 of their papers we have counts for
6 papers · 1 filter
Worst-Case Input Generation for Concurrent Programs under Non-Monotone Resource Metrics
Long Pham, Jan Hoffmann
Worst-case input generation aims to automatically generate inputs that exhibit the worst-case performance of programs. It has several applications, and can, for example, detect vul…
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…
Typable Fragments of Polynomial Automatic Amortized Resource Analysis
Long Pham, Jan Hoffmann
Being a fully automated technique for resource analysis, automatic amortized resource analysis (AARA) can fail in returning worst-case cost bounds of programs, fundamentally due to…
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…
Defunctionalization of Higher-Order Constrained Horn Clauses
Long Pham, Steven J. Ramsay, C. -H. Luke Ong
Building on the successes of satisfiability modulo theories (SMT), Bjørner et al. initiated a research programme advocating Horn constraints as a suitable basis for automatic progr…