Formal Logical Methods for System Security and Correctness

Front Cover
Orna Grumberg, Tobias Nipkow, Christian Pfaller
IOS Press, 2008 - Business & Economics - 319 pages
Offers information in the field of proof technology in connection with secure and correct software. This title shows that methods of correct-by-construction program and process synthesis allow a high level programming method more amenable to security and reliability analysis and guarantees.
 

What people are saying - Write a review

We haven't found any reviews in the usual places.

Contents

Compilation of Certificates
1
Formal Foundations of Computer Security
29
Building a Software Model Checker
53
Automatic Refinement and Vacuity Detection
89
Automated and Interactive Theorem Proving
111
Correctness of EffectBased Program Transformations
149
Abstract and Concrete Models for Recursion
175
Secrecy Analysis in Protocol Composition Logic
199
The Engineering Challenges of Trustworthy Computing
233
Reflecting Quantifier Elimination for Linear Arithmetic
245
Content in Proofs of List Reversal
267
Proof Theory Large Functions and Combinatorics
287
Author Index
319
Copyright

Other editions - View all

Common terms and phrases