000			02945nam a2200361 i 4500
001			CR9781107256552
003			UkCbUP
005			20240916200911.0
006			m|||||o||d||||||||
007			cr||||||||||||
008			130516s2014||||enk o ||1 0|eng|d
020			_a9781107256552 (ebook)
020			_z9781107048010 (hardback)
040			_aUkCbUP _beng _erda _cUkCbUP
050	0	0	_aQA76.76.V47 _bA65 2014
082	0	0	_a005.1/4 _223
100	1		_aAppel, Andrew W., _d1960- _eauthor.
245	1	0	_aProgram logics for certified compilers / _cAndrew W. Appel [and seven others].
264		1	_aCambridge : _bCambridge University Press, _c2014.
300			_a1 online resource (x, 458 pages) : _bdigital, PDF file(s).
336			_atext _btxt _2rdacontent
337			_acomputer _bc _2rdamedia
338			_aonline resource _bcr _2rdacarrier
500			_aTitle from publisher's bibliographic system (viewed on 05 Oct 2015).
505	0		_aGeneric separation logic -- Hoare logic -- Separation logic -- Soundness of Hoare logic -- Mechanized semantic library -- Separation algebras -- Operators on separation algebras -- First-order separation logic -- A little case study -- Covariant recursive predicates -- Share accounting -- Higher order separation logic -- Separation logic as a logic -- From separation algebras to separation logic -- Simplification by rewriting -- Introduction to step-indexing -- Predicate implication and subtyping -- General recursive predicates -- Case study: separation logic with first-class functions.
520			_aSeparation logic is the twenty-first-century variant of Hoare logic that permits verification of pointer-manipulating programs. This book covers practical and theoretical aspects of separation logic at a level accessible to beginning graduate students interested in software verification. On the practical side it offers an introduction to verification in Hoare and separation logics, simple case studies for toy languages, and the Verifiable C program logic for the C programming language. On the theoretical side it presents separation algebras as models of separation logics; step-indexed models of higher-order logical features for higher-order programs; indirection theory for constructing step-indexed separation algebras; tree-shares as models for shared ownership; and the semantic construction (and soundness proof) of Verifiable C. In addition, the book covers several aspects of the CompCert verified C compiler, and its connection to foundationally verified software analysis tools. All constructions and proofs are made rigorous and accessible in the Coq developments of the open-source Verified Software Toolchain.
650		0	_aComputer software _xVerification.
650		0	_aLogic, Symbolic and mathematical.
650		0	_aCompilers (Computer programs)
776	0	8	_iPrint version: _z9781107048010
856	4	0	_uhttps://doi.org/10.1017/CBO9781107256552
942			_2ddc _cEB
999			_c9449 _d9449