The following are unreleased features in Vericert that are currently being worked on and have not been completely proven correct yet. Currently this includes features such as:
This page gives some preliminary information on how the features are implemented and how the proofs for the features are being done. Once these features are properly implemented, they will be added to the proper documentation.
Scheduling #
Scheduling is an optimisation which is used to run
Operation Chaining #
Scheduling is an optimisation which is used to run
If-conversion #
If-conversion
Loop pipelining #
Loop pipelining
Functions #
Functions.