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 programs, etc.
Please find more details for each project in its corresponding project website.
Resource-Parameterized Program Analysis using Observation Sequences
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 using observation sequences
Recently, we applied the observation sequences to the undecidable problem of
context-unbounded reachability analysiss. See CUBA for more
Reachability Analysis for Abstract Unbounded-Thread Programs
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.