Sonar helps you commit clean C++ code every time. With over 550 unique rules to find C++ bugs, code smells & vulnerabilities, Sonar finds the issues while you focus on the work. Learn more →
Alive2 Alternatives
Similar projects and alternatives to alive2
-
CrossHair
An analysis tool for Python that blurs the line between testing and type systems.
-
recreational-rosette
Some fun examples of solving problems with symbolic execution
-
Sonar
Write Clean C++ Code. Always.. Sonar helps you commit clean C++ code every time. With over 550 unique rules to find C++ bugs, code smells & vulnerabilities, Sonar finds the issues while you focus on the work.
-
Symbolica
Symbolica's open-source symbolic execution engine. [Moved to: https://github.com/Symbolica/Symbolica] (by SymbolicaDev)
-
-
-
-
ONLYOFFICE
ONLYOFFICE Docs — document collaboration in your environment. Powerful document editing and collaboration in your app or environment. Ultimate security, API and 30+ ready connectors, SaaS or on-premises
-
-
-
coq
Coq is a formal proof management system. It provides a formal language to write mathematical definitions, executable algorithms and theorems together with an environment for semi-interactive development of machine-checked proofs.
-
x86-sat
Basic SAT model of x86 instructions using Z3, autogenerated from Intel docs
-
-
NOTE:
The number of mentions on this list indicates mentions on common posts plus user suggested alternatives.
Hence, a higher number means a better alive2 alternative or higher similarity.
alive2 reviews and mentions
Posts with mentions or reviews of alive2.
We have used some of these posts to build our list of alternatives
and similar projects. The last one was on 2023-05-15.
-
Basic SAT model of x86 instructions using Z3, autogenerated from Intel docs
You can use it to (mostly) validate small snippets are the same. See Alive2 for the application of Z3/formalization of programs as SMT for that [1]. As far as I'm aware there are some problems scaling up to arbitrarily sized programs due to a lack of formalization in higher level languages in addition to computational constraints. With a lot of time and effort it can be done though [2].
-
Verifying GCC optimizations using an SMT solver
Yeah, this kind of thing is nice.
Alive had been used for years (almost a decade actually) by people to verify LLVM instcombine transforms.
Alive2 (https://github.com/AliveToolkit/alive2) makes it easier to do the same with most optimization passes.
-
Programming in Z3 by learning to think like a compiler
Alive/Alive2 [1] is one of the most famous frameworks for compiler transformation verification using BitVec logic
-
A note from our sponsor - Sonar
www.sonarsource.com | 2 Jun 2023
Stats
Basic alive2 repo stats
4
474
2.1
11 days ago
AliveToolkit/alive2 is an open source project licensed under MIT License which is an OSI approved license.
The primary programming language of alive2 is C++.
Access the most powerful time series database as a service
Ingest, store, & analyze all types of time series data in a fully-managed, purpose-built database. Keep data forever with low-cost storage and superior data compression.
www.influxdata.com