Skip to content

Verification-condition-generation-based verifier for the Viper intermediate verification language.

License

Notifications You must be signed in to change notification settings

viperproject/carbon

Repository files navigation

Carbon

Carbon is a verification-condition-generation-based verifier for the Viper intermediate verification language.

The Viper project is developed by the Programming Methodology group at ETH Zurich.

See the documentation wiki for instructions on how to try out or install the Viper tools.

Installation Instructions:

We recommend using carbon through the VS Code plugin. Alternatively, one can compile carbon from source with the following steps:

  • Install Z3 and Boogie and set the environment variables Z3_EXE and BOOGIE_EXE correspondingly (see wiki above)
  • Clone this repository recursively by running:
    git clone --recursive https://github.com/viperproject/carbon

And then

  • Compile and run with:
    sbt "run [options] <path to Viper file>"
  • Alternatively, for a faster startup without compilation each time, build a .jar file:
    sbt assembly
    And then run with:
    java -jar ./target/scala-*/carbon.jar [options] <path to Viper file>

About

Verification-condition-generation-based verifier for the Viper intermediate verification language.

Topics

Resources

License

Stars

Watchers

Forks

Packages

No packages published

Languages