Leo Freitas. 

We present results from the mechanisation of a priority queue and its operations. Our interest comes from its use in the specification and refinement of a scheduler for OS kernels for embedded real-time devices. It is part of a pilot project within the international Grand Challenge in Verified Software. Our work uncovers important hidden and missing properties, and their relation to kernel design.

http://www.springerlink.com/content/m5h2p7r64u6w1pt6/

Processando consulta.