Peizun Liu

Peizun Liu

PhD Candidate @ Computer Science


About Me

I am a Computer Science Ph.D. student at Khoury college 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.

News

  • Our paper Verifying Asynchronous Event-Driven Programs using Partial Abstract Transformers is accepted by CAV.

  • I am interning at MathWorks this summer. My work is to formally reason about simulink models.

Research

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.

Projects

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 shared-memory recursive programs. See CUBA for more details.

    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 in P language. The work will be out soon. Email me for a draft if you are interested.


  • Parameterized Verification

    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.

Publications

  1. Peizun Liu, Thomas Wahl and Akash Lal, "Verifying Asynchronous Event-Driven Programs Using Partial Abstract Transformers". To appear in CAV, 2019. [Preprint]

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

  3. 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]

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

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

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

Teaching

Activities

Conference PC member:

ICSEA 2018, ICSEA 2017

Conference reviewing:

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

This Site