Automated verification of the freeRTOS scheduler in HIP/SLEEK
Automated verification of operating system kernels is a challenging problem, partly due to the use of shared mutable data structures. In this paper, we show how we can automatically verify memory safety and functional correctness of the task scheduler component of the FreeRTOS kernel using the verif...
| Autor principal: | |
|---|---|
| Outros Autores: | , |
| Formato: | conferencePaper |
| Idioma: | eng |
| Publicado em: |
2012
|
| Assuntos: | |
| Texto completo: | http://hdl.handle.net/1822/38093 |
| País: | Portugal |
| Oai: | oai:repositorium.sdum.uminho.pt:1822/38093 |