Skip to content

Latest commit

 

History

History
25 lines (18 loc) · 1.2 KB

README.md

File metadata and controls

25 lines (18 loc) · 1.2 KB

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>