NATO science series. Series III, Computer and systems sciences,
v. 200
1387-6694 ;
"Proceedings of the NATO Advanced Study Institute on Proof Technology and Computation, Marktoberdorf, Germany, 29 July-10 August 2003"--Title page verso.
"Published in cooperation with NATO Public Diplomacy Division."
Includes bibliographical references and index.
Title page; Preface; Contents; Information-Intensive Proof Technology; Introduction to Proof Theory; The Abstraction-Refinement Framework in Model Checking; Verification: Industrial Applications; Selected Topics on Computability, Complexity, and Termination; Jinja: Towards a Comprehensive Formal Semantics for a Java-like Language; The Formulae-as-Classes Interpretation of Constructive Set Theory; Constructive Analysis with Witnesses; Predicates as Types; Automata- and Logic-Based Systems Design; Recursions and Proofs; Author Index.
0
Software engineers have integrated proof processing into industrial development tools, and these implementations are now getting very efficient. The chapters deal with: The benefits and technical challenges of sharing formal mathematics among interactive theorem provers; proof normalization for various axiomatic theories; abstraction-refinement framework of temporal logic model checking; formal verification in industrial hardware design; readable machine-checked proofs and semantics and more.
IOS Press
978-1-58603-625-6
Proof technology and computation.
9781586036256
Automatic theorem proving, Congresses.
Computer programming, Congresses.
Computer software-- Development, Congresses.
Automatic theorem proving.
Computer programming.
Computer software-- Development.
COMPUTERS-- Expert Systems.
COM-- 025000
006
.
3/33
22
QA76
.
9
.
A96
N38
2003eb
Schwichtenberg, Helmut,1942-
Spies, Katharina.
NATO Advanced Study Institute on Proof Technology and Computation(2003 :, Marktoberdorf, Germany)