GitPlanet

Cheap and reliable Node.js hosting starts at $3/month, and $1/month static HTML hosting

Created with love in Canada, visit hostnodejs.com today

Feel like to post an Ad? Learn Details
All Projects → smackers → Smack

smackers / Smack

Licence: other
SMACK Software Verifier and Verification Toolchain

Programming Languages

c
50402 projects - #5 most used programming language
rust
11053 projects

Labels

llvmverificationsmt

Projects that are alternatives of or similar to Smack

Alive2
Automatic verification of LLVM optimizations
Stars: ✭ 199 (-34.75%)
Mutual labels:  llvm, verification, smt
Stp
Simple Theorem Prover, an efficient SMT solver for bitvectors
Stars: ✭ 341 (+11.8%)
Mutual labels:  verification, smt
Pysmt
pySMT: A library for SMT formulae manipulation and solving
Stars: ✭ 352 (+15.41%)
Mutual labels:  verification, smt
Sbv
SMT Based Verification in Haskell. Express properties about Haskell programs and automatically prove them using SMT solvers.
Stars: ✭ 125 (-59.02%)
Mutual labels:  verification, smt
Sat smt by example
"SAT/SMT by example" free ebook
Stars: ✭ 339 (+11.15%)
Mutual labels:  verification, smt
Seahorn
SeaHorn Verification Framework
Stars: ✭ 270 (-11.48%)
Mutual labels:  llvm, verification
Liquidhaskell
Liquid Types For Haskell
Stars: ✭ 863 (+182.95%)
Mutual labels:  verification, smt
Fstar
A Proof-oriented Programming Language
Stars: ✭ 2,171 (+611.8%)
Mutual labels:  verification, smt
Sea Dsa
A new context, field, and array-sensitive heap analysis for LLVM bitcode based on DSA.
Stars: ✭ 90 (-70.49%)
Mutual labels:  llvm, verification
Stainless
Verification framework and tool for higher-order Scala programs
Stars: ✭ 241 (-20.98%)
Mutual labels:  verification, smt
Alive
Alive: Automatic LLVM's Instcombine Verifier
Stars: ✭ 204 (-33.11%)
Mutual labels:  llvm, verification
Symbiotic
Symbiotic is a tool for finding bugs in computer programs based on instrumentation, program slicing and KLEE
Stars: ✭ 212 (-30.49%)
Mutual labels:  llvm, verification
Olifant
A simple programming language targeting LLVM
Stars: ✭ 58 (-80.98%)
Mutual labels:  llvm
Clang Power Tools
Bringing clang-tidy magic to Visual Studio C++ developers.
Stars: ✭ 285 (-6.56%)
Mutual labels:  llvm
kolibrios-llvm
KolibriOS ported to LLVM
Stars: ✭ 31 (-89.84%)
Mutual labels:  llvm
smt
A Go library that implements a Sparse Merkle tree for a key-value map.
Stars: ✭ 83 (-72.79%)
Mutual labels:  smt
Awesome Graal
A curated list of awesome resources for Graal, GraalVM, Truffle and related topics
Stars: ✭ 302 (-0.98%)
Mutual labels:  llvm
Kremlin
KreMLin is a tool for extracting low-level F* programs to readable C code
Stars: ✭ 285 (-6.56%)
Mutual labels:  verification
Ruscall
自作言語処理系のコンパイラ制作
Stars: ✭ 41 (-86.56%)
Mutual labels:  llvm
vercors
The VerCors verification toolset for verifying parallel and concurrent software
Stars: ✭ 30 (-90.16%)
Mutual labels:  verification
View All Similar Projects ➔

master branch ci status develop branch ci status

SMACK Logo

SMACK is both a modular software verification toolchain and a self-contained software verifier. It can be used to verify the assertions in its input programs. In its default mode, assertions are verified up to a given bound on loop iterations and recursion depth; it contains experimental support for unbounded verification as well. SMACK handles complicated feature of the C language, including dynamic memory allocation, pointer arithmetic, and bitwise operations.

Under the hood, SMACK is a translator from the LLVM compiler's popular intermediate representation (IR) into the Boogie intermediate verification language (IVL). Sourcing LLVM IR exploits an increasing number of compiler front-ends, optimizations, and analyses. Currently SMACK only supports the C language via the Clang compiler, though we are working on providing support for additional languages. Targeting Boogie exploits a canonical platform which simplifies the implementation of algorithms for verification, model checking, and abstract interpretation. Currently, SMACK leverages the Boogie and Corral verifiers.

See below for system requirements, installation, usage, and everything else.

We are very interested in your experience using SMACK. Please do contact Zvonimir or Michael with any possible feedback.

Support

  • For general questions, first consult the FAQ.

  • If something is otherwise broken or missing, open an issue.

  • As a last resort, send mail to Michael, Zvonimir, or both.

  • To stay informed about updates, you can either watch SMACK's Github page, or you can join SMACK's Google Group mailing list. Even without a Google account, you may join by sending mail to [email protected].

Acknowledgements

SMACK project has been partially supported by funding from the National Science Foundation, VMware, and Microsoft Research. We also rely on University of Utah's Emulab infrastructure for extensive benchmarking of SMACK.

Table of Contents

  1. System Requirements and Installation
  2. Running SMACK
  3. Demos
  4. FAQ
  5. Inline Boogie Code
  6. Contribution Guidelines
  7. Projects
  8. Publications
  9. People
Note that the project description data, including the texts, logos, images, and/or trademarks, for each open source project belongs to its rightful owner. If you wish to add or remove any projects, please contact us at [email protected].