| Document Type
|
:
|
BL
|
| Record Number
|
:
|
1008559
|
| Doc. No
|
:
|
b762929
|
| Main Entry
|
:
|
NATO Advanced Study Institute on Proof Technology and Computation(2003 :, Marktoberdorf, Germany)
|
| Title & Author
|
:
|
Proof technology and computation /\ edited by Helmut Schwichtenberg and Katharina Spies.
|
| Publication Statement
|
:
|
Amsterdam ;Washington, DC :: IOS Press,, ©2006.
|
| Series Statement
|
:
|
NATO science series. Series III, Computer and systems sciences,; v. 200
|
| Page. NO
|
:
|
1 online resource
|
| ISBN
|
:
|
1423797558
|
|
|
:
|
: 1601294840
|
|
|
:
|
: 1607501805
|
|
|
:
|
: 9781423797555
|
|
|
:
|
: 9781601294845
|
|
|
:
|
: 9781607501800
|
|
|
:
|
1586036254
|
|
|
:
|
9781586036256
|
| Notes
|
:
|
"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."
|
| Bibliographies/Indexes
|
:
|
Includes bibliographical references and index.
|
| Contents
|
:
|
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.
|
| Abstract
|
:
|
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.
|
| Subject
|
:
|
Automatic theorem proving, Congresses.
|
| Subject
|
:
|
Computer programming, Congresses.
|
| Subject
|
:
|
Computer software-- Development, Congresses.
|
| Subject
|
:
|
Automatic theorem proving.
|
| Subject
|
:
|
Computer programming.
|
| Subject
|
:
|
Computer software-- Development.
|
| Subject
|
:
|
COMPUTERS-- Expert Systems.
|
| Dewey Classification
|
:
|
006.3/33
|
| LC Classification
|
:
|
QA76.9.A96N38 2003eb
|
| Added Entry
|
:
|
Schwichtenberg, Helmut,1942-
|
|
|
:
|
Spies, Katharina.
|