Peizun Liu

Peizun Liu

PhD Candidate @ Computer Science

About Me

I am a Computer Science Ph.D. student at CCIS and a member of Formal Methods group. Before joining Northeastern, I graduate with a Master's degree in Software Engineering from Tsinghua University and a Bachelor's degree in Information Management & Information System from Chengdu University of Technology.


  • I am doing my summer internship at The MathWorks, and am working on formal verification.
  • Our CUBA work (see below) is accepted by PLDI'18.


Research Interests

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 details.

  • 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.


  1. Peizun Liu and Thomas Wahl, “CUBA: Interprocedural Context-Unbounded Analysis of Concurrent Programs”. In PLDI, pp.105-119, 2018. [PDF|Artifact]

  2. Peizun Liu and Thomas Wahl, “IJIT: An API for Boolean Program Analysis with Just-in-Time Translation”. In SEFM, pp.316-331, 2017. [PDF|Slides|Artifact]

  3. Peizun Liu and Thomas Wahl, "Concolic Unbounded-Thread Reachability via Loop Summaries". In ICFEM, pp.346-362, 2016. [PDF|Slides|Artifact]

  4. Konstantinos Athanasiou, Peizun Liu and Thomas Wahl, "Unbounded-Thread Program Verification using Thread-State Equations". In IJCAR, pp. 516-531, 2016. [PDF|Slides|Artifact].

  5. Peizun Liu and Thomas Wahl, "Infinite-State Backward Exploration of Boolean Broadcast Programs". In FMCAD, pp.155-162, 2014. [PDF|Slides|Artifact]



Conference PC member:

ICSEA 2018, ICSEA 2017

Conference reviewing:

VMCAI 2018, CAV 2017, FMCAD 2017, CAV 2015, CAV 2014, FMCAD 2014, DATE 2014, CAV 2013, FMCAD 2013, DATE 2013

This Site