大学院
過去（2019年度）の授業の情報です
学内のオンライン授業の情報漏洩防止のため，URLやアカウント、教室の記載は削除しております。
最終更新日：2024年4月22日
授業計画や教室は変更となる可能性があるため、必ずUTASで最新の情報を確認して下さい。
UTASにアクセスできない方は、担当教員または部局教務へお問い合わせ下さい。
最終更新日：2024年4月22日
授業計画や教室は変更となる可能性があるため、必ずUTASで最新の情報を確認して下さい。
UTASにアクセスできない方は、担当教員または部局教務へお問い合わせ下さい。
コンピュータ科学特別講義VII
Fundamentals of Stateless Model Checking for Concurrent Programs
Model checking of concurrent programs with shared memory under SC or relaxed memory semantics has been an active area of research. One of the central problems in model checking concurrent programs is the state-space explosion due to the possibility of numerous number of interleavings of program events. Partial order reduction (POR) techniques (proposed in early 90s) offer a powerful solution to address the afore-mentioned schedulestate explosion. In this course, I will begin by first explaining the central notions of the POR theory
followed by detailed discussions on some of the recent advances in the area.
followed by detailed discussions on some of the recent advances in the area.
時間割／共通科目コード
コース名
教員
学期
時限
4810-1211
GIF-CS6079L1
コンピュータ科学特別講義VII
須田 礼仁
集中
マイリストに追加
マイリストから削除
講義使用言語
英語
単位
1
実務経験のある教員による授業科目
NO
他学部履修
不可
開講所属
情報理工学系研究科
授業計画
Class 1: 6/24(Mon) 14:55-16:40
Fundamentals of partial order reduction
Class 2: 6/25(Tue) 16:50-18:35
Dynamic Partial Order Reduction (DPOR)
Class 3: 7/1(Mon) 14:55-16:40
Optimal DPOR
Class 4: 7/2(Tue) 16:50-18:35
Variants of DPOR
Class 5: 7/8(Mon) 14:55-16:40
Exercises on DPOR
Class 6: 7/9(Tue) 16:50-18:35
Understanding relaxed memory models and improvising DPOR for TSO, PSO, SPARC and RMM
Class 7: 7/15(Mon) 14:55-16:40
Recent research topics
Details:
1) Fundamentals of partial order reduction -- model checking concurrent software using representatives. I
will cover concepts relating to static computation of persistent sets, ample sets, stubborn sets, sleep
sets and establishing their correctness (CAV'90, CAV'93, FMSD'92 )[~ 2hrs]
2) Dynamic Partial Order Reduction (DPOR) and making it optimal (POPL'05, JACM 17, POPL'14) [~2 hrs]
3) Variants of DPOR -- making the algorithm stateful, distributed, property-driven and exploiting
transition symmetries (SPIN'07, SPIN'08) [~3 hrs]
4) Understanding relaxed memory models and improvising DPOR for TSO, PSO, SPARC and RMM (PLDI'15, CAV 16, TACAS'16,17) [~3 hrs]
5) Optimal Symbolic POR (CAV'09), Combining partial order semantics with DPOR (CONCUR'15), DPOR for timed systems (CAV'14) [~1 hr]
授業の方法
プロジェクター・黒板を併用した講義の形式で行います。
The lecture is given in English using a projector and a blackboard.
成績評価方法
授業出席とレポート
class attendance and a report
教科書
先端研究について議論するため、本講義には教科書を使いません。
As this is a class on recent research topics, there will be no textbook for this class.
参考書
1. Yang, Yu, et al. "Efficient stateful dynamic partial order reduction." International SPIN Workshop on Model Checking of Software. Springer, Berlin, Heidelberg, 2008.
2. Abdulla, Parosh, et al. "Optimal dynamic partial order reduction." ACM SIGPLAN Notices. Vol. 49. No. 1. ACM, 2014.
履修上の注意
本講義には、論理や代数など数学的な議論が多いため、オートマトン理論をはじめシステム数理モデルの知識を前提とする。
The course is fairly mathematical (algebraic and logical) and hence students who have a strong inclination towards mathematical modelling of systems (including automata theoretic) will probably enjoy it.
その他
講師
Subodh Sharma助教授 (インド工科大学、デリー校)
Instructor
Assistant Prof. Subodh Sharma (Indian Institute of Technology, Delhi)
