Handbook of Model Checking

買這商品的人也買了...

商品描述

Model checking is a computer-assisted method for the analysis of dynamical systems that can be modeled by state-transition systems. Drawing from research traditions in mathematical logic, programming languages, hardware design, and theoretical computer science, model checking is now widely used for the verification of hardware and software in industry.

 

The editors and authors of this handbook are among the world's leading researchers in this domain, and the 32 contributed chapters present a thorough view of the origin, theory, and application of model checking. In particular, the editors classify the advances in this domain and the chapters of the handbook in terms of two recurrent themes that have driven much of the research agenda: the algorithmic challenge, that is, designing model-checking algorithms that scale to real-life problems; and the modeling challenge, that is, extending the formalism beyond Kripke structures and temporal logic.

The book will be valuable for researchers and graduate students engaged with the development of formal methods and verification tools.

 

商品描述(中文翻譯)

模型檢查是一種計算機輔助的方法,用於分析可以通過狀態轉換系統建模的動態系統。借鑒數學邏輯、編程語言、硬件設計和理論計算機科學的研究傳統,模型檢查現在被廣泛應用於工業界的硬件和軟件驗證。

本手冊的編輯和作者是這一領域世界領先的研究人員,32個貢獻章節全面介紹了模型檢查的起源、理論和應用。特別是,編輯根據兩個經常出現的主題將這一領域的進展和手冊的章節進行了分類:算法挑戰,即設計能夠應對實際問題的模型檢查算法;建模挑戰,即將形式化方法擴展到Kripke結構和時間邏輯之外。

本書對於從事形式化方法和驗證工具開發的研究人員和研究生非常有價值。