Skip to content

affeldt-aist/seplog

Folders and files

NameName
Last commit message
Last commit date

Latest commit

 

History

22 Commits
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 

Repository files navigation

ARCHIVE Formal verification of low-level programs using Separation Logic

Contents

The purpose of this repository is to serve as an archive for the code corresponding to the following papers:

Requirements

Coq version 8.12.1, MathComp 1.12.0

Install

coq_makefile -o Makefile -f _CoqProject

Install X only, where X \in {SEPLOG,BBS,BEGCD,SEPLOGC}

coq_makefile -o Makefile -f _CoqProject; make

Doc

make -f MakeDoc (once everything has been compiled)

see https://staff.aist.go.jp/reynald.affeldt/coqdev/

Releases

No releases published

Packages

No packages published

Languages