Skip to content

Formal proof of a presburger abstract domain on a SSA language

Notifications You must be signed in to change notification settings

math-fehr/PresburgerAI-Coq

Folders and files

NameName
Last commit message
Last commit date

Latest commit

 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 

Repository files navigation

documentation link

Building

Generate a makefile and run the makefilw with:

$ coq_makefile -f _CoqProject -o Makefile && make
Using nix for build environments

To use nix, the purely functional package manager to automatically setup the correct build environment, run nix-shell at the folder with default.nix (top-level folder).

bash$ nix-shell
[nix-shell]: coq_makefile -f _CoqProject -o Makefile && make

This should never fail if the nix-shell succeeds.

About

Formal proof of a presburger abstract domain on a SSA language

Resources

Stars

Watchers

Forks

Releases

No releases published

Packages

No packages published

Languages