Pensumboken er
Peter C. Ölveczky: Designing Reliable Distributed Systems: A Formal Methods Approach Based on Executable Modeling in Maude. Springer 2018 (står muligens 2017 i boken). Boken skal være tilgjengelig hvis man sitter på UiO's nettverk. Forhåpentligvis er boken til salgs på campus.
Som hovedregel er boken, alle forelesninger med foiler, ukeoppgaver med løsningsforslag og obligatoriske oppgaver pensum. Fra kompendiet utgår fotnoter og de markerte "ikke-pensum" delene (avsnittene merket med "stjerne"). Kapitlene 7 (og muligens 17, vi får se hvor langt vi kommer) er ikke pensum i IN-2100. Beviset for at terminering er uavgjørbart (med Turingmaskiner og greier) og den elegante teorien rundt forenklingsordninger er dessverre ikke pensum. Dvs i kapittel 4.1 utgår alt unntatt stoffet til og med Theorem 4.1 (beviset er ikke pensum). Videre utgår kapittel 4.4 t.o.m. side 78, og 4.4.3 (dvs 4.4.1 og 4.4.2 er pensum, men ikke resten av 4.4).
I tillegg er artikkelen "How Amazon Web Services Uses Formal Methods" pensum.
Støttelitteratur
Maude hjemmeside for manual, download, etc.
Filen prelude.maude leses inn automatisk av Maude og inneholder blant annet definisjonen av de innebygde modulene. Nyttig!
Maude for Windows
Emnet benytter språket/systemet Maude. Maude kan lastes opp enkelt for Linux og MacOS fra http://maude.cs.illinois.edu. Det enkleste og beste for Windows-brukere har vært å laste ned Ubuntu eller lignende, og kjøre Maude der. Maude for Windows har dermed ikke vært problematisk tidligere. Merk at vi ikke skal bruke CVC-4 eller noen annen SMT solver i kurset, så man trenger ikke å laste opp CVC-4 (eller Yices).
Husk også at Ifi's linux-maskiner alle har installert Maude: bare å gi kommandoen maude.