6 papers · 1 filter
Source-Level Bitwise Branching for Temporal Verification
Yuandong Cyrus Liu, Ton-Chanh Le, Eric Koskinen
There is increasing interest in applying verification tools to programs that have bitvector operations. SMT solvers, which serve as a foundation for these tools, have thus increase…
Proving LTL Properties of Bitvector Programs and Decompiled Binaries (Extended)
Yuandong Cyrus Liu, Chengbin Pang, Daniel Dietsch +4
There is increasing interest in applying verification tools to programs that have bitvector operations (eg., binaries). SMT solvers, which serve as a foundation for these tools, ha…
DynamiTe: Dynamic Termination and Non-termination Proofs
Ton Chanh Le, Timos Antonopoulos, Parisa Fathololumi +2
There is growing interest in termination reasoning for non-linear programs and, meanwhile, recent dynamic strategies have shown they are able to infer invariants for such challengi…
Automated Verification of CountDownLatch
Wei-Ngan Chin, Ton Chanh Le, Shengchao Qin
The CountDownLatch (CDL) is a versatile concurrency mechanism that was first introduced in Java 5, and is also being adopted into C++ and C#. Its usage allows one or more threads t…
Specification and Inference of Trace Refinement Relations
Timos Antonopoulos, Eric Koskinen, Ton-Chanh Le
Modern software is constantly changing. Researchers and practitioners are increasingly aware that verification tools can be impactful if they embrace change through analyses that a…
SLING: Using Dynamic Analysis to Infer Program Invariants in Separation Logic
Ton Chanh Le, Guolong Zheng, ThanhVu Nguyen
We introduce a new dynamic analysis technique to discover invariants in separation logic for heap-manipulating programs. First, we use a debugger to obtain rich program execution t…