Vai al contenuto principale della pagina
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 | |
Soggetto genere / forma: | Electronic books. |
Altri autori: |
SchwichtenbergHelmut <1942->
![]() ![]() |
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.: | 9910450834903321 |
Lo trovi qui: | Univ. Federico II |
Opac: | Controlla la disponibilità qui |