VerC3: Verification Toolkit for C3
Switch branches/tags
Nothing to show
Clone or download
Pull request Compare This branch is even with icsa-caps:master.
Fetching latest commit…
Cannot retrieve the latest commit at this time.
Permalink
Type Name Latest commit message Commit time
Failed to load latest commit information.
doc/api
include/verc3
site_scons/site_tools
src
test
third_party
.clang-format
.clang_complete
.gitignore
.gitmodules
AUTHORS
CONTRIBUTING.rst
Doxyfile
LICENSE
NOTICE
README.rst
SConstruct

README.rst

VerC3: Verification Toolkit for C3

Contains a library for explicit-state model checking in C++. Example models can be found in src/models.

Current features:

  • Symmetry reduction.
  • Several search strategies: memory-usage friendly hashing of states only; and precise but more demand on memory usage.
  • Synthesis.

Build Instructions

Dependencies:

  • TCMalloc (optional, but improves performance noticeably)
$ ./third_party/update.sh
$ scons -j4 # add --release for optimized build

Running

$ ./build/bin/verc3 runmodel list
$ ./build/bin/verc3 runmodel <model-name>

Citation

If you use this library or any parts of the code in your work, we would appreciate if you cite:

@inproceedings{ElverBJN2018,
  author    = {Marco Elver and Christopher J. Banks and Paul Jackson and
               Vijay Nagarajan},
  title     = {{VerC3}: {A} {L}ibrary for {E}xplicit {S}tate {S}ynthesis of
               {C}oncurrent {S}ystems},
  booktitle = {Design, Automation {\&} Test in Europe (DATE)},
  publisher = {{IEEE}},
  month     = mar,
  year      = {2018},
  venue     = {Dresden, Germany}
}