You are here

Home › Teaching › SS 2015 ›

Seminar Formal Verification

Semester: 
SS 2015
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 and 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) model and a property specification.

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

Preliminary meeting (Vorbesprechung)
Tuesday April 7, 2015 15:00-16:00 (1.108 (Besprechungsraum ISP), Building 64)

click to view Dates.

Important Dates

  • Abstract and Outline: 18 May
  • Report (final version):  15 June, 23.59h CEST
  • Presentation material (final version):  22 June, 23.59h CEST
  • Seminar: 1st July

Subjects

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

  • Formal Models and Semantics
    • Transition systems
    • Automata and games
    • Process algebra
    • Logic
    • Models of computation
  • Program analysis and verification
    • Type systems
    • Shape  and data flow analysis
    • Model checking
    • Runtime verification
  • Diagnosis
  • Testing

Please, feel free to propose specific topics that fit the scope of the semniar.

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.

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

Templates

The following templates can be used for the seminar.

 

Material
PDF icon Slides preliminary meeting 2015-04-07