Peizun Liu

Peizun Liu

Senior SWE @ Google


About Me

Highlights

  • A self-motivated researcher, engineer, problem solver, and deep thinker with an interdisciplinary mindset.

  • Published a series of research results in top journals & conferences, like ACM TOPLAS, PLDI, CAV, ICJAR, etc.

  • Established expertise in cloud computing, network systems, firewall, distributed systems, programming languages, program analysis and formal verification.

  • Extensive communication & leadership skills: worked as a tech lead at Google, and worked as a head TA for multiple semesters at Northheastern University.

News


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-Aware Program Analysis

    See RAPA for more details.


  • 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 Thomas Reps. "Interprocedural Context-Unbounded Program Analysis Using Observation Sequences." In ACM TOPLAS, Vol. 42, Issue. 4, pp.1-34, 2020.

  2. Peizun Liu, Thomas Wahl and Akash Lal. "Verifying Asynchronous Event-Driven Programs Using Partial Abstract Transformers." In CAV, pp.386-404, 2019.

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

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

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

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

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

Service

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

Teaching

I have been teaching the following classes (as a head TA):


This Site