Dette emnet er erstattet av IN9100 – Utvalgte emner i omskrivningslogikk.

INF9130 – Utvalgte emner i omskrivningslogikk

Timeplan, pensum og eksamensdato

Velg semester

Kort om emnet

Emnet er en fortsettelse av INF3230 /INF4231  og tar for seg grunnleggende teori rundt omskrivningslogikk som Knuth-Bendix-komplettering, refleksjon og metaprogrammering, samt eksempler på avanserte anvendelser av omskrivningslogikk til modellering og analyse av systemer i verktøyet Maude. Aktuelle systemer å modellere kan være sikkerhets- og nettverksprotokoller, sanntidssystemer, mobile systemer og biokjemiske prosesser.

Hva lærer du?

Etter å ha tatt INF9130

- har du bedre kompetanse på formell modellering og analyse av
  distribuerte systemer på et høyt abstraksjonsnivå, og spesielt
  kunnskap om omskrivingslogikk-baserte verktøy,

- vet du hva meta-programmering er, og du forstår begrepene
  refleksjon og metanivåberegning innen omskrivningslogikk;
  spesielt kan du definere ad hoc strategier for gjennomføring og
  analyse av Maude moduler ved hjelp av
  meta-programmeringsmulighetene i Maude,

- har du god kjennskap av state-of-the-art anvendelser av
  omskrivningslogikk innen bestemte domener, som for eksempel
  biokjemiske prosesser, sanntidsdatasystemer og mobile prosesser,

- kan du spesifisere og analysere systemkrav ved bruk av temporal
  logikk og modellsjekking, og særlig ved hjelp av Maudes
  modellsjekker for lineær tid,

- kjenner du avanserte omskriving-logikk-baserte analyseteknikker
  for distribuerte systemer som innsnevring og domenetilpassede
  strategispråk,

- har du en bedre innsikt i hvordan å lese og forstå vitenskapelige artikler,

- har du bedre trening i vitenskapelige presentasjoner.

Opptak og adgangsregulering

Ph.d.-kandidater ved UiO søker plass på undervisningen og melder seg til eksamen i Studentweb.

Hvis emnet har begrenset kapasitet, vil ph.d.-kandidater som har emnet i sin utdanningsplan ved UiO bli prioritert. Noen nasjonale forskerskoler kan ha egne regler for rangering av søkere til emner med begrenset kapasitet.

Ph.d.-kandidater som har opptak ved andre utdanningsinstitusjoner må innen angitt frist søke om hospitantplass.

Overlappende emner

10 studiepoeng overlapp mot INF5130 – Utvalgte emner i omskrivningslogikk (videreført)

Undervisning

To til tre timer undervisning per uke (forelesning eller gruppeøvelse). Det kreves innlevering av obligatoriske oppgaver. Les mer om krav til innlevering av oppgaver, gruppearbeid og lovlig samarbeid under retningslinjer for obligatoriske oppgaver.

Eksamen

Studenten skal holde en muntlig presentasjon som teller 1/3 av den endelige karakteren. En muntlig eksamen teller 2/3. Dersom mange studenter følger emnet, kan eksamen bli skriftlig. De obligatoriske oppgavene må være bestått for å kunne gå opp til eksamen.

Karakterskala

Emnet bruker karakterskala bestått/ikke bestått. Les mer om karakterskalaen.

Begrunnelse og klage

Adgang til ny eller utsatt eksamen

Studenter som dokumenterer gyldig fravær fra ordinær eksamen, kan ta utsatt eksamen i starten av neste semester.

Det tilbys ikke ny eksamen til studenter som har trukket seg under ordinær eksamen, eller som ikke har bestått.

Trekk fra eksamen

Det er mulig å ta eksamen i emnet inntil tre ganger. Dersom du trekker deg fra eksamen etter fristen eller under eksamen, bruker du et eksamensforsøk.

Annet

Det er sterkt anbefalt å møte på første forelesning fordi det vil bli gitt viktig informasjon.

Fakta om emnet

Studiepoeng

10

Nivå

Ph.d.

Undervisning

Høst 2019

Høst 2015

Høst 2013

Høst 2011

Annethvert høstsemester. Ikke høst 2017.

Eksamen

Annethvert høstsemester.

Undervisningsspråk

Norsk (engelsk på forespørsel)