Slides from the first meeting on September 3:
Introduction to model checking:
ADVICE ON WRITING AND PRESENTATION IN COMPUTER SCIENCE
Recommended reading is Zobel's book "Writing in Computer Science", for a pdf version see here:
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.
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
9 IC3/PDR / Korhonen
-Aaron R. Bradley: SAT-Based Model Checking without Unrolling. VMCAI 2011: 70-87
-Niklas Eén, Alan Mishchenko, Robert K. Brayton: Efficient implementation of property directed reachability. FMCAD 2011: 125-134
-Aaron R. Bradley: Understanding IC3. SAT 2012: 1-14
10. K-induction / Lehtonen
-Mary Sheeran, Satnam Singh, Gunnar Stålmarck: Checking Safety Properties Using Induction and a SAT-Solver. FMCAD 2000: 108-125
-Niklas Eén, Niklas Sörensson: Temporal induction by incremental SAT solving. Electr. Notes Theor. Comput. Sci. 89(4): 543-560 (2003)
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
+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)
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
-Hernán Ponce de León, Florian Furbach, Keijo Heljanko, Roland Meyer: BMC with Memory Models as Modules. FMCAD 2018: 1-9
-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
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.
-Xiang Gan, Jori Dubrovin, Keijo Heljanko. A symbolic model checking approach to verifying satellite onboard software. Science of Computer Programming, 82:44-55 (2014).,
-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).
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
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.
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