@inproceedings{oai:ipsj.ixsq.nii.ac.jp:00241050, author = {河野, 真治}, book = {コンピュータシステム・シンポジウム論文集}, month = {Nov}, note = {GearsOS は軽量継続を用いて,さまざまなプログラムを記述する.この時の記述言語として C base の CbC (Continuation based C) と,Agda baseのgearsAgda がある.CbC で記述されたプログラムは Model 検査することができるが,それには計算量がかかる.geasAgda で記述されたプログラムは,Invariant をメタレベルに導入することでさまざまな検証をおこなうことができる この論文では gearsAgda を使ったモデル検査について述べる.Buchi automaton と時相論理式の記述を Agda で記述し,それを Invariant として gearsAgda の code にいれることで検証をおこなう.gearsAgdaのfair scheduler で実行せずに,検証を行うことが可能になる したがって,正確にはモデル検査的な手法を用いたプログラムの検証になる}, pages = {17--20}, publisher = {情報処理学会}, title = {GearsOSとgearsAgda上のモデル検査について}, volume = {2024}, year = {2024} }