research
∙
04/25/2023
Resource Specifications for Resource-Manipulating Programs
Specifications for modular program verifiers are expressed as constraint...
share
research
∙
10/18/2022
Compositional Reasoning for Side-effectful Iterators and Iterator Adapters
Iteration is a programming operation that traditionally refers to visiti...
research
∙
02/11/2022
REST: Integrating Term Rewriting with Program Verification (Extended Version)
We introduce REST, a novel term rewriting technique for theorem proving ...
research
∙
05/29/2021
Formally Validating a Practical Verification Condition Generator (extended version)
A program verifier produces reliable results only if both the logic used...
research
∙
04/20/2021
Modular Verification of Collaborating Smart Contracts
Smart contracts are programs that execute inside blockchains such as Eth...
research
∙
11/19/2019
Local Reasoning for Global Graph Properties
Separation logics are widely used for verifying programs that manipulate...
research
∙
08/16/2019
Modular Verification of Heap Reachability Properties in Separation Logic
The correctness of many algorithms and data structures depends on reacha...
research
∙
04/11/2018