Seminar Formal Verification

Semester:

WS 2013/2014

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.

WS 2013/2014

Preliminary meeting (Vorbesprechung)
Tuesday 14:30-16:00 AM S 1 (Seminarraum 1, Auditorium Maximum) (not every week)

click to view Dates.

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
Model checking
- Abstraction refinement (CEGAR)
- Bounded model checking and inductive proofs
Runtime Verification
Diagnosis
Testing
- Conformance Testing
- Model-based Testing

Specific Topics

Material for the following specific topics is available below.

Model-based diagnosis
Type systems 1 - Concepts in modern programming languages
Type systems 2 - Towards behavioural verification
Binary decission diagrams

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

Templates

The following templates may be used for the seminar.

Article templates commonly used for publications in computer science
- IEEE Author Kit (two-column, download below)
- LIPIcs author template (single column, CC license)
ISP LaTeX Beamer template

Material