000 03897nam a22005175i 4500
001 978-0-85729-018-2
003 DE-He213
005 20140220083711.0
007 cr nn 008mamaa
008 110103s2011 xxk| s |||| 0|eng d
020 _a9780857290182
_9978-0-85729-018-2
024 7 _a10.1007/978-0-85729-018-2
_2doi
050 4 _aQA76.758
072 7 _aUMZ
_2bicssc
072 7 _aCOM051230
_2bisacsh
082 0 4 _a005.1
_223
100 1 _aAlmeida, José Bacelar.
_eauthor.
245 1 0 _aRigorous Software Development
_h[electronic resource] :
_bAn Introduction to Program Verification /
_cby José Bacelar Almeida, Maria João Frade, Jorge Sousa Pinto, Simão Melo de Sousa.
264 1 _aLondon :
_bSpringer London :
_bImprint: Springer,
_c2011.
300 _aXIII, 307p. 52 illus.
_bonline resource.
336 _atext
_btxt
_2rdacontent
337 _acomputer
_bc
_2rdamedia
338 _aonline resource
_bcr
_2rdacarrier
347 _atext file
_bPDF
_2rda
490 1 _aUndergraduate Topics in Computer Science,
_x1863-7310
505 0 _aList of Figures -- 1. Introduction -- 2. An Overview of Formal Methods Tools and Techniques -- 3. Propositional Logic -- 4. First-Order Logic -- 5. Hoare Logic -- 6. Generating Verification Conditions -- 7. Safety Properties -- 8. Procedures and Contracts -- 9. Specifying C Programs -- 10. Verifying C Programs -- Bibliography -- Index.
520 _aThe use of mathematical methods in the development of software is essential when reliable systems are sought; in particular they are now strongly recommended by the official norms adopted in the production of critical software. Program Verification is the area of computer science that studies mathematical methods for checking that a program conforms to its specification. This text is a self-contained introduction to program verification using logic-based methods, presented in the broader context of formal methods for software engineering. The idea of specifying the behaviour of individual software components by attaching contracts to them is now a widely followed approach in program development, which has given rise notably to the development of a number of behavioural interface specification languages and program verification tools. A foundation for the static verification of programs based on contract-annotated routines is laid out in the book. These can be independently verified, which provides a modular approach to the verification of software. The text assumes only basic knowledge of standard mathematical concepts that should be familiar to any computer science student. It includes a self-contained introduction to propositional logic and first-order reasoning with theories, followed by a study of program verification that combines theoretical and practical aspects -- from a program logic (a variant of Hoare logic for programs containing user-provided annotations) to the use of a realistic tool for the verification of C programs (annotated using the ACSL specification language), through the generation of verification conditions and the static verification of runtime errors.
650 0 _aComputer science.
650 0 _aSoftware engineering.
650 0 _aLogic design.
650 0 _aAlgebra
_xData processing.
650 1 4 _aComputer Science.
650 2 4 _aSoftware Engineering.
650 2 4 _aLogics and Meanings of Programs.
650 2 4 _aSymbolic and Algebraic Manipulation.
700 1 _aFrade, Maria João.
_eauthor.
700 1 _aPinto, Jorge Sousa.
_eauthor.
700 1 _aMelo de Sousa, Simão.
_eauthor.
710 2 _aSpringerLink (Online service)
773 0 _tSpringer eBooks
776 0 8 _iPrinted edition:
_z9780857290175
830 0 _aUndergraduate Topics in Computer Science,
_x1863-7310
856 4 0 _uhttp://dx.doi.org/10.1007/978-0-85729-018-2
912 _aZDB-2-SCS
999 _c105107
_d105107