Skip to content

SPARK formal verification automated with Travis CI

License

Notifications You must be signed in to change notification settings

jklmnn/continuous-verification

Folders and files

NameName
Last commit message
Last commit date

Latest commit

 

History

11 Commits
 
 
 
 
 
 
 
 
 
 
 
 

Repository files navigation

Continuous Verification

This repository aims to show an example how to automatically prove Ada/SPARK software with Travis CI. The current process consists of downloading and installing the GPL versions of GNAT and SPARK and then build and prove the project.

With the current state it is possible to:

  • check if the project builds without Ada warnings
  • automatically run the SPARK proof
  • fail the CI test if SPARK does not prove

To use the GitHub template simply create a new repository from it, enable Travis and replace the src directory and the .gpr file with your own. Then change the CV_PROJECT variable in .travis.yml to your own project file.

About

SPARK formal verification automated with Travis CI

Resources

License

Stars

Watchers

Forks

Releases

No releases published

Packages

No packages published

Languages