17 citations · 39 across the 12 of their papers we have counts for
10 papers · 1 filter
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…
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…
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…
Program Verification via Predicate Constraint Satisfiability Modulo Theories
Hiroshi Unno, Yuki Satake, Tachio Terauchi +1
This paper presents a verification framework based on a new class of predicate Constraint Satisfaction Problems called pCSP where constraints are represented as clauses modulo firs…
Reducing Commutativity Verification to Reachability with Differencing Abstractions
Eric Koskinen, Kshitij Bansal
Commutativity of data structure methods is of ongoing interest, with roots in the database community. In recent years commutativity has been shown to be a key ingredient to enablin…
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…
Automatic Generation of Precise and Useful Commutativity Conditions (Extended Version)
Kshitij Bansal, Eric Koskinen, Omer Tripp
Reasoning about commutativity between data-structure operations is an important problem with applications including parallelizing compilers, optimistic parallelization and, more re…