diff -r 24e6884d9258 -r 6f50e6a8c6e0 Journal/Paper.thy --- a/Journal/Paper.thy Tue Mar 04 08:45:11 2014 +0000 +++ b/Journal/Paper.thy Tue Mar 04 09:40:40 2014 +0000 @@ -28,7 +28,7 @@ original_priority ("priority") and DUMMY ("\<^raw:\mbox{$\_\!\_$}>") - + (*>*) section {* Introduction *} @@ -1465,7 +1465,7 @@ pointed out an error in a paper about Preemption Threshold Scheduling \cite{ThreadX}. The use of a theorem prover was invaluable to us in order to be confident about the correctness of our reasoning - (no case can be overlooked). + (no case can be overlooked). The most closely related work to ours is the formal verification in PVS of the Priority Ceiling Protocol done by Dutertre \cite{dutertre99b}---another solution to the Priority Inversion