research
∙
03/02/2023
Securing Verified IO Programs Against Unverified Code in F*
We introduce SCIO*, a formally secure compilation framework for statical...
share
research
∙
04/12/2021
A Note on the Performance of Algorithms for Solving Linear Diophantine Equations in the Naturals
We implement four algorithms for solving linear Diophantine equations in...
research
∙
07/19/2020
Who Verifies the Verifiers? A Computer-Checked Implementation of the DPLL Algorithm in Dafny
We build a SAT solver implementing the DPLL algorithm in the verificatio...
research
∙
07/01/2020
A Typo in the Paterson-Wegman-de Champeaux algorithm
We investigate the Paterson-Wegman-de Champeaux linear-time unification ...
research
∙
01/27/2020
Operationally-based Program Equivalence Proofs using LCTRSs
We propose an operationally-based deductive proof method for program equ...
research
∙
09/04/2019
Verifying the DPLL Algorithm in Dafny
Modern high-performance SAT solvers quickly solve large satisfiability i...
research
∙
07/11/2019
Trace-Relating Compiler Correctness and Secure Compilation
Compiler correctness is, in its simplest form, defined as the inclusion ...
research
∙
02/22/2019
Reducing Total Correctness to Partial Correctness by a Transformation of the Language Semantics
We give a language-parametric solution to the problem of total correctne...
research
∙
10/25/2018
All-Path Reachability Logic
This paper presents a language-independent proof system for reachability...
research
∙
04/23/2018