Seminar Formal Verification

Semester:

SS 2013

Modul:

CS3702,

CS5840,

CS5480,

CS5015,

CS5191

Lecturer:

Prof. Dr. Martin Leucker

Assistants:

Normann Decker , Daniel Thoma

In the context of hardware and software systems, formal verification is the act of proving or disproving the correctness of intended algorithms underlying a system with respect to a certain formal specification or property, using formal methods of mathematics. [Wikipedia]

We particularily consider the verification of software systems including their modelling on different levels of abstraction and the specification of properties that are to be verified. Typical approaches are, for example theorem proving, testing, model checking, runtime verification, static analysis, type checking. They rely on formal concepts such as (temporal) logic, automata- and game theory or process algebras. The major goal is an automatic comparisson of the (possibly abstract) modell and a property specification.

SS 2013

Preliminary meeting (Vorbesprechung)
Monday 15:00-16:00 1.108 (Besprechungsraum ISP), Building 64 (not every week)

(2nd) Preliminary meeting (Vorbesprechung)
Friday 13:30-14:30 2.132 (von Neumann), Building 64 (not every week)

click to view Dates.

Topics

The aim of this seminar is to give an overview on a selection of topics within the field of formal verification. Available topics include but are not limited to

Transition systems
- Well-structured transition systems
- Parity games
- Energy games
- Timed automata
Process algebras
- π-calculus
- Calculus of Communicating Systems (CCS)
Code analysis
- Type checking
- Abstract interpretation
- Proof carrying code
Model checking
- Abstraction refinement (CEGAR)
- Bounded model checking and inductive proofs

Mailing list

Important information related to the seminar Formal Verification will be distributed through the mailing list. Participants are strongly encouraged to register with the list. Note that access is only possible from inside the domain uni-luebeck.de.

Mailing list Formal Verification

Organization

Participants obtain a dedicated topic from their supervisor and are expected to

Get acquainted with the individual topic on their own
Write an overview article: approx. 5000 Words, e.g. up to 6 pages IEEE (two-column) format
Hand in the article (in PDF) 2 weeks before the talk
Give a presentation: 30-45 min, additional 15 min are reserved for discussion
Hand in complete presentation material (slides) 1 week before the talk
Attend all of the presentations