17 citations · 20 across the 8 of their papers we have counts for
11 papers
DrNLA: Extending Verification to Non-linear Programs through Dual Re-writing
Yuandong Cyrus Liu, Ton-Chanh Le, Timos Antonopoulos +2
For many decades, advances in static verification have focused on linear integer arithmetic (LIA) programs. Many real-world programs are, however, written with non-linear integer a…
An algebra of alignment for relational verification
Timos Antonopoulos, Eric Koskinen, Ton Chanh Le +3
Relational verification encompasses information flow security, regression verification, translation validation for compilers, and more. Effective alignment of the programs and comp…
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…
Automated Lemma Synthesis in Symbolic-Heap Separation Logic
Quang-Trung Ta, Ton Chanh Le, Siau-Cheng Khoo +1
The symbolic-heap fragment of separation logic has been actively developed and advocated for verifying the memory-safety property of computer programs. At present, one of its bigge…
Automated Mutual Explicit Induction Proof in Separation Logic
Quang-Trung Ta, Ton Chanh Le, Siau-Cheng Khoo +1
We present a sequent-based deductive system for automatically proving entailments in separation logic by using mathematical induction. Our technique, called mutual explicit inducti…
Preliminary Notes on Termination and Non-Termination Reasoning
Ton Chanh Le
In this preliminary note, we will illustrate our ideas on automated mechanisms for termination and non-termination reasoning.