Executable Semantic Framework (K Framework)
The K Framework is being developed jointly by the FSL group at UIUC lead by Grigore Rosu together with the FMSE group lead by Dorel Lucanu.
In this page we include specific information related to the contribution of FMSE group at this project. For more general information visit the oficial page for K Framework: http://kframework.org/.
FMSE group contributed to:
- development of the first versions of the tool (until 3.4). Now FMSE group is partially involved in the development of the parser;
- incorporating Maude LTL model checker
- formalization and prototyping of the symbolic execution engine;
- formalization and prototyping of a verification procedure based on symbolic execution and circular coinduction;
- formalization and prototyping of the program equivalence
- complete definition of Java Semantics
- complete definition of Javacard Semantics
- partial definition of JVM
Contents
Quick links:
- K Framework home page
- Github repository for the K Tool
- Java Semantics
- Online interface for K3.4 (including the symbolic execution prototype)
- Javacard Semantics
- JVM semantics