Principles of Abstract Interpretation
暫譯: 抽象解釋原則
Cousot, Patrick
- 出版商: Summit Valley Press
- 出版日期: 2021-09-21
- 售價: $3,140
- 貴賓價: 9.5 折 $2,983
- 語言: 英文
- 頁數: 832
- 裝訂: Hardcover - also called cloth, retail trade, or trade
- ISBN: 0262044900
- ISBN-13: 9780262044905
海外代購書籍(需單獨結帳)
相關主題
商品描述
Introduction to abstract interpretation, with examples of applications to the semantics, specification, verification, and static analysis of computer programs. Formal methods are mathematically rigorous techniques for the specification, development, manipulation, and verification of safe, robust, and secure software and hardware systems. Abstract interpretation is a unifying theory of formal methods that proposes a general methodology for proving the correctness of computing systems, based on their semantics. The concepts of abstract interpretation underlie such software tools as compilers, type systems, and security protocol analyzers. This book provides an introduction to the theory and practice of abstract interpretation, offering examples of applications to semantics, specification, verification, and static analysis of programming languages with emphasis on calculational design. The book covers all necessary computer science and mathematical concepts--including most of the logic, order, linear, fixpoint, and discrete mathematics frequently used in computer science--in separate chapters before they are used in the text. Each chapter offers exercises and selected solutions. Chapter topics include syntax, parsing, trace semantics, properties and their abstraction, fixpoints and their abstractions, reachability semantics, abstract domain and abstract interpreter, specification and verification, effective fixpoint approximation, relational static analysis, and symbolic static analysis. The main applications covered include program semantics, program specification and verification, program dynamic and static analysis of numerical properties and of such symbolic properties as dataflow analysis, software model checking, pointer analysis, dependency, and typing (both for forward and backward analysis), and their combinations. Principles of Abstract Interpretation is suitable for classroom use at the graduate level and as a reference for researchers and practitioners.
商品描述(中文翻譯)
抽象解釋的介紹,並舉例應用於計算機程序的語義、規範、驗證和靜態分析。
正式方法是數學上嚴謹的技術,用於安全、穩健和安全的軟體及硬體系統的規範、開發、操作和驗證。抽象解釋是一種統一的正式方法理論,提出了一種基於計算系統語義的正確性證明的一般方法論。抽象解釋的概念是許多軟體工具的基礎,例如編譯器、類型系統和安全協議分析器。本書提供了抽象解釋的理論和實踐的介紹,並舉例應用於編程語言的語義、規範、驗證和靜態分析,特別強調計算設計。
本書在使用文本之前,分章涵蓋所有必要的計算機科學和數學概念,包括計算機科學中經常使用的大多數邏輯、序、線性、固定點和離散數學。每章提供練習題和選擇解答。章節主題包括語法、解析、追蹤語義、屬性及其抽象、固定點及其抽象、可達性語義、抽象域和抽象解釋器、規範和驗證、有效的固定點近似、關係靜態分析和符號靜態分析。主要應用包括程序語義、程序規範和驗證、程序的動態和靜態分析,包括數值屬性和數據流分析、軟體模型檢查、指標分析、依賴性和類型(包括前向和後向分析)及其組合。抽象解釋原則適合用於研究生階段的課堂教學,並作為研究人員和實務工作者的參考。
作者簡介
Patrick Cousot is Julius Silver, Roslyn S. Silver, and Enid Silver Winslow Professor in the Computer Science Department at New York University.
作者簡介(中文翻譯)
帕特里克·庫索特(Patrick Cousot)是紐約大學計算機科學系的朱利斯·西爾弗(Julius Silver)、羅斯林·S·西爾弗(Roslyn S. Silver)和伊尼德·西爾弗·溫斯洛(Enid Silver Winslow)教授。