5840 Software-Analyse - WS 2009/10

Organisatorisches

Vorlesungen (1 Vorlesung mit 2 SWS):
Donnerstags 14:00 - 15:30, IM HS 11, Dirk Beyer
(Fuer Inf.-Dipl.: Die Veranstaltung zaehlt als 3 SWS VL, da die dritte SWS Vorlesung als Block in Form von projektbezogener Stoffvermittlung abgehalten wird.)

Uebungen (1 Gruppe mit 1 SWS):
Donnerstags 18:00 - 18:45, IM HS 12, Dirk Beyer

Sprechstunde (Voranmeldung via E-Mail):
Donnerstags 15:30 - 17:00, IM 131, Dirk Beyer

Hinweise:
Wir bieten Vorlesungen und Uebungen an. Sie sind herzlich willkommen zur Sprechstunde, um ueber Ihre Resultate, Probleme und Sorgen mit uns zu sprechen. Die Uebungsleiter und ich werden Ihnen gern weiterhelfen. Falls Sie den Faden verlieren, Hilfe wuenschen, oder einfach nur ueber Softwaretechnik sprechen moechten, bitte sprechen Sie mich an --- lassen Sie sich nicht im Stoff zurueckfallen! Senden Sie mir eine E-Mail mit einem individuellen Termin.

Termine:

Erste Vorlesung:	Do, 2009-10-22
Letzte Vorlesung:	Do, 2010-02-11
Pruefung:	muendlich, Termine: 2010-03-11 und 2010-04-30

Prozeduren

Web-Page. Diese Web-Seite sollte die akkurateste und verlaesslichste Informationsquelle zu unserer Vorlesung sein.
Falls Sie einen Fehler finden oder irgendetwas unklar sein sollte, bitte kontaktieren Sie uns umgehend.
E-Mail. Kontaktieren Sie uns via E-Mail oder vereinbaren Sie einen Termin um uns zu sehen.
Stellen Sie bitte sicher, '5840-WS2009' (und die Uebungsblatt-Nummer) im Betreff zu erwaehnen bei jeder E-Mail.
Bewertung. Die Note wird allein durch das Ergebnis der muendlichen Pruefung ermittelt. Jedoch ist eine regelmaessige Teilnahme an der Vorlesung sowie die bescheinigt erfolgreiche Durchfuehrung des Semesterprojektes Vorraussetzung zur Anmeldung der muendlichen Pruefung.

Inhalt der Vorlesung

Modulbeschreibung
Informationen auf Stud-IP

Kurzuebersicht zur Vorlesung:

Program analysis, data-flow analysis
Abstract domains and abstract interpretation
Software model checking, counterexample-guided abstraction refinement
Generation of program invariants
Testing, test-case generation, directed random testing
Analysis of the structure of large software systems
Relational programming
Software visualization
Interfaces and component-based design, web service interfaces
Finite state verification
Data structures for representing finite state sets
Infinite state verification, in particular real-time systems
Data structures for representing infinite state sets
Applications of theorem proving

Literatur (Bibliothek der Uni Passau)

Carlo Ghezzi, Dino Mandrioli, Mehdi Jazayeri. Fundamentals of Software Engineering. Prentice Hall, 2002.
Gerard J. Holzmann. The SPIN Model Checker: Primer and Reference Manual. Addison-Wesley, 2003.
Flemming Nielson, Hanne Riis Nielson, Chris Hankin. Principles of Program Analysis. Springer, 2005.

Mehr Literatur-Referenzen

Vorlesungsinhalte, Uebungsblaetter, Lese-Material

(Angaben wie Kapitel und Abschnitte beziehen sich auf das Lehrbuch.)

Week 1 (2009-10-22):

VL Di: Organization
VL Do: Overview software analysis, introduction to computer-aided verification, formal verification, testing, system - specification - model - implementation, model checking
Reading: Alur&Henzinger Chapter 0

Week 2 (2009-10-29):

VL: Invariant verification and reachability analysis, transition system, states
Reading: Alur&Henzinger Chapter 2

Week 3 (2009-11-05):

VL: Reachability problem, enumerative search algorithm, symbolic state sets, symbolic search algorithm

Week 4 (2009-11-12):

VL: Symbolic invariant verification, binary decision diagrams
Reading: Alur&Henzinger Chapter 3.1

Week 5 (2009-11-19):

VL: Binary decision diagrams, data-flow analysis (introduction, lattices)
Reading: Alur&Henzinger Chapter 3.2

Week 6 (2009-12-03):

VL: Data-flow analysis (abstract domain, examples, transfer relation)

Week 7 (2009-12-10):

VL: Data-flow analysis (iteration algorithm, constant propagation, reaching definitions)

Week 8 (2009-12-17):

VL: Configurable program analysis (reach algorithm, CPA algorithm, merge and stop operators)
Reading: Configurable Software Verification

Week 9 (2010-01-07):

VL: Predicate abstraction, boolean abstraction and cartesian abstraction
Reading: Blast Talk, Blast Article

Week 10 (2010-01-14):

VL: ART-based model checking, predicate refinement, interpolation

Week 11 (2010-01-21):

VL: Precision adjustment in CPA-based analyses, couterexample-guided abstraction refinement (CEGAR)

Week 12 (2010-01-28):

VL: Refinement procedure for predicate abstraction, graph models for software structure analysis, relational programming, pattern analysis

Week 13 (2010-02-04):

VL: Visual software clustering
Reading: Noack Article, CCVisu

Week 14 (2010-02-11):

VL: Project Presentations, recap and structure of the lecture

Authors: Dirk Beyer