2 citations · 5 across the 5 of their papers we have counts for
5 papers
Verifying Asynchronous Event-Driven Programs Using Partial Abstract Transformers (Extended Manuscript)
Peizun Liu, Thomas Wahl, Akash LaL
We address the problem of analyzing asynchronous event-driven programs, in which concurrent agents communicate via unbounded message queues. The safety verification problem for suc…
CUBA: Interprocedural Context-UnBounded Analysis of Concurrent Programs (Extended Manuscript)
Peizun Liu, Thomas Wahl
A classical result by Ramalingam about synchronization-sensitive interprocedural program analysis implies that reachability for concurrent threads running recursive procedures is u…
IJIT: An API for Boolean Program Analysis with Just-in-Time Translation (Extended Technical Report)
Peizun Liu, Thomas Wahl
Exploration algorithms for explicit-state transition systems are a core back-end technology in program verification. They can be applied to programs by generating the transition sy…
Concolic Unbounded-Thread Reachability via Loop Summaries (Extended Technical Report)
Peizun Liu, Thomas Wahl
We present a method for accelerating explicit-state backward search algorithms for systems of arbitrarily many finite-state threads. Our method statically analyzes the program exec…
Unbounded-Thread Reachability via Symbolic Execution and Loop Acceleration (Technical Report)
Peizun Liu, Thomas Wahl
We present an approach to parameterized reachability for communicating finite-state threads that formulates the analysis as a satisfiability problem. In addition to the unbounded n…