forked from ondrik-research-archived/spen
-
Notifications
You must be signed in to change notification settings - Fork 1
SeParation logic ENtailment
License
mihasighi/spen
This commit does not belong to any branch on this repository, and may belong to a fork outside of the repository.
Folders and files
Name | Name | Last commit message | Last commit date | |
---|---|---|---|---|
Repository files navigation
About ===== This is a decision procedure for entailment problems between formulas in the fragment of Separation Logic with Recursive Definitions (SLRD) defined in [FIT-TR-2014-01]. Requires ======== To compile: - a C99 compiler (tested under gcc) - GNU flex >= 2.5.33 - GNU bison (tested under bison 2.7.0) - SMTLIB2 parser of Alberto Griggio available at https://es.fbk.eu/people/griggio/misc/smtlib2parser.html To execute: - MINISAT solver available at http://minisat.se/ and compiled with the incremental feature (see README_incremental_minisat.txt) Installation ============ 1) Configuring: - change the SMTLIB2_PREFIX variable in the Makefile.config file with the directory where can be found the libsmtlib2parser.so - (optional) change the compiler name or the compilation flags for the C compiler 2) Compiling: - do 'make' in src directory 3) Install: - put the 'minisat' tool in the PATH - move the 'spen' binary to a known executable path libVATA ======= libVATA is provided as a Git submodule fetching a specific revision of the library from Github. 1) Download with $ git submodule init $ git submodule update 2) Compile with $ cd libvata $ make release - or '$ make debug' for a debug version - or '$ MAKE="make -j" make release' (or debug) for faster compilation (on a multicore machine) 3) See the examples in libvata/examples 4) When the libVATA submodule is updated, you need to run again $ git submodule update
About
SeParation logic ENtailment
Resources
License
Stars
Watchers
Forks
Releases
No releases published
Packages 0
No packages published
Languages
- C 74.8%
- C++ 24.3%
- Other 0.9%