17 citations · 39 across the 12 of their papers we have counts for
15 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…
Veracity: Declarative Multicore Programming with Commutativity
Adam Chen, Parisa Fathololumi, Eric Koskinen +1
There is an ongoing effort to provide programming abstractions that ease the burden of exploiting multicore hardware. Many programming abstractions (e.g., concurrent objects, trans…
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…
Constraint-based Relational Verification
Hiroshi Unno, Tachio Terauchi, Eric Koskinen
In recent years they have been numerous works that aim to automate relational verification. Meanwhile, although Constrained Horn Clauses (CHCs) empower a wide range of verification…
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…