Skip to content

Lightweight formal verification system developed to support research on usability of automated proof verification tools.

License

Notifications You must be signed in to change notification settings

aartifact/aartifact-verifier

Folders and files

NameName
Last commit message
Last commit date

Latest commit

 

History

42 Commits
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 

Repository files navigation

aartifact-verifier

Lightweight formal verification system developed to support research on usability of automated proof verification tools.

Background

This repository has been posted for archival purposes. The work that involved this verification system is described in a number of publications and reports (listed below):

Subsequent publications describe later versions of the verification system inspired by the version in this repository:

Building and installing

Run the usual cabal command from the project's root directory:

cabal install

Running

A number of example proof scripts can be found in the examples directory. They can be processed as is done with the example below:

aartifact -ascii examples/test.txt

The ASCII output should look as follows:

\vbeg
Introduce !!>$x$<!!.
Assume !!>$x = 5$<!!.
Assert !!>$x = 5$<!!.
Assert <<<$x = 6$>>>.
\vend

About

Lightweight formal verification system developed to support research on usability of automated proof verification tools.

Topics

Resources

License

Stars

Watchers

Forks