Kaisa_2012_3_photo by Veikko Somerpuro

We in our everyday lives rely heavily on various types of computing infrastructures to perform as expected. These vary from hardware devices such as microprocessors to software device drivers used in our personal computers and smartphones. In addition we have safety critical systems such as embedded systems controlling modern cars, medical equipment, and airplanes. The correct functioning of all of these systems is critical both on the level of individual persons and the society. Model checking is a exciting area of computer science which, combined with automated reasoning (with direct connections to logic), aims to provide automated tools for finding bugs and for ensuring the correctness of hardware and software designs alike.

In particular, model checking provides algorithmic means of determining whether an abstract model representing a hardware or software design is guaranteed to satisfy a formal specification. The approach can also provide a counterexample execution in the case that the specification is not satisfied, helping the designer to pinpoint the errors in the design. Today, model checking is a key tool in the hardware and software industries for guaranteeing the correctness of different kinds of critical hardware and software systems, such as VLSI circuits, communication protocols, software device drivers, real-time embedded systems, and security algorithms.

The aim of this MSc level seminar is to provide an overview of fundamental concepts and some of the state-of-the-art techniques for model checking from a modern computer science perspective.

The seminar is intended for MSc students with interest in discrete algorithms, computation and in particular the use of formal logic and automated reasoning to verify the correctness of hardware and software. Students majoring in mathematics, in particular mathematical logic, are also encouraged to attend. PhD students are also welcome.
A certain level of algorithmic and mathematical maturity is expected from the participants. Please consult some of the research articles listed under "MATERIAL" for an impression of the seminar contents. Attendance is limited to at most 12 students due to the organization of the seminar.

The course work consists of

-giving a 40 min presentation,
-writing a 10-15 page scientific report (plus references),
-acting as an opponent during on presentation, and
-peer-review of two student reports.

Hands-on project work can also be done as an alternative to peer-review. Please let the seminar organizers know if you are interested in a hands-on project!

Enrol

Timetable

SEPTEMBER 3: Introduction and choosing topics
(for the practical arrangements and introductory slides, see under "MATERIAL")

DEADLINES:

-One week before your presentation (for presenters):
Preliminary version of report and slides (by email to the instructors)

-December 8: peer-review version of report
-December 16: peer-reviews
-December 20: final version of report

PRESENTATION SCHEDULE:

See under "MATERIAL" for the articles.

OCTOBER 29 (responsible teacher: Matti)
-Topic 1: Introduction to Model Checking / Kemppainen
Opponent: Salonen
-Topic 2: Temporal Logic and Fair Discrete Systems / Sandström
Opponent: Mäki

NOVEMBER 5 (responsible teacher: Keijo)
-Topic 3: Partial Order Reduction / Koivisto
Opponent: Lehtonen
-Topic 6: Combining Model Checking and Testing / **CANCELLED**

NOVEMBER 12 (responsible teacher: Matti)
-Topic 5: Propositional SAT Solving / Salonen
Opponent: Mohamed
-Topic 11: SAT-based bounded model checking / Mäki
Opponent: Savela

NOVEMBER 19 (responsible teacher: Keijo)
-Topic 10: K-induction / Lehtonen
Opponent: Matti&Keijo
-Topic 9: IC3/PDR / Korhonen
Opponent: Lång

NOVEMBER 26 (responsible teacher: Matti)
-Topic 7: Symbolic Trajectory Evaluation / Mohamed
Opponents: Korhonen, Kemppainen
-Topic 8: Model Checking Probabilistic Systems / **CANCELLED**

DECEMBER 3 (responsible teacher: Keijo)
-Topic 13: Use of model checking in industry / Lång
Opponent: Koivisto, Sandström

DateTimeLocation
Tue 3.9.2019
14:00 - 16:00
Tue 29.10.2019
14:00 - 16:00
Tue 5.11.2019
14:00 - 16:00
Tue 12.11.2019
14:00 - 16:00
Tue 19.11.2019
14:00 - 16:00
Tue 26.11.2019
14:00 - 16:00
Tue 3.12.2019
14:00 - 16:00
Tue 10.12.2019
14:00 - 16:00

Other teaching

Material

Slides from the first meeting on September 3:
Practical arrangements:
https://www.cs.helsinki.fi/u/mjarvisa/seminar19mc/practical.pdf

Introduction to model checking:
https://www.cs.helsinki.fi/u/mjarvisa/seminar19mc/model-checking-intro.pdf

ADVICE ON WRITING AND PRESENTATION IN COMPUTER SCIENCE

Recommended reading is Zobel's book "Writing in Computer Science", for a pdf version see here:
https://pingpong.chalmers.se/public/pp/public_courses/course08583/publis...

SEMINAR TOPICS

Each student will choose one topic for the seminar work (oral presentation, seminar report) from the following list. You may also propose a topic within the topic of the seminar outside this list based on your own interested; in case you want to propose your own topic, please contact the teachers.

TOPICS:

Chapters from Handbook of Model Checking
UH-restricted e-book: http://login.libproxy.helsinki.fi/login?url=http://search.ebscohost.com/...

1. Chapter 1 (p. 1-26): Introduction to Model Checking / Kemppainen
2. Chapter 2 (p. 27-73): Temporal Logic and Fair Discrete Systems / Sandström
3. Chapter 6 (p. 173-190): Partial Order Reduction / Koivisto
4. Chapter 8 (p. 219-245): BDD-Based Symbolic Model Checking
5. Chapter 9 (p. 247-275): Propositional SAT Solving / Salonen
6. Chapter 19 (p. 613-649): Combining Model Checking and Testing / Kärnä
7. Chapter 25 (p. 831-870): Symbolic Trajectory Evaluation / Mohamed
8. Chapter 28 (p.963-999): Model Checking Probabilistic Systems / Savela

