Skip to content

Port non-seq aRTA

Sergey Bozhko requested to merge sbozhko/rt-proofs:port-nonseq-arta into master

Mostly it is just a copy-paste of the old Abstract RTA.

However, I add a new section FixpointIsNoLessThanArrival in file abstract_rta.v; so comments are very welcome.

PDF-file for convenience: abstract.core.abstract_rta.pdf

Edited by Sergey Bozhko

Merge request reports