Viited
OCaml
- Learn OCaml ametlikul veebilehel.
- OCaml from the Very Beginning.
- OCaml Programming: Correct + Efficient + Beautiful — Cornelli ülikooli kursus.
Püsipunktid
- Introduction to Compiler Design, peatükk 1.5.1.
Mudelkontroll
- TLA+ — üks mudelkontrolli süsteem.
- How Amazon Web Services uses formal methods — mudelkontroll Amazonis.
Abstraktne interpretatsioon
- Jan Midtgaard-i slaidid — abstraktse interpretatsiooni talvekoolist.
- Compiler Design: Analysis and Transformation, peatükid 1.5, 1.9-1.10.
- Tutorial on Static Inference of Numeric Invariants by Abstract Interpretation, peatükid 1.1, 2.1, 3.5, 4.1-4.5.
- Static Program Analysis, peatükid 4, 5.1-5.2.
- Abstract interpretation: application to verification and static analysis — LIP6 kursus Prantsusmaal.
Automaatsed teoreemitõestajad
- Z3Py Guide — Z3 Python-i teegi tutorial.
- Programming Z3.
- SAT/SMT by Example.
- Z3 OCaml-i API.
Hoare'i loogika
- Programming Language Foundations, peatükid Hoare, Hoare2, HoareAsLogic — Coq-is formaliseeritud.
- Algoritmid ja andmestruktuurid, peatükk 8 — eestikeelne.
Võrrandisüsteemid
- Introduction to Compiler Design, peatükk 2.7, lisa A.4.3.
- Compiler Design: Analysis and Transformation, peatükid 1.5, 1.12.
- Static Program Analysis, peatükid 4.4, 5.3.
- Frameworks for analyzing multi-threaded C — Kalmer Apinise doktoritöö.
- Three improvements to the top-down solver — Goblint-is kasutusel olev TD3 solver.