Klaus Schneider Book order

This collection explores the utility of formal methods in software development and certification, highlighting various techniques and applications. It covers topics such as formal techniques in software engineering, ensuring correct software and safe systems, and the use of separation logic in small-step cminor. The annotation discusses formalizing Java’s data race-free guarantee, finding lexicographic orders for termination proofs in Isabelle/HOL, and extracting purely functional contents from logical inductive types. It also addresses modular formalization of finite group theory and verifying nonlinear real formulas via sums of squares. Expectation properties for discrete random variables in HOL are examined, along with a formally verified prover for description logic. The work includes proof pearls on termination analysis, usability improvements in HOL through automation tactics, and verified decision procedures for context-free grammars. The application of XCAP for certifying realistic systems code is highlighted, alongside discussions on source-level proof reconstruction for interactive theorem proving. The power of higher-order encodings in logical frameworks is emphasized, as well as operational reasoning for concurrent Caml programs. The collection also presents a monad-based modeling and verification toolbox for security protocols, primality proving with elliptic curves, and systems of classical higher-order logic wi

This book is a solid foundation of the most important formalisms used for specification and verification of reactive systems. In particular, the text presents all important results on m-calculus, w-automata, and temporal logics, shows the relationships between these formalisms and describes state-of-the-art verification procedures for them. It also discusses advantages and disadvantages of these formalisms, and shows up their strengths and weaknesses. Most results are given with detailed proofs, so that the presentation is almost self-contained. Includes all definitions without relying on other material Proves all theorems in detail Presents detailed algorithms in pseudo-code for verification as well as translations to other formalisms