Pensum vil best? av en samling artikler, som blir delt ut p? forelesning eller linket fra forelesningsplanen etterhvert.
Z. Manna og A. Pnueli: Temporal Verification of Reactive Systems: Safety, Springer-Verlag, 1995. Kap. 0, 74 s.
Z. Manna og A. Pnueli: Adequate Proof Principles for Invariance and Liveness Properties of Concurrent Programs. Science of Computer Programming 4: 257-289. 1984.
G. Holzmann: The Model Checker SPIN. IEEE Transactions on Software Engineering 23(5):279-295. 1997.
G. Holzmann: The Spin Model Checker. Addison-Wesley, 2004.
- Kap. 6: Automata & Logic, 25 s.
- Kap. 7: Promela Semantics, 13 s.
- Kap. 8: Search Algorithms, 26 s.
- Appendix A: Automata Products, 9 s.
Artikkel om branching og linear time temporal logikk.
I tillegg vil obliger og forelesningsmateriale v?re pensum.
V?r oppmerksom p? at denne pensumoversikten kan bli justert etterhvert.