曝光台 注意防骗
网曝天猫店富美金盛家居专营店坑蒙拐骗欺诈消费者
nPacketsOld = nPackets;
if(request){
request = request->Next;
KeReleaseSpinLock();
nPackets++;
}
} while(nPackets!=nPacketsOld);
KeReleaseSpinLock();
11
Refined Boolean Abstraction
s:=U;
do {
assert(s=U); s:=L;
b := true;
if(*){
assert(s=L); s:=U;
b := b ? false : *;
}
} while ( !b );
assert(s=L); s:=U;
b : (nPacketsOld == nPackets)
b
b
b
b
U
L
L
L
L
U
L
U
U
b
b
!b
12
Invariant
13
Software Verification:
A Search for Abstractions
• A complex search space with a fitness
function (false errors)
– search for right abstraction
– search within state space of abstraction
• Can a machine beat a human at search
for the right abstractions?
• Deep Blue beat Kasparov
14
Overview
• Part I: Abstract Interpretation
– [Cousot & Cousot, POPL’77]
– Manual abstraction and refinement
– ASTRÉE Analyzer
• Part II: Predicate Abstraction
– [Graf & Saïdi, CAV ’97]
– Automated abstraction and refinement
– SLAM and Static Driver Verifier
• Part III: Comparing Approaches
15
16
17
18
19
20
21
22
23
24
25
26
Abstract Transitions
a
a’
27
28
29
Slide courtesy of Patrick Cousot
30
Slide courtesy of Patrick Cousot
31
Slide courtesy of Patrick Cousot
32
Slide courtesy of Patrick Cousot
33
Diagram from Cousot, Cousot, POPL 1977
34
35
36
37
Patrick Cousot, Radhia Cousot, Jérôme Feret, Laurent Mauborgne,
Antoine Miné, David Monniaux, Xavier Rival, Bruno Blanchet
ASTRÉE analyzes structured C programs, without dynamic
memory allocation and recursion.
In Nov. 2003, ASTRÉE automatically proved the absence of any run-time
error in the primary flight control software of the Airbus A340 fly-by-wire
system
a program of 132,000 lines of C analyzed in 1h20 on a 2.8 GHz 32-bit PC
using 300 Mb of memory
38
Abstraction Refinement:
PLDI’03 Case Study of Blanchet et al.
• “… the initial design phase is an iterative manual
refinement of the analyzer.”
• “Each refinement step starts with a static analysis of the
program, which yields false alarms. Then a manual
backward inspection of the program starting from sample
false alarms leads to the understanding of the origin of
the imprecision of the analysis.”
• “There can be two different reasons for the lack of
precision:
– some local invariants are expressible in the current version of
the abstract domain but were missed
– some local invariants are necessary in the correctness proof but
are not expressible in the current version of the abstract
domain.”
39
Part I: Summary
• Create abstract domains and supporting
algorithms
• Relate domains via and functions
• Prove Galois connection
• Create abstract transformer T#
• Show that T# approximates ° T °
• Widening to achieve termination
• Refinement to reduce false errors
40
Part II: Predicate Abstraction
– Graf & Saïdi, CAV ’97
• Idea
– Given set of predicates P = { P1, …, Pk }
• Formulas describing properties of system state
• Abstract State Space
– Set of Boolean variables B = { b1, …, bk }
• bi = true Set of states where Pi holds
– 41 –
Apppprrooxxiimaattiinngg ccoonnccrreettee ssttaatteess
Fundamental Operation
Approximating a set of
concrete states by a set of
predicates
Requires exponential
number of theorem prover
calls in worst case
#
Partitioning defined by the predicates
42
Abstraction and Concretization
Functions
43
Abstraction and Concretization
Functions
44
Abstraction and Concretization
Functions
45
46
47
48
49
50
51
52
53
54
55
Refining Predicate Abstraction
56
Initial set = I
Error set = E
abstract error path = S0, S1, … , Sk
中国航空网 www.aero.cn
航空翻译 www.aviation.cn
本文链接地址：
航空资料23(85)
