| Descript |
1 online resource (456 pages) |
|
text txt rdacontent |
|
computer c rdamedia |
|
online resource cr rdacarrier |
| Note |
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 |
|
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 |
|
Description based on publisher supplied metadata and other sources |
|
Electronic reproduction. Ann Arbor, Michigan : ProQuest Ebook Central, 2020. Available via World Wide Web. Access may be limited to ProQuest Ebook Central affiliated libraries |
| Link |
Print version: Schwichtenberg, H. Proof Technology and Computation
Amsterdam : IOS Press,c2006 9781586036256
|
| Subject |
Automatic theorem proving -- Congresses.;Computer programming -- Congresses.;Computer software -- Development -- Congresses
|
|
Electronic books
|
| Alt Author |
Spies, K
|
|
NATO Advanced Study Institute on Proof Technology and Computation,
|
|
