LEADER 03347nam  2200697Ia 450 
001 9910453840003321
005 20200520144314.0
010   $a6611733469
010   $a1-281-73346-6
010   $a9786611733469
010   $a1-4356-7788-9
010   $a1-60750-315-8
010   $a600-00-0427-3
010   $a1-4337-1233-4
035   $a(CKB)1000000000542528
035   $a(EBL)346214
035   $a(OCoLC)437213124
035   $a(SSID)ssj0000157228
035   $a(PQKBManifestationID)11149915
035   $a(PQKBTitleCode)TC0000157228
035   $a(PQKBWorkID)10138573
035   $a(PQKB)10322913
035   $a(MiAaPQ)EBC346214
035   $a(Au-PeEL)EBL346214
035   $a(CaPaEBR)ebr10231732
035   $a(CaONFJC)MIL173346
035   $a(EXLCZ)991000000000542528
100   $a20080407d2008      uy             0
101 0 $aeng
135   $aur|n|---|||||
181   $ctxt
182   $cc
183   $acr
200 10$aFormal logical methods for system security and correctness$b[electronic resource] /$fedited by Orna Grumberg, Tobias Nipkow and Christian Pfaller
210   $aAmsterdam, Netherlands ;$aWashington, DC $cIOS Press$dc2008
215   $a1 online resource (332 p.)
225 1 $aNATO security through science series. D, Information and communication security,$x1874-6268 ;$vv. 14
300   $a"Proceedings of the NATO Advanced Study Institute on Formal Logical Methods for System Security and Correctness, Marktoberdorf, Germany, 31 July-12 August 2007."--T.p. verso.
311   $a1-58603-843-5 
320   $aIncludes bibliographical references and index.
327   $aTitle page; Preface; Contents; Compilation of Certificates; Formal Foundations of Computer Security; Building a Software Model Checker; Symbolic Trajectory Evaluation (STE): Automatic Refinement and Vacuity Detection; Automated and Interactive Theorem Proving; Correctness of Effect-Based Program Transformations; Abstract and Concrete Models for Recursion; Secrecy Analysis in Protocol Composition Logic; The Engineering Challenges of Trustworthy Computing; Reflecting Quantifier Elimination for Linear Arithmetic; Content in Proofs of List Reversal; Proof Theory, Large Functions and Combinatorics
327   $aAuthor Index
330   $aOffers 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.
410  0$aNATO security through science series.$nD,$pInformation and communication security ;$vv. 14.
606   $aComputer security$vCongresses
606   $aComputer logic$vCongresses
608   $aElectronic books.
615  0$aComputer security
615  0$aComputer logic
676   $a005.8
701   $aGrumberg$b Orna$067499
701   $aNipkow$b Tobias$f1958-$062010
701   $aPfaller$b Christian$01046388
712 12$aNATO Advanced Study Institute on Formal Logical Methods for System Security and Correctness
801  0$bMiAaPQ
801  1$bMiAaPQ
801  2$bMiAaPQ
906   $aBOOK
912   $a9910453840003321
996   $aFormal logical methods for system security and correctness$92473255
997   $aUNINA