000 03523nam a22003735i 4500
001 291079
003 MX-SnUAN
005 20160429154829.0
007 cr nn 008mamaa
008 150903s2009 xxk| o |||| 0|eng d
020 _a9781848822405
_99781848822405
024 7 _a10.1007/9781848822405
_2doi
035 _avtls000344394
039 9 _a201509030403
_bVLOAD
_c201405050306
_dVLOAD
_y201402061255
_zstaff
040 _aMX-SnUAN
_bspa
_cMX-SnUAN
_erda
050 4 _aQA76.758
100 1 _aStanley, William.
_eautor
_9322182
245 1 0 _aSoftware Verification and Analysis :
_bAn Integrated, Hands-On Approach /
_cby William Stanley, Janusz Laski.
264 1 _aLondon :
_bSpringer London :
_bImprint: Springer,
_c2009.
300 _brecurso en línea.
336 _atexto
_btxt
_2rdacontent
337 _acomputadora
_bc
_2rdamedia
338 _arecurso en línea
_bcr
_2rdacarrier
347 _aarchivo de texto
_bPDF
_2rda
500 _aSpringer eBooks
505 0 _aThe Semantic Analysis -- Why Not Write Correct Software the First Time? -- How to Prove a Program Correct: Programs Without Loops -- How to Prove a Program Correct: Iterative Programs -- Prepare Test for Any Implementation: Black-Box Testing -- Static Analysis -- Intermediate Program Representation -- Program Dependencies -- What Can One Tell About a Program Without Its Execution: Static Analysis -- Dynamic Analysis -- Is There a Bug in the Program? Structural Program Testing -- Dynamic Program Analysis.
520 _aThis book advocates the integrated and tool supported use of all available verification methods to improve software correctness. The following major software verification techniques and their supporting tools, based on sound mathematical models, are discussed: • Correctness by construction, using the Vienna Development Method-Specification Language (VDM-SL) and its supporting CSK’s Toolbox. • Static program analysis supported by the PRAXIS’ SPARK toolset and SofTools’ System for Testing And Debugging (STAD 4.0). • Program proving supported by SPARK. • Dynamic program analysis supported by STAD. VDM-SL Toolbox and SPARK illustrate, respectively, the correctness by construction and program proving paradigms. The author demonstrates that while both methods are powerful, errors are inevitable and detecting these may be more difficult than in the case of an informally developed program. Consequently, error detection must be an integral part of the entire life cycle of a programming project. Black-Box (specification based) and Structural (code based) testing are covered and supported by STAD (including 5 testing criteria). STAD also features a quite powerful descriptive and proscriptive static analysis. Software engineers, students and computer scientists will find that the book provides the reader with a comprehensive understanding of software verification issues. STAD’s outputs allow the user to implement and test their own ideas. The most recent version of STAD can be downloaded from http://www.stadtools.com.
590 _aPara consulta fuera de la UANL se requiere clave de acceso remoto.
700 1 _aLaski, Janusz.
_eautor
_9322183
710 2 _aSpringerLink (Servicio en línea)
_9299170
776 0 8 _iEdición impresa:
_z9781848822399
856 4 0 _uhttp://remoto.dgb.uanl.mx/login?url=http://dx.doi.org/10.1007/978-1-84882-240-5
_zConectar a Springer E-Books (Para consulta externa se requiere previa autentificación en Biblioteca Digital UANL)
942 _c14
999 _c291079
_d291079