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 → nunoplopes → Alive

nunoplopes / Alive

Licence: apache-2.0
Alive: Automatic LLVM's Instcombine Verifier

Programming Languages

python
139335 projects - #7 most used programming language

Labels

llvmverification

Projects that are alternatives of or similar to Alive

Alive2
Automatic verification of LLVM optimizations
Stars: ✭ 199 (-2.45%)
Mutual labels:  llvm, verification
Seahorn
SeaHorn Verification Framework
Stars: ✭ 270 (+32.35%)
Mutual labels:  llvm, verification
Smack
SMACK Software Verifier and Verification Toolchain
Stars: ✭ 305 (+49.51%)
Mutual labels:  llvm, verification
Symbiotic
Symbiotic is a tool for finding bugs in computer programs based on instrumentation, program slicing and KLEE
Stars: ✭ 212 (+3.92%)
Mutual labels:  llvm, verification
Sea Dsa
A new context, field, and array-sensitive heap analysis for LLVM bitcode based on DSA.
Stars: ✭ 90 (-55.88%)
Mutual labels:  llvm, verification
Dstep
A tool for converting C and Objective-C headers to D modules
Stars: ✭ 177 (-13.24%)
Mutual labels:  llvm
Fakepdb
Tool for PDB generation from IDA Pro database
Stars: ✭ 186 (-8.82%)
Mutual labels:  llvm
Md5 File
return an md5sum of a given file
Stars: ✭ 176 (-13.73%)
Mutual labels:  verification
Laravel2step
Laravel 2-Step verification is a package to add 2-Step user authentication to any Laravel project easily. It is configurable and customizable. It uses notifications to send the user an email with a 4-digit verification code. Laravel 2-Step Authentication Verification for Laravel. Can be used in out the box with Laravel's authentication scaffolding or integrated into other projects.
Stars: ✭ 175 (-14.22%)
Mutual labels:  verification
Android Play Safetynet
Samples for the Google SafetyNet Attestation API
Stars: ✭ 195 (-4.41%)
Mutual labels:  verification
Awesome Llvm
A curated list of awesome LLVM related docs, tools, and other resources.
Stars: ✭ 184 (-9.8%)
Mutual labels:  llvm
Constexpr Everything
Rewrite C++ code to automatically apply `constexpr` where possible
Stars: ✭ 178 (-12.75%)
Mutual labels:  llvm
Scilla
Scilla - A Smart Contract Intermediate Level Language
Stars: ✭ 186 (-8.82%)
Mutual labels:  verification
Webassembly Examples
From Simple To Complex. A complete collection of webassembly examples.
Stars: ✭ 177 (-13.24%)
Mutual labels:  llvm
How To Write An Llvm Register Allocator
This repository contains a tutorial for a quick start in how to write a register allocator using LLVM
Stars: ✭ 197 (-3.43%)
Mutual labels:  llvm
Play with llvm
A book about LLVM & Clang（中文开源书：玩转 LLVM）
Stars: ✭ 175 (-14.22%)
Mutual labels:  llvm
Yansollvm
Yet Another Not So Obfuscated LLVM
Stars: ✭ 180 (-11.76%)
Mutual labels:  llvm
Reopt
A tool for analyzing x86-64 binaries.
Stars: ✭ 190 (-6.86%)
Mutual labels:  llvm
Clang Expand
🐉 A clang tool for happy refactoring without source-code gymnastics
Stars: ✭ 182 (-10.78%)
Mutual labels:  llvm
Whileycompiler
The Whiley Compiler (WyC)
Stars: ✭ 181 (-11.27%)
Mutual labels:  verification
View All Similar Projects ➔

Alive: Automatic LLVM's Instcombine Verifier

Alive is a tool that can prove the correctness of InstCombine optimizations specified in a high-level language.

NOTE: Alive is in maintenance mode; no new features are planned. Please try Alive2 instead.

Requirements

Alive requires Python 2.7.x and Z3 4.3.2 (or later), which can be obtained from https://github.com/Z3Prover/z3 (use the unstable branch)

Usage

./alive.py file.opt

The 'tests' directory has multiple examples of optimizations.

More Information

Please see this paper for more details about Alive:

http://www.cs.utah.edu/~regehr/papers/pldi15.pdf

Online Version

Alive is also available online at: http://rise4fun.com/Alive

Generating Benchmarks

Alive will automatically generate benchmarks in SMT-LIB 2 format when the 'bench' directory exists and when python is run in non-optimized mode (the default). These benchmarks are over the bit-vector theory and may or may not have quantifiers.

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].