Formal Methods. An Appetizer

Preface......Page 3
Prologue......Page 6
Contents......Page 11
1.1 Program Graphs......Page 14
1.2 Semantics......Page 16
1.3 The Structure of the Memory......Page 20
1.4 Properties of Program Graphs......Page 22
1.5 Bit-Level Semantics (Bonus Material)......Page 24
2.1 Syntax......Page 28
2.2 Program Graphs......Page 30
2.3 Semantics......Page 34
2.4 Alternative Approaches......Page 37
2.5 More Control Structures (Bonus Material)......Page 39
3.1 Predicates......Page 44
3.2 Predicate Assignments......Page 47
3.3 Partial Predicate Assignments......Page 49
3.4 Guarded Commands with Predicates......Page 53
3.5 Reverse Postorder (Bonus Material)......Page 56
4.1 Abstract Properties......Page 60
4.2 Analysis Assignments......Page 62
4.3 Analysis Functions......Page 64
4.4 Analysis Specification......Page 68
4.5 Computing Solutions (Bonus Material)......Page 71
5.1 Information Flow......Page 74
5.2 Reference-Monitor Semantics......Page 76
5.3 Security Analysis......Page 80
5.4 Multi-Level Security......Page 83
5.5 Non-Interference (Bonus Material)......Page 86
6.1 Transition Systems......Page 90
6.2 Computation Tree Logic – CTL......Page 93
6.3 Syntax and Semantics of CTL......Page 95
6.4 From Program Graphs to Transition Systems......Page 97
6.5 Towards an Algorithm (Bonus Material)......Page 99
7.1 Declarations......Page 104
7.2 Blocks......Page 106
7.3 Procedures with Dynamic Scope......Page 111
7.4 Procedures with Static Scope......Page 117
8.1 Shared Variables......Page 122
8.2 Asynchronous Communication......Page 125
8.3 Synchronous Communication......Page 130
8.4 Broadcast and Gather (Bonus Material)......Page 132
Epilogue......Page 137
MicroC Language......Page 140
Programming Projects......Page 143
Core Development......Page 146
Program Verification......Page 149
Program Analysis......Page 151
Language-based Security......Page 154
Learning Environment......Page 157
Welcome Screen......Page 158
Step-wise Execution......Page 159
Verification Conditions......Page 160
Detection of Signs Analysis......Page 161
Security Analysis......Page 162
Symbols......Page 163
Index......Page 165