■モデル検査と形式証明 モデル検査と形式証明は形式検証技術の主要な技術である。一般に、型式証明は「安全性証明」と言われているが、具体的に「安全性証明」というものは存在せず、「デッドロックがない」とか「ブレーキを踏むと必ずブレーキランプが点灯…

ペアワイズ法は多くのバグを検出できるが、バグがないことを示すものではない。一般的な方法でバグ検出率が高い方法。こうした技術はシステムが一定の品質基準（網羅基準、または社内の品質基準）を満たすことを示すために用いるのに都合が良い。品質基準を…

VirtualBox において、ゲストOSの解像度の調整をしたい。以下の方法を試すが、「VirtualBoxのメニューから「Devices」→「Install Guest Addsinions」をクリックします。」の時点で、「マウントできません（could not mount media）」とエラーが出てしまう。 …

The following code shows a sample of calling a program in Haskell code. It works with compilation (i.e., >ghc CallSATSolver.hs) but not GHCI. import System.Exit import System.Process import Control.Monadmain :: IO () main = do putStrLn "Ru…

The result of planner in the visual viewSamaneh Soltani, Mohsen Asadi, Dragan Gasevic, Marek Hatala, Ebrahim Bagheri: Automated planning for feature model configuration based on functional and non-functional requirements. SPLC (1) 2012: 56…

Haskell parsec で命題論理（propositional logic）の構文解析器を作ってみた。作ってみた、とは一言っても、つくりかけ。BNF の右辺が２つの時はできるのだけど、それが３つ以上になった時にどうして良いかわからない。以下を参考に作った。以下と違って、…

The main challenge of this study was to model the input space in terms of a set of parameters and values. Once the model was designed,we generated test cases using ACTS, which were then later used to test ACTS

An Integrated Approach for Combining BDDs and SAT Provers, by Rolf Drechsler, Gorschwin Fey, and Sebastian Kinder FACTA UNIVERSITATIS (NIS)ˇSER.: ELEC. ENERG. vol. 20. no. 3, December 2007, 415-436 The two most frequently used methods are …