You are here

Home › Teaching › WS 2014/2015 ›

Seminar Formal Verification

Semester: 
WS 2014/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) modell and a property specification.

WS 2014/2015
Preliminary meeting (Vorbesprechung)
Friday 13:00-13:40 1.108 (Besprechungsraum ISP), Building 64 (not every week)

Abstract and outline
Wednesday 23:59-23:59 submission deadline (not every week)

Report final version
Monday 23:59-23:59 submission deadline (not every week)

Presentation material (slides) final version
Monday 23:59-23:59 submission deadline (not every week)

Preliminary meeting (Vorbesprechung)
Friday July 25, 2014 13:00-13:40 (1.108 (Besprechungsraum ISP), Building 64)

Abstract and outline
Wednesday October 8, 2014 23:59-23:59 (submission deadline)

Report final version
Monday December 1, 2014 23:59-23:59 (submission deadline)

Presentation material (slides) final version
Monday December 8, 2014 23:59-23:59 (submission deadline)

click to view Dates.

Schedule and Selected Topics

This semester the following topics were selected and are going to be presented according to the following schedule.

Monday, 15 December
Building 64, Room 2.021 (Seminarraum Inst. f. Theoretische Informatik)

  • 09.00 - 11.00 Session 1: Basic approaches to formal semantics of programs
    • Operational semantics
    • Axiomatic semantics
  • 11.15 - 13.15 Session 2: Functional concepts in programming
    • Denotational semantics
    • Typed λ-calculus

Tuesday, 16 December
Building 64, Room 3.004 (Seminarraum Inst. f. Mathematik)

  • 14.00 - 16.00 Session 3: Program verification
    • Abstract interpretation
    • CTL Model Checking
  • 16.15 - 18.15 Session 4: Abstract models and analysis
    • Well-structured transition systems
    • Timed Automata

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

  • Transition systems
    • Well-structured transition systems
    • Parity games
    • Energy games
    • Timed automata
  • Process algebras
    • Calculus of Communicating Systems (CCS)
  • Code analysis
    • Type checking
    • Shape Analysis
  • Model checking
    • Abstraction refinement (CEGAR)
    • Bounded model checking and inductive proofs
  • Runtime Verification
  • Diagnosis
  • Testing
    • Conformance Testing
    • Model-based Testing

Please, feel free to propose further 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 2014-07-25
Package icon ISP LaTeX Beamer template