Verificarea programelor

Anul IV, Sem.1 2006-2007, Fac. Mat.-Inf, Univ. Bucuresti
Profesor: Stefanescu, Gheorghe
Asistent: Dragoi, Cezara

Cursuri

• Lec00: Probleme organizatorice
• Lec01: Logica propozitionala 1: Deductie naturala [pdf]
• Lec02: Logica propozitionala 2: Sintaxa, semantica, corectitudine & completitudine [pdf]
• Lec03: Logica propozitionala 2: Forme normale, etc. [pdf]
• Lec04: Logica predicatelor 1: Sintaxa, deductie naturala [pdf]
• Lec05: Logica predicatelor 2: Demonstratii, semantica, nedecidabilitatea validitatii [pdf]
• Lec06: Logica predicatelor 3: Forme normale, deductie, programare logica [pdf]
• Lec07: Model checking 1: CTL*, sintaxa, semantica, exemple [pdf]
• Lec08: Model checking 2: Algorithm de model checking; SMV [pdf]
• Lec09: Model checking 3: Exemple, corectitudine, extensii [pdf]
• Lec10: Verificarea prorgamelor 1: Logica Floyd-Hoare - I [pdf]
• Lec11: Verificarea prorgamelor 2: Logica Floyd-Hoare - II [pdf]
• Lec12: Logica predicatelor 4: Corectitudine si completitudine; Teorema de incompletitudine Godel [pdf]
• Lec13: Specificatii spatio-temporale [pdf]
• Lec14: Sisteme interactive cu registri si voci (rv-sisteme) [pdf]
• Lec15: Logica Floyd pentru rv-programe [pdf]
• Lec16: Lectie invitata, Drd Cezara Dragoi: Rv-programe structurate si verificarea lor [pdf, a se posta]