The LSTS frontend requires support for logical corollaries that "mixin" to existing functions and code. A corollary could be something like certification of the memory model etc. and works by producing extra type information beyond the direct local types.
The LSTS frontend requires support for logical corollaries that "mixin" to existing functions and code. A corollary could be something like certification of the memory model etc. and works by producing extra type information beyond the direct local types.