source: src/ERTL/ERTLToLTLProof.ma

Revision Log Mode:


Legend:

Added
Modified
Copied or renamed
Diff Rev Age Author Log Message
(edit) @3388   6 years piccolo partial commit
(edit) @3372   7 years piccolo Added new implementation of labelling approach based on LTS and …
(edit) @3371   7 years piccolo Modified RTLsemantics and ERTLsemantics. Now the pop frame will set …
(edit) @3261   7 years piccolo reverted joint_semantics rtl_semantics and ltl_semantics
(edit) @3259   7 years piccolo changed ERTL semantics: 1) added manipulation of stack pointer …
(edit) @3253   7 years piccolo some proof obbligation closed of ERTL to LTL proof
(edit) @3252   7 years piccolo proof obbligation added on ERTL to LTL proof
(add) @3217   7 years piccolo Correctness of ERTL to LTL in place
Note: See TracRevisionLog for help on using the revision log.