Kontakt
Kako kupovati
Dostava
Savjetnik za kupnju
Scalable Bit-precise Formal Verification of Embedded Software
Engleski
99 b
Do 30 dana za povrat
Kupci su kupili i
/
Meki uvez
13.65
€
/
Meki uvez
32.06
€
/
Meki uvez
16.18
€
Many of the automatic formal verification techniques choose to model a non-Boolean program variable as a bit-vector with bounded width (i.e. a vector of multiple bits like 32- or 64- bits) to achieve bit-precise verification. The major challenge of applying such formal technique to real-world embedded software is scalability. This book explores several abstraction techniques to deal with this challenge. It first proposes a tight integration of program slicing, which is an important static program analysis technique, with bounded model checking. Then it presents a new symbolic simulation for scalable formal verification. This simulation involves using distinguishing Xs as symbolic values to abstract concrete variables' values. It also defines two testability metrics - controllability and observability - as the high-level structural guidance to improve efficiency of the proof-based abstraction refinement framework. This book finally proposes a novel algorithm to discover path-oriented non-uniform encoding widths of individual variables, which may be smaller than their original modeling width but large enough for formal verification.
Informacije o knjizi
Engleski
Kategorija
Poklonite ovu knjigu još danas
To je jednostavno
1 Dodajte knjigu u košaricu i odaberite isporuku kao poklon 2 Zauzvrat ćemo vam poslati kupon 3 Knjiga dolazi na adresu poklonoprimcaMoglo bi vas zanimati i
/
Tvrdi uvez
45.81
€
/
Meki uvez
14.86
€
/
Meki uvez
7.68
€
/
Tvrdi uvez
237.71
€
Dobar dan! Ja sam Libroamiko, vaš književni savjetnik.
Kako vam mogu pomoći?