Proof technology and computation [[electronic resource] /] / edited by Helmut Schwichtenberg and Katharina Spies
(Visualizza in formato marc)
(Visualizza in BIBFRAME)
| Titolo: |
Proof technology and computation [[electronic resource] /] / edited by Helmut Schwichtenberg and Katharina Spies
|
| Pubblicazione: | Amsterdam ; ; Washington, DC, : IOS Press, c2006 |
| Descrizione fisica: | 1 online resource (456 p.) |
| Disciplina: | 511.3 |
| Soggetto topico: | Automatic theorem proving |
| Computer programming | |
| Computer software - Development | |
| Altri autori: |
SchwichtenbergHelmut <1942->
SpiesKatharina
|
| Note generali: | "Proceedings of the NATO Advanced Study Institute on Proof Technology and Computation, Marktoberdorf, Germany, 29 July-10 August 2003"--T.p. verso. |
| "Published in cooperation with NATO Public Diplomacy Division." | |
| Nota di bibliografia: | Includes bibliographical references and index. |
| Nota di contenuto: | 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 |
| Sommario/riassunto: | 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. |
| Titolo autorizzato: | Proof technology and computation |
| ISBN: | 661054767X |
| 1-280-54767-7 | |
| 9786610547678 | |
| 1-4237-9755-8 | |
| 1-60750-180-5 | |
| 600-00-0528-8 | |
| 1-60129-484-0 | |
| Formato: | Materiale a stampa  |
| Livello bibliografico | Monografia |
| Lingua di pubblicazione: | Inglese |
| Record Nr.: | 9910784245903321 |
| Lo trovi qui: | Univ. Federico II |
| Opac: | Controlla la disponibilità qui |
Serie:
NATO science series. : Series III, . -Computer and systems sciences ; ; v. 200.