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

Quick links:

 

Publications

2016

2015

2014

2013

2012

2011

2010

Sidebar