A refinement-based verification framework for preemptive OS kenerls.
Download : https://coq.inria.fr/distrib/V8.5/files/coq-8.5.tar.gz
- Dowload coq8.5
- ./configure -prefix path_to_install_coq
- make && make install.
- vim ~/.bashrc
- add command "export coq85bin=path_to_install_coq" to .bashrc
- cd CertiuCOS2/coqimp
- make -j4 certiucos/proofs/ucos_correct.vo (32G Memory at least)
- Extending our separation logic assertion to support half permission, which is able to specify more complicated protocols used in OS kernels.
- Do NOT require arbitrary client code for system APIs, we can specify our expectation for the client code with the specification language.
- Extend the framework to support reasoning about task creation and deletion, and the corresponding APIs in uC/OS-II have been verified in our new framework.