Velkommen til IN5100/Welcome to IN5100

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 temaer (sanntid/prob systemer, etc), og til sist ymse temaer/artikler som studenter skal presentere.  Har man tatt IN2100 har man forkunnskapene man trenger.  Mange studenter har gjort det tipp-topp i emnet uten ? ha tatt IN2100.   Ingen pensumbok (selv om IN2100-boken "Designing Reliable Distributed Systems" kan v?re nyttig for en kjapp intro til Maude). Vi vil basere oss p? artikler, som jeg og studenter vil presentere.

Emnet vil enten bli gitt p? norsk eller engelsk.

The course will be given in Norwegian or English, depending on who is attending.