Muutke küpsiste eelistusi

Software Safety and Security: Tools for Analysis and Verification [Kõva köide]

Edited by , Edited by
Teised raamatud teemal:
Teised raamatud teemal:
Recent decades have seen major advances in methods and tools for checking the safety and security of software systems. Automatic tools can now detect security flaws not only in programs of the order of a million lines of code, but also in high-level protocol descriptions. There has also been something of a breakthrough in the area of operating system verification. This book presents the lectures from the NATO Advanced Study Institute on Tools for Analysis and Verification of Software Safety and Security; a summer school held at Bayrischzell, Germany, in 2011. This Advanced Study Institute was divided into three integrated modules: Foundations of Safety and Security, Applications of Safety Analysis and Security Analysis. Subjects covered include mechanized game-based proofs of security protocols, formal security proofs, model checking, using and building an automatic program verifier and a hands-on introduction to interactive proofs. Bringing together many leading international experts in the field, this NATO Advanced Study Institute once more proved invaluable in facilitating the connections which will influence the quality of future research and the potential to transfer research into practice. This book will be of interest to all those whose work depends on the safety and security of software systems.
Preface v
Mechanizing Game-Based Proofs of Security Protocols
1(25)
Bruno Blanchet
Formal Security Proofs
26(38)
Hubert Comon-Lundh
Stephanie Delaune
Model Checking: From BDDs to Interpolation
64(21)
Orna Grumberg
Interactive Proof: Applications to Semantics
85(41)
Gerwin Klein
Advances in Probabilistic Model Checking
126(26)
Marta Kwiatkowska
David Parker
Getting Started with Dafny: A Guide
152(30)
Jason Koenig
K. Rustan
M. Leino
Lecture Notes on Software Model Checking
182(23)
Rupak Majumdar
Boolean Satisfiability Solvers: Techniques and Extensions
205(49)
Georg Weissenbacher
Sharad Malik
Interactive Proof: Introduction to Isabelle/HOL
254(32)
Tobias Nipkow
A Primer on Separation Logic (and Automatic Program Verification and Analysis)
286(33)
Peter W. O'Hearn
A Perspective on Information-Flow Control
319(29)
Daniel Hedin
Andrei Sabelfeld
Precise Program Analysis through Strategy Iteration and Optimization
348(37)
Thomas Martin Gawlitza
Helmut Seidl
Subject Index 385(2)
Author Index 387