Skip to content

dbueno/horn2vmt

master
Switch branches/tags

Name already in use

A tag already exists with the provided branch name. Many Git commands accept both tag and branch names, so creating this branch may cause unexpected behavior. Are you sure you want to create this branch?
Code

Latest commit

 

Git stats

Files

Permalink
Failed to load latest commit information.
Type
Name
Latest commit message
Commit time
lib
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 

Horn2VMT

This is a proof of concept implementation of the paper, "Horn2VMT: Translating Horn Reachability into Transition Systems," available online at http://eptcs.web.cse.unsw.edu.au/content.cgi?VPTHCVS2020#EPTCS320.13.

This tool converts linear Horn clauses into a transition system format, VMT, described at the nuXmv site. VMT is SMT-LIBv2 compatible.

Dependencies

  • Z3 - 4.8.7 is tested but earlier should work
  • LLVM - 5 & 10 tested but in between should work
  • CMake 3.14
  • Boost 1.67
  • fmtlib - in a submodule of this repo

install recipe

git submodule init
git submodule update
cmake -DZ3_DIR=/opt/z3-4.8.7/ \
    -DLLVM_DIR=/opt/clang+llvm-10.0.0-x86_64-apple-darwin/ ..

usage

horn2vmt file.smt2 > file.vmt

Reproducible build

nix-build -E "with import (fetchTarball "https://github.com/NixOS/nixpkgs/archive/058b981b5bd.tar.gz") {}; callPackage (builtins.fetchurl "https://raw.githubusercontent.com/dbueno/horn2vmt/master/default.nix") {}"
./result/bin/horn2vmt -h

About

Translation from (linear) Horn clauses into VMT, a logic-based transition system format

Resources

Stars

Watchers

Forks

Releases

No releases published

Packages

No packages published