Proof Technology and Computation
Author: Helmut Schwichtenberg, Katharina Spies
Format: Unknown Binding
Publisher: Not Avail
Release Date: May 28, 2014
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.