- BASIL, formerly bil-to-boogie-translator Translating lifted Aarch64 binaries to boogie annotated weakest pre-condition and rely/guarantee for information flow.
-
bap Fork of CMU Binary Analysis Platform with the ASLp plugin and primus lisp semantics. ASLp is used by default instead of the primus semantics.
- The home of the previous project to provide Aarch64 semantics to bap manually using its Primus lisp plugin framework
- barrier-tools Tools used in writing the BAP Primus semantics. Contains some scripts useful for exploring BAP's lifter
- qemu
- BAP QEMU fork instrumented to provide traces for comparing BAP generated semantics. Supports basic instructions with partial support for SIMD and FP instructions.
-
gtirb-semantics In-progress project to use the GTIRB lifter with instruction level semantics provided by ASLp, (to replace BAP)
-
wemelt An earlier information flow logic verifier for a source code language
-
ASL Lifter Project (FMCAD 2023)
- aslp The Architecture Specification Language interpreter (ASLi) partial evaluator (ASLp)
- bap-asli-plugin BAP plugin for lifting aarch64, with instruction-level semantics provided by the ASL partial evaluator (ASLp)
- llvm-translator Tool for evaluating and comparing ASLp against existing lifters using Alive2
-
wpif_csf2021 Isabelle theories for Backwards-directed information flow analysis for concurrent programs CSF'21 paper
-
wmm-rg Isabelle theories for a Rely/guarantee logic for weak memory models based on interfering thread-local instruction pairs
