Information Technology Reference
In-Depth Information
The diculty lay in making the right design decisions for the formalisation.
We generally tried to model the Isabelle proofs on the paper-and-pencil proofs
of the literature, but especially for the colouring, it turned out to be better
to develop a new constructive proof from scratch. In that particular case, as
mentioned above, the original code contained a mistake, which we discovered
during our vain efforts to prove the code correct.
Concerning the first optimisation, there is also a more sophisticated algorithm
[3]. However this algorithm relies on the
edge
labels in an automaton and thus
it is not immediately possible to implement this algorithm in our scenario.
Our formalisation consists of around 1500 lines of code (approximately 3000
lines of code if the formalisation of Tarjan's SCC algorithm is counted).
References
1. Clarke, E.M., Grumberg, O., Peled, D.A.: Model Checking, 5th print. MIT Press
(2002)
2. Esparza, J., Lammich, P., Neumann, R., Nipkow, T., Schimpf, A., Smaus, J.-G.:
A fully verified executable LTL model checker. In: Sharygina, N., Veith, H. (eds.)
CAV 2013. LNCS, vol. 8044, pp. 463-478. Springer, Heidelberg (2013)
3. Etessami, K., Holzmann, G.J.: Optimizing Buchi automata. In: Palamidessi, C.
(ed.) CONCUR 2000. LNCS, vol. 1877, pp. 153-167. Springer, Heidelberg (2000)
4. Gerth,R.,Peled,D.,Vardi,M.Y.,Wolper,P.:Simpleon-the-flyautomaticverifica-
tion of linear temporal logic. In: Dembinski, P., Sredniawa, M. (eds.) Proceedings
of the 15th International Symposium on Protocol Specification, Testing, and Veri-
fication. IFIP Conference Proceedings, vol. 38, pp. 3-18. Chapman and Hall (1996)
5. Holzmann, G.J.: The SPIN Model Checker - primer and reference manual. Addison-
Wesley (2004)
6. Lammich, P., Tuerk, T.: Applying data refinement for monadic programs to
Hopcroft's algorithm. In: Beringer, L., Felty, A. (eds.) ITP 2012. LNCS, vol. 7406,
pp. 166-182. Springer, Heidelberg (2012)
7. Nipkow, T., Paulson, L.C., Wenzel, M.: Isabelle/HOL. LNCS, vol. 2283. Springer,
Heidelberg (2002)
8. Schimpf, A., Merz, S., Smaus, J.-G.: Construction of Buchi automata for LTL
model checking verified in Isabelle/HOL. In: Berghofer, S., Nipkow, T., Urban,
C., Wenzel, M. (eds.) TPHOLs 2009. LNCS, vol. 5674, pp. 424-439. Springer,
Heidelberg (2009)
9. Tarjan, R.E.: Depth-first search and linear graph algorithms. SIAM J. Com-
put. 1(2), 146-160 (1972)
10. Thomas, W.: Automata on infinite objects. In: Handbook of Theoretical Computer
Science, Volume B: Formal Models and Semantics (B), pp. 133-192. Elsevier and
MIT Press (1990)
