停止性自動検証ツールにおける SAT Solver の使い方 Export

@article{citeulike:4024790, abstract = {項書換えや関数型言語のプログラムの停止性を自動証明するツールは、この5年 間で証明能力・実行速度ともに飛躍的に改善した。最新のツールでは、複雑怪奇 な方程式を解くことによって停止性の証明を行うが、その実装は意外にもシンプ ルである。その秘訣は、複雑な問題を全て SAT 問題へ帰着させることにある。 このチュートリアルでは、関数型言語などの計算モデルである項書換え系のため の停止性検証ツールの実装方法を紹介する。「停止性ってなに？」「SAT ってな に？」という基礎からはじめ「どうやって停止性問題を SAT 問題に帰着させる か？」「なぜ SAT solver は速いのか」までを詳説する。}, author = {広川}, citeulike-article-id = {4024790}, day = {11}, keywords = {2007, read, sat, trs}, month = {September}, posted-at = {2009-02-09 09:30:43}, priority = {0}, title = {停止性自動検証ツールにおける SAT Solver の使い方}, year = {2007} }

TY - JOUR ID - citeulike:4024790 L3 - citeulike-article-id:4024790 N2 - 項書換えや関数型言語のプログラムの停止性を自動証明するツールは、この5年 間で証明能力・実行速度ともに飛躍的に改善した。最新のツールでは、複雑怪奇 な方程式を解くことによって停止性の証明を行うが、その実装は意外にもシンプ ルである。その秘訣は、複雑な問題を全て SAT 問題へ帰着させることにある。 このチュートリアルでは、関数型言語などの計算モデルである項書換え系のため の停止性検証ツールの実装方法を紹介する。「停止性ってなに？」「SAT ってな に？」という基礎からはじめ「どうやって停止性問題を SAT 問題に帰着させる か？」「なぜ SAT solver は速いのか」までを詳説する。 TI - 停止性自動検証ツールにおける SAT Solver の使い方 KW - 2007 KW - read KW - sat KW - trs AU - 広川 PY - 2007/09/11/ ER -