My research interests are program analysis and formal
verification. The goal of my research is to improve the
reliability of various types of software, especially the
critical system software, device drivers, etc. My recent work
focuses on formally analyzing concurrent programs, distributed
Please find more details for each project in its
corresponding project webpage.
Resource-Parameterized Program Analysis
Resource-parameterized programs are omnipresent as the
majority of programs including critical ones are naturally
designed, intentionally or not, over a variable number of
certain resources. Although highly desirable, formally
analyzing said programs are notoriously hard or even
intractable in many cases. Resource bounds are thus
imposed to ensure the tractability of the analysis, and
lead to a series of incomplete techniques in turn that
are, however, believed to catch "most bugs" in
practice. The question whether these techniques can also
prove the absence of bugs at least in some cases has
remained largely open.
We address this question by introducing a broad verification
methodology for resource-parameterized programs that
observes how changes to the resource parameter affect the
behavior of the program. We call our methodology as
observation sequences. This is an ongoing project.
1. Context-unbounded analysis (CUBA)
We have applied the observation sequences to the undecidable problem of
context-unbounded reachability analysis for multithreaded
programs. See CUBA for more
2. Queue-unbounded analysis (QUBA)
Recently, we applied the observation sequences to the
queue-unbounded reachability analysis for asynchronous
event-driven programs. Those programs communicate via
unbounded FIFO message queues. We evaluate our approach on
a set of benchmark programs written
language. The work will be out soon. Email me for a
draft if you are interested.
1. Reachability analysis for abstract Boolean programs with just-in-time translation
We apply the just-in-time
translation idea to a well-known infinite-state backward reachability analysis algorithm to avoid the state space explosion usually cased by static translation.
This is the project
UCOB. Then, we extend the idea by providing an API IJIT
to help users to adjust their transition system based algorithms / tools to algorithms
/ tools operating on Boolean programs directly.
2. Symbolic analysis for unbounded-thread programs
We encode reachability questions in a way that makes it expressible compactly as a Presburger arithmetic formulae. Then, we feed the formulae to a SMT solver, e.g. Z3, to approximate the reachability. More details in CUTR, TSE.