Proving LTL Properties of Bitvector Programs and Decompiled Binaries. - Yuandong Cyrus Liu; Chengbin Pang; Daniel Dietsch; Eric Koskinen; Ton-Chanh Le; Georgios Portokalidis; Jun Xu 024 (APLAS, 2021)

Source-Level Bitwise Branching for Temporal Verification of Lifted Binaries. - Yuandong Cyrus Liu; Chengbin Pang; Daniel Dietsch; Eric Koskinen; Ton-Chanh Le; Georgios Portokalidis; Jun Xu 024 (CoRR, 2021)

Source-Level Bitwise Branching for Temporal Verification. - Yuandong Cyrus Liu; Ton-Chanh Le; Eric Koskinen (CoRR, 2021)

DrNLA: Extending Verification to Non-linear Programs through Dual Re-writing. - Yuandong Cyrus Liu; Ton-Chanh Le; Timos Antonopoulos; Eric Koskinen; ThanhVu Nguyen (CoRR, 2023)

VESC: Towards Temporal Verification of Smart Contracts. - Samuel Larsen; Kevin Johanson; Yuandong Cyrus Liu (SPLASH Companion, 2024)