Beskjeder

Plan for den f?rste delen av undervisningen er ute.  Her kan det bli endel endringer hvis jeg trenger ? reise noe sted, og/eller basert p? ?nsker fra studentene.  Tenker vi starter med de tre obligatiske oppgavene (finne feil i kommunikasjonsprotokoll; meta-programmering; lage interpret til enkelt imperativt spr?k) i f?rste delen av semesteret, og tar studentpresentasjoner av ymse temaer i emnets andre del.  Ligger an til undervisningsfri/jobbing med obliger i slutten av september.

Very tentative schedule for the first month published. There could be significant changes, based on my needs to travel for work, and/or wishes by the students. After intro to Maude, I guess we start with the three mandatory assignments (finding mistakes in published communication protocols; meta-programming; defining an intepreter/semantics for simple imperative languages) in the first part of the course, and student presentations of selected papers in the second...

Emnet ser p? ulike aspekter ved formell modellering og analyse av distributerte systemer.  For eksempel ser vi p? sanntidssystemer og probabilistiske systemer. Vi har ogs? en introduksjon til meta-programmering. Som alltid: disse er fundamentale begreper som ikke er knyttet til omskrivningslogikk, men vi eksemplifiserer dem ved bruk av omskrivningslogikk (og formalismen og verkt?yet Maude).  Vi studerer ogs? hvordan man kan definere semantikken/en interpret til et programmeringsspr?k i Maude.  Til sist ser vi p? endel eksempler p? bruk av formelle metoder til ymse systemer, som for eksempel cloud-baserte transaksjonssystemer, modellering av biokjemiske reaksjoner, analyse av smarte kontrakter, hvordan knekke web browsere og VISA/MasterCard ved bruk av formelle metoder, finne feil i DNS, og s? videre.  Vi starter med repetisjon/kort introduksjon av Maude, og deretter ser om vi kan knekke en liten publisert kommunikasjonsprotokoll.  Deretter noen felles...