AliveToolkit / alive2 Star 824 Code Issues Pull requests Discussions Automatic verification of LLVM optimizations llvm verification symbolic-execution model-checking smt llvm-ir translation-validation automatic-verification Updated Dec 29, 2024 C++
nyu-systems / gauntlet Star 35 Code Issues Pull requests Finding bugs in P4 compilers using translation validation. p4c z3 p4 translation-validation Updated Oct 19, 2024 P4
kframework / p4-semantics Star 20 Code Issues Pull requests Formal Semantics of P4 in K interpreter formal-semantics verification symbolic-execution model-checking p4language p4 translation-validation Updated May 21, 2021 P4
seL4 / graph-refine Star 12 Code Issues Pull requests proof sel4 translation-validation refinement-proof Updated Mar 29, 2023 Python
xzhseh / translation-validator Star 3 Code Issues Pull requests Validate semantic equivalence between C++ and Rust LLVM IR using State-Of-The-Art Verification z3 smt llvm-ir translation-validation alive2 Updated Dec 11, 2024 C++
sdasgup3 / PLDI20-Artifact-Evaluation Star 0 Code Issues Pull requests Artifact Evaluation, PLDI'20 validation virtualbox x86-64 reverse-engineering evaluation formal-semantics symbolic-execution-engine compiler-optimization graph-matching llvm-ir pldi verification-conditions language-semantics translation-validation mcsema symbolic-summaries verification-queries detecting-bugs reproducing-bugs Updated Apr 18, 2020