research
∙
06/27/2023
DrNLA: Extending Verification to Non-linear Programs through Dual Re-writing
For many decades, advances in static verification have focused on linear...
share
research
∙
02/09/2022
An algebra of alignment for relational verification
Relational verification encompasses information flow security, regressio...
research
∙
11/04/2021
Source-Level Bitwise Branching for Temporal Verification
There is increasing interest in applying verification tools to programs ...
research
∙
05/11/2021
Proving LTL Properties of Bitvector Programs and Decompiled Binaries (Extended)
There is increasing interest in applying verification tools to programs ...
research
∙
10/12/2020
DynamiTe: Dynamic Termination and Non-termination Proofs
There is growing interest in termination reasoning for non-linear progra...
research
∙
08/26/2019
Automated Verification of CountDownLatch
The CountDownLatch (CDL) is a versatile concurrency mechanism that was f...
research
∙
03/22/2019
SLING: Using Dynamic Analysis to Infer Program Invariants in Separation Logic
We introduce a new dynamic analysis technique to discover invariants in ...
research
∙
03/18/2019
Specification and Inference of Trace Refinement Relations
Modern software is constantly changing. Researchers and practitioners ar...
research
∙
10/26/2017