000			02292nam a22003498i 4500
001			CR9781139629294
003			UkCbUP
005			20200124160216.0
006			m|||||o||d||||||||
007			cr||||||||||||
008			121130s2015||||enk o ||1 0|eng|d
020			_a9781139629294 (ebook)
020			_z9781107040731 (hardback)
020			_z9781107656840 (paperback)
040			_aUkCbUP _beng _erda _cUkCbUP
050	0	0	_aQA76.73.S59 _bM38 2015
082	0	0	_a004.2 _223
100	1		_aMcCormick, John W., _d1948- _eauthor.
245	1	0	_aBuilding high integrity applications with SPARK / _cJohn W. McCormick, University of Northern Iowa, Peter C. Chapin, Vermont Technical College.
264		1	_aCambridge : _bCambridge University Press, _c2015.
300			_a1 online resource (xiv, 367 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).
520			_aSoftware is pervasive in our lives. We are accustomed to dealing with the failures of much of that software - restarting an application is a very familiar solution. Such solutions are unacceptable when the software controls our cars, airplanes and medical devices or manages our private information. These applications must run without error. SPARK provides a means, based on mathematical proof, to guarantee that a program has no errors. SPARK is a formally defined programming language and a set of verification tools specifically designed to support the development of software used in high integrity applications. Using SPARK, developers can formally verify properties of their code such as information flow, freedom from runtime errors, functional correctness, security properties and safety properties. Written by two SPARK experts, this is the first introduction to the just-released 2014 version. It will help students and developers alike master the basic concepts for building systems with SPARK.
650		0	_aSPARK (Computer program language)
650		0	_aFault-tolerant computing.
700	1		_aChapin, Peter C., _eauthor.
776	0	8	_iPrint version: _z9781107040731
856	4	0	_uhttps://doi.org/10.1017/CBO9781139629294
999			_c516327 _d516325