Repositories list

• DuoAI

  Public
  Duo is an automated tool to formally verify distributed protocols (e.g., Paxos) by inferring inductive invariants.

  C++

  •

  BSD 3-Clause "New" or "Revised" License

  •3•9•0•0•Updated May 1, 2025May 1, 2025

• sosp-paper211-ae-proof

  Public
  Mirror of sosp-paper211-ae-proof

  Coq

  •

  GNU General Public License v2.0

  •3•1•0•1•Updated Jan 26, 2023Jan 26, 2023

• VIA

  Public
  Mirror of Artifact for OSDI 22 Paper: Design and Verification of the Arm Confidential Compute Architecture

  Coq

  •

  GNU General Public License v3.0

  •0•3•0•0•Updated Jul 15, 2022Jul 15, 2022

• sosp-paper211-ae

  Public
  Mirror of Artifact for SOSP 21 Paper: Verifying a Multiprocessor Hypervisor on Arm Relaxed Memory Hardware

  Shell

  •

  GNU General Public License v2.0

  •2•3•0•0•Updated Jul 15, 2022Jul 15, 2022

• DistAI

  Public
  DistAI: Data-Driven Automated Invariant Learning for Distributed Protocols

  Python

  •2•17•0•0•Updated Jan 1, 2022Jan 1, 2022

• E6998-Formal-Verification

  Public
  Coq

  •0•0•0•0•Updated Nov 9, 2021Nov 9, 2021

• VRM-proof

  Public
  Coq

  •

  GNU General Public License v2.0

  •0•1•0•0•Updated Nov 4, 2021Nov 4, 2021

• VRM

  Public
  Artifact for SOSP 21 Paper: Verifying a Multiprocessor Hypervisor on Arm Relaxed Memory Hardware

  Shell

  •

  GNU General Public License v2.0

  •2•7•0•0•Updated Nov 4, 2021Nov 4, 2021

• usenix-ae-linux

  Public
  C

  •

  Other

  •2•3•0•0•Updated Nov 4, 2021Nov 4, 2021

• vct-qemu

  Public
  C

  •

  Other

  •3•0•0•0•Updated Sep 19, 2021Sep 19, 2021

• qemu-3.0-SeKVM

  Public
  Modified QEMU for SeKVM

  C

  •

  Other

  •2•3•0•0•Updated Sep 18, 2021Sep 18, 2021

• SeKVM-4.18

  Public
  Verified KVM on Arm Relaxed Memory Hardware

  C

  •

  Other

  •2•6•0•0•Updated Sep 18, 2021Sep 18, 2021

• Certified-Conccurrent-Abstraction-Layers

  Public
  HTML

  •0•0•0•0•Updated Feb 27, 2020Feb 27, 2020