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!
Aikataulu
Materiaalit
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...
Kuvaus
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