Research articles:

9 IC3/PDR / Korhonen

-Aaron R. Bradley: SAT-Based Model Checking without Unrolling. VMCAI 2011: 70-87
https://doi.org/10.1007/978-3-642-18275-4_7

-Niklas Eén, Alan Mishchenko, Robert K. Brayton: Efficient implementation of property directed reachability. FMCAD 2011: 125-134
http://dl.acm.org/citation.cfm?id=2157675

-Aaron R. Bradley: Understanding IC3. SAT 2012: 1-14
https://doi.org/10.1007/978-3-642-31612-8_1

10. K-induction / Lehtonen

-Mary Sheeran, Satnam Singh, Gunnar Stålmarck: Checking Safety Properties Using Induction and a SAT-Solver. FMCAD 2000: 108-125
https://doi.org/10.1007/3-540-40922-X_8

-Niklas Eén, Niklas Sörensson: Temporal induction by incremental SAT solving. Electr. Notes Theor. Comput. Sci. 89(4): 543-560 (2003)
https://doi.org/10.1016/S1571-0661(05)82542-3

11. Bounded model checking / Mäki

-Armin Biere: Bounded Model Checking. Handbook of Satisfiability 2009: 457-481 (ask the teachers for a copy)

Further reading on topic 11:
+Armin Biere, Alessandro Cimatti, Edmund M. Clarke, Yunshan Zhu: Symbolic Model Checking without BDDs.
TACAS 1999: 193-207
https://doi.org/10.1007/3-540-49059-0_14
+Armin Biere, Keijo Heljanko, Tommi A. Junttila, Timo Latvala, Viktor Schuppan: Linear Encodings of Bounded LTL
Model Checking. Logical Methods in Computer Science 2(5) (2006)
https://doi.org/10.2168/LMCS-2(5:5)2006

12. Model Checking for Weak Memory Models:

-Hernán Ponce de León, Florian Furbach, Keijo Heljanko, Roland Meyer: Portability Analysis for Weak Memory Models. PORTHOS: One Tool for all Models. SAS 2017: 299-320
https://doi.org/10.1007/978-3-319-66706-5_15

-Hernán Ponce de León, Florian Furbach, Keijo Heljanko, Roland Meyer: BMC with Memory Models as Modules. FMCAD 2018: 1-9
https://doi.org/10.23919/FMCAD.2018.8603021

-Natalia Gavrilenko, Hernán Ponce de León, Florian Furbach, Keijo Heljanko, Roland Meyer: BMC for Weak Memory Models: Relation Analysis for Compact SMT Encodings. CAV (1) 2019: 355-365
https://doi.org/10.1007/978-3-030-25540-4_19

Own topics:
13. Use of model checking in industry / Lång

-Bruschi D., Di Pasquale A., Ghilardi S., Lanzi A., Pagani E. Formal Verification of ARP (Address Resolution Protocol) Through SMT-Based Model Checking - A Case Study. In: Polikarpova N., Schneider S. (eds) Integrated Formal Methods. IFM 2017. Lecture Notes in Computer Science, vol 10510. Springer 2017.
https://link.springer.com/chapter/10.1007/978-3-319-66845-1_26

-Xiang Gan, Jori Dubrovin, Keijo Heljanko. A symbolic model checking approach to verifying satellite onboard software. Science of Computer Programming, 82:44-55 (2014).,
https://doi.org/10.1016/j.scico.2013.03.005.

-M. Webster et al. Toward Reliable Autonomous Robotic Assistants Through Formal Verification: A Case Study. IEEE Transactions on Human-Machine Systems 46(2):186-196 (2016).
http://ieeexplore.ieee.org/stamp/stamp.jsp?tp=&arnumber=7106471&isnumber...

Description

Master's Programme in Computer Science is responsible for the course.

The course belong to following modules:

  • Discrete Algorithms course package CSM12100
  • Module in Discrete Algorithms CSM22100

The course is available to students from other degree programmes.

Course CSM12101 Design and Analysis of Algorithms, or equivalent knowledge and skills. Basic knowledge of formal logic.

-What other courses are recommended to be taken in addition to this course?

To continue with a Master's thesis in computer science related to the topic of the seminar.

Courses: Automated Logical Reasoning.

-Which other courses support the further development of the competence provided by this
course?

Academic writing courses

An ability to give scientific presentations. An ability to peer-review and give oral and written feedback on written work and on oral presentations. Improved scientific writing skills on discrete algorithms topics in general and in model checking in particular. In-depth theoretical and/or practical understanding of an advanced topic in model checking and verification.

After (or at the same time as) the course CSM12101 Design and Analysis of Algorithms.

Autumn 2019

The seminar is focused on fundamentals and state-of-the-art algorithmic approaches to hardware and software model checking.

Selected scientific articles and handbook chapters on aspects of model checking. Reading materials will be provided in electronic form to the students.

Suggestions on supplemental works will be made available at the time the seminar starts.

Grading is 1..5. Oral presentation, written work, and peer-review work are evaluated with a common grade

The course is primarily available as a 5-ECTS seminar consisting of a seminar presentation, written work, and peer review. Active participation in the seminar meetings is expected.

Keijo Heljanko, Matti Järvisalo