Maximal Trace Semantics

For more info about our services contact : help@bestpfe.com

Table of contents

I Introduction 
1 Introduction 
1.1 Software Verification
1.1.1 Testing
1.1.2 Formal Methods
1.2 Program Properties
1.2.1 Safety Properties
1.2.2 Liveness Properties
1.3 Termination
1.4 Liveness Properties
II Safety 
2 Abstract Interpretation 
2.1 Basic Notions and Notations
2.2 Abstract Interpretation
2.2.1 Maximal Trace Semantics
2.2.2 Galois Connections
2.2.3 Widening and Narrowing
3 A Small Imperative Language 
3.1 A Small Imperative Language
3.2 Maximal Trace Semantics
3.3 Invariance Semantics
3.4 Numerical Abstract Domains
3.4.1 Intervals Abstract Domain
3.4.2 Polyhedra Abstract Domain
3.4.3 Octagons Abstract Domain
III Termination 
4 An Abstract Interpretation Framework for Termination 
4.1 Ranking Functions
4.2 Termination Semantics
4.2.1 Termination Trace Semantics
4.2.2 Termination Semantics
4.3 Denotational Definite Termination Semantics
5 Piecewise-Defined Ranking Functions 
5.1 Piecewise-Defined Ranking Functions
5.2 Decision Trees Abstract Domain
5.2.1 Decision Trees
5.2.2 Binary Operators
5.2.3 Unary Operators
5.2.4 Widening
5.3 Abstract Definite Termination Semantics
5.4 Related Work
6 Ordinal-Valued Ranking Functions 
6.1 Ordinal-Valued Ranking Functions
6.2 Ordinal Arithmetic
6.3 Decision Trees Abstract Domain
6.3.1 Decision Trees
6.3.2 Binary Operators
6.3.3 Unary Operators
6.3.4 Widening
6.4 Abstract Definite Termination Semantics
6.5 Related Work
7 Recursive Programs 
7.1 A Small Procedural Language
7.2 Maximal Trace Semantics
7.3 Definite Termination Semantics
7.3.1 Definite Termination Semantics
7.3.2 Abstract Definite Termination Semantics
8 Implementation 
8.1 FuncTion
8.2 Experimental Evaluation
IV Liveness 
9 A Hierarchy of Temporal Properties 
9.1 A Hierarchy of Temporal Properties
9.1.1 Safety Properties
9.1.2 Guarantee Properties
9.1.3 Obligation Properties
9.1.4 Recurrence Properties
9.1.5 Persistence Properties
9.1.6 Reactivity Properties
9.2 Guarantee Semantics
9.2.1 Guarantee Semantics
9.2.2 Denotational Guarantee Semantics
9.2.3 Abstract Guarantee Semantics
9.3 Recurrence Semantics
9.3.1 Recurrence Semantics
9.3.2 Denotational Recurrence Semantics
9.3.3 Abstract Recurrence Semantics
9.4 Implementation
9.5 Related Work
V Conclusion 
10 Future Directions 
Bibliography 
A Proofs
A.1 Missing Proofs from Chapter 1
A.2 Missing Proofs from Chapter 4
A.3 Missing Proofs from Chapter 5
A.4 Missing Proofs from Chapter 6
A.5 Missing Proofs from Chapter 7
A.6 Missing Proofs from Chapter 9