Systems and Software Verification : Model-Checking Techniques and Tools /

Model checking is a powerful approach for the formal verification of software. When applicable, it automatically provides complete proofs of correctness, or explains, via counter-examples, why a system is not correct. This book provides a basic introduction to this new technique. The first part desc...

Full description

Bibliographic Details
Main Author: Bérard, Béatrice
Corporate Author: SpringerLink (Online service)
Other Authors: Bidoit, Michel, Finkel, Alain, Laroussinie, François, Petit, Antoine, Petrucci, Laure, Schnoebelen, Philippe, McKenzie, Pierre
Format: eBook
Language:English
Published: Berlin, Heidelberg : Springer Berlin Heidelberg, 2001.
Subjects:
Online Access:Connect to the full text of this electronic book

MARC

Tag First Indicator Second Indicator Subfields
LEADER 00000cam a2200000Mi 4500
001 in00003577621
006 m o d
007 cr mnu---uuaaa
008 130321s2001 gw o 000 0 eng
005 20260421164436.0
020 |a 9783662045589 (electronic bk.) 
020 |a 3662045583 (electronic bk.) 
020 |z 9783642074783 
020 |z 3642074782 
020 |z 3662045583 
035 |a (OCoLC)851367865 
040 |a AU@  |b eng  |c AU@  |d GW5XE  |d UtOrBLW 
049 |a TXAM 
050 4 |a QA76.758 
072 7 |a UMZ  |2 bicssc 
072 7 |a COM051230  |2 bisacsh 
082 0 4 |a 005.1  |2 23 
100 1 |a Bérard, Béatrice. 
245 1 0 |a Systems and Software Verification :  |b Model-Checking Techniques and Tools /  |c by Béatrice Bérard, Michel Bidoit, Alain Finkel, François Laroussinie, Antoine Petit, Laure Petrucci, Philippe Schnoebelen, Pierre McKenzie. 
264 1 |a Berlin, Heidelberg :  |b Springer Berlin Heidelberg,  |c 2001. 
300 |a 1 online resource (xii, 190 pages 67 illustrations) 
336 |a text  |b txt  |2 rdacontent 
337 |a computer  |b c  |2 rdamedia 
338 |a online resource  |b cr  |2 rdacarrier 
520 |a Model checking is a powerful approach for the formal verification of software. When applicable, it automatically provides complete proofs of correctness, or explains, via counter-examples, why a system is not correct. This book provides a basic introduction to this new technique. The first part describes in simple terms the theoretical basis of model checking: transition systems as a formal model of systems, temporal logic as a formal language for behavioral properties, and model-checking algorithms. The second part explains how to write rich and structured temporal logic specifications in practice, while the third part surveys some of the major model checkers available. 
500 |a Electronic resource. 
650 0 |a Computer science. 
650 0 |a Software engineering. 
650 0 |a Artificial intelligence. 
650 0 |a Information systems. 
655 7 |a Electronic books.  |2 local 
700 1 |a Bidoit, Michel. 
700 1 |a Finkel, Alain. 
700 1 |a Laroussinie, François. 
700 1 |a Petit, Antoine. 
700 1 |a Petrucci, Laure. 
700 1 |a Schnoebelen, Philippe. 
700 1 |a McKenzie, Pierre. 
710 2 |a SpringerLink (Online service) 
776 1 8 |i Print version:  |z 9783642074783 
856 4 0 |u http://proxy.library.tamu.edu/login?url=https://link.springer.com/10.1007/978-3-662-04558-9  |z Connect to the full text of this electronic book  |t 0 
994 |a 92  |b TXA 
999 |a MARS 
999 f f |s ececfa01-45f7-340a-98af-3947260fb20c  |i 7de0d9c3-d952-3175-86c7-d2058f158f87  |t 0 
952 f f |a Texas A&M University  |b College Station  |c Electronic Resources  |s www_evans  |d Available Online  |t 0  |e QA76.758  |h Library of Congress classification 
998 f f |a QA76.758  |t 0  |l Available Online