Handbook of Model Checking
暫譯: 模型檢查手冊

Clarke, Edmund M., Henzinger, Thomas A., Veith, Helmut

Handbook of Model Checking
  • 出版商: Springer
  • 出版日期: 2020-11-14
  • 售價: $5,810
  • 貴賓價: 9.5 折 $5,520
  • 語言: 英文
  • 頁數: 1210
  • 裝訂: Quality Paper - also called trade paper
  • ISBN: 3030132331
  • ISBN-13: 9783030132330
  • 其他版本: 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 結構和時間邏輯的範疇。

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

作者簡介

Edmund M. Clarke is Professor Emeritus in the Dept. of Computer Science at Carnegie Mellon University, where he was formerly the FORE Systems Professor. He received his Ph.D. in Computer Science from Cornell University in 1976. With E. Allen Emerson and Joseph Sifakis he received the ACM Turing Award in 2007 for his work on the development of model checking. He cofounded the Computer Aided Verification (CAV) conference, and the journal Formal Methods in Systems Design. Among many honors, he was elected to the US National Academy of Engineering and to the American Academy of Arts and Sciences. His research interests include software and hardware verification and automatic theorem proving.

Thomas A. Henzinger is President of IST Austria (Institute of Science and Technology Austria). He holds a Ph.D. in Computer Science from Stanford University (1991). He has held assistant, associate, and full professorships in Cornell University (1992-95), the University of California, Berkeley (1996-2004), and EPFL in Lausanne, Switzerland (2004-09); he was also Director at the Max Planck Institute for Computer Science in Saarbrücken, Germany (1999). His research focuses on modern systems theory, especially models, algorithms, and tools for the design and verification of reliable software, hardware, and embedded systems. He is an ISI highly cited researcher, a member of Academia Europaea, the German Academy of Sciences (Leopoldina), and the Austrian Academy of Sciences, and a Fellow of the AAAS, ACM, and IEEE. He has received the Milner Award of the Royal Society, the Wittgenstein Award of the Austrian Science Fund, and an ERC Advanced Investigator Grant.

Helmut Veith was a professor in the Faculty of Informatics of Technische Universität Wien, and an adjunct professor at Carnegie Mellon University. He received his PhD (sub auspiciis praesidentis) in Computer Science from TU Wien. He previously held professor positions at TU München and TU Darmstadt. In his research, he applied formal and logical methods to problems in software technology and engineering, focusing on model checking, software verification and testing, embedded software, and computer security. Prof. Veith passed away in 2016 during the final editing on the Handbook.

Roderick Bloem received his PhD from the University of Colorado at Boulder (2001) for work on formal verification using linear temporal logic. He moved to Technische Universität Graz in 2002, where he has been a full professor since 2008. His research interests are in formal methods for the design and verification of digital systems, including hardware, software, and combinations such as embedded systems. He studies applications of game theory to the automatic synthesis of systems from their specifications, connections between temporal logics and omega-automata, model checking, and automatic fault localization and repair.

 

作者簡介(中文翻譯)

艾德蒙·M·克拉克（Edmund M. Clarke）是卡內基梅隆大學計算機科學系的名譽教授，曾擔任FORE Systems教授。他於1976年在康奈爾大學獲得計算機科學博士學位。與E. Allen Emerson和Joseph Sifakis共同獲得2007年ACM圖靈獎，以表彰他在模型檢查發展方面的工作。他共同創辦了計算機輔助驗證（CAV）會議和期刊《系統設計中的形式方法》。他獲得了許多榮譽，包括當選美國國家工程院和美國藝術與科學學院的院士。他的研究興趣包括軟體和硬體驗證以及自動定理證明。

托馬斯·A·亨辛格（Thomas A. Henzinger）是奧地利科學與技術研究所（IST Austria）的院長。他於1991年在史丹佛大學獲得計算機科學博士學位。他曾在康奈爾大學（1992-95）、加州大學伯克利分校（1996-2004）和瑞士洛桑的EPFL（2004-09）擔任助理教授、副教授和正教授；他還曾擔任德國薩爾布呂肯的馬克斯·普朗克計算機科學研究所所長（1999）。他的研究專注於現代系統理論，特別是可靠軟體、硬體和嵌入式系統的設計與驗證的模型、演算法和工具。他是ISI高被引研究者，歐洲學院成員，德國科學院（Leopoldina）和奧地利科學院的成員，以及美國科學促進會（AAAS）、ACM和IEEE的會士。他曾獲得英國皇家學會的米爾納獎、奧地利科學基金的維特根斯坦獎和歐洲研究委員會的高級研究者獎。

赫爾穆特·維特（Helmut Veith）曾是維也納科技大學（Technische Universität Wien）資訊學院的教授，並擔任卡內基梅隆大學的兼任教授。他在維也納科技大學獲得計算機科學博士學位（sub auspiciis praesidentis）。他曾在慕尼黑科技大學和達姆施塔特科技大學擔任教授。在他的研究中，他將形式和邏輯方法應用於軟體技術和工程中的問題，專注於模型檢查、軟體驗證和測試、嵌入式軟體以及計算機安全。維特教授於2016年在《手冊》的最終編輯過程中去世。

羅德里克·布魯姆（Roderick Bloem）於2001年在科羅拉多大學博爾德分校獲得博士學位，研究主題為使用線性時間邏輯的形式驗證。他於2002年轉至格拉茨科技大學，並自2008年起擔任正教授。他的研究興趣在於數位系統的設計與驗證的形式方法，包括硬體、軟體及嵌入式系統等組合。他研究博弈論在自動合成系統中的應用、時間邏輯與ω-自動機之間的聯繫、模型檢查以及自動故障定位和修復。

類似商品