Infinite-state backward exploration of Boolean broadcast programs. - Peizun Liu; Thomas Wahl (FMCAD, 2014)

Unbounded-Thread Reachability via Symbolic Execution and Loop Acceleration (Technical Report). - Peizun Liu; Thomas Wahl (CoRR, 2015)

Unbounded-Thread Program Verification using Thread-State Equations. - Konstantinos Athanasiou; Peizun Liu; Thomas Wahl (IJCAR, 2016)

Concolic Unbounded-Thread Reachability via Loop Summaries. - Peizun Liu; Thomas Wahl (ICFEM, 2016)

Concolic Unbounded-Thread Reachability via Loop Summaries (Extended Technical Report). - Peizun Liu; Thomas Wahl (CoRR, 2016)

IJIT: An API for Boolean Program Analysis with Just-in-Time Translation. - Peizun Liu; Thomas Wahl (SEFM, 2017)

IJIT: An API for Boolean Program Analysis with Just-in-Time Translation (Extended Technical Report). - Peizun Liu; Thomas Wahl (CoRR, 2017)

CUBA: interprocedural Context-UnBounded Analysis of concurrent programs. - Peizun Liu; Thomas Wahl (PLDI, 2018)

CUBA: Interprocedural Context-UnBounded Analysis of Concurrent Programs (Extended Manuscript). - Peizun Liu; Thomas Wahl (CoRR, 2018)

Verifying Asynchronous Event-Driven Programs Using Partial Abstract Transformers. - Peizun Liu; Thomas Wahl; Akash Lal (CAV (2), 2019)

Verifying Asynchronous Event-Driven Programs Using Partial Abstract Transformers (Extended Manuscript). - Peizun Liu; Thomas Wahl; Akash Lal (CoRR, 2019)

Interprocedural Context-Unbounded Program Analysis Using Observation Sequences. - Peizun Liu; Thomas Wahl; Thomas W. Reps (ACM Trans. Program. Lang. Syst., 2021)