Projects using K
Featured
-
The K semantics of the C programming language specifies the translation, linking, and execution semantics of the C language according to the official C standard. It has been used to build tools like RV-Match, which detects undefined behaviors in users programs by running their test-suites through the C semantics.
-
KWasm is the K semantics of WebAssembly. WebAssembly is a low-level (but simple and streamlined) assembly language that was originally developed to provide a fast execution engine for browser-based tools. More recently, it has been used in several blockchain smart-contract platforms as the underlying language for executing financial agreements. KWasm has been used for measuring coverage of test-suites over Wasm code and verifying programs which are compiled to Wasm.
-
IELE is the underlying VM integrated into the Cardano blockchain. IELE is a register-based VM (inspired by LLVM), which attempts to avoid many of the missteps in design present in EVM.
-
KEVM is the K semantics of the Ethereum Virtual Machine. It passes all of the Ethereum Test Suite, and is used for verifying EVM programs.
-
K-Michelson (Oct 2019 - Present)
K-Michelson is the K semantics of Michelson blockchain programming language, which powers the Tezos blockchain. KMichelson provides additional testing tools for developers, including a unit-testing framework which is extendable to symbolic property testing.
-
Presents an executable formal semantics for Boogie, an intermediate language for verification. The K semantics of Boogie provides an independent verification engine for programs compiled to Boogie. This, for example, allows Dafny users to either discharge their verification goals using Boogie or using the K semantics of Boogie.
-
The semantics of Elrond is a wrapper around KWasm which extends it with the Elrond blockchain primitives. This extension enables developers targeting the Elrond blockchain to measure coverage of their test-suite directly at the Wasm level.
Archived
- llvm (2011-2018)
- python (2012-2013)
- java (2012-2016)
- ocaml (2012-2013)
- javascript (2013-2015)
- aadl (2013-2013)
- alk (2013-2014)
- cink (2013-2015)
- jvm (2013-2014)
- modelink (2013-2013)
- javacard (2014-2014)
- orc (2016-2017)
- haskell core (2016-2017)
- plutus core (2016-2019)
- p4 (2016-2020)
- X86-64 (2017-2020)
- vyper (2017-2018)
- erc20 (2017-2018)
- solidity (2018-2019)
- eei (2018-2019)
- erc777 (2018-2018)
- k (2018-2020)
- yul (2019-2019)
- KEwasm (2019-2020)
- hybrid programs (2020-2020)