The octagon abstract domain [Min01b]

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

Table of contents

1 Introduction 
1.1 Program verification
1.1.1 Tests
1.1.2 Model Checking
1.1.3 Program proving
1.1.4 Abstract interpretation
1.2 Content of the thesis
1.3 Outline of the thesis
2 Background – Abstract interpretation 
2.1 Notations
2.2 Order theory
2.2.1 Order and Galois connections
2.2.2 An example of Galois connection: intervals [CC76]
2.2.3 Operators, fixpoint theorems
2.2.4 Widening
2.3 Abstract Interpretation
2.3.1 By example
2.3.2 Improving precision of the abstract fixpoint computation
2.3.3 Composing abstract domains
2.3.4 Concretization only framework
2.4 Numerical Domains
2.4.1 Definitions
2.4.2 The polyhedra abstract domain [CH78]
2.4.3 The octagon abstract domain [Min01b]
2.4.4 Notations
2.5 Conclusion
3 MOPSA 
3.1 Introduction
3.1.1 Motivations
3.1.2 Outline of the chapter
3.2 Unified Domains Signature
3.2.1 Lattice
3.2.2 Managers
3.2.3 Flows
3.2.4 Evaluations
3.2.5 Queries
3.3 Domain Composition
3.4 Experiments
3.5 Conclusion
4 String abstraction 
4.1 Introduction
4.1.1 Motivations
4.1.2 Outline of the chapter
4.2 Syntax and concrete semantics
4.3 Background – Cell abstract domain
4.4 String abstract domain
4.4.1 Domain definition
4.4.2 Galois connection with the Cell abstract domain
4.4.3 Operators
4.4.4 Abstract evaluation
4.4.5 Abstract transformations
4.4.6 String declaration
4.4.7 Dynamic memory allocation
4.5 Related works
4.6 Conclusion
5 Modular analysis 
5.1 Introduction
5.1.1 Motivations
5.1.2 Outline of the chapter
5.2 General remarks
5.3 Using relational domains
5.4 Building the summary functions
5.4.1 Summaries
5.4.2 Inferring and proving summaries
5.4.3 Improvements
5.5 Preliminary experimental evaluation
5.6 Related works
5.7 Conclusion
6 Numerical Abstraction 
6.1 Introduction
6.1.1 Homogeneous definition sets
6.1.2 Fixed finite definition set
6.1.3 Outline of the chapter.
6.2 Concrete semantics
6.2.1 Definition
6.2.2 Example of use
6.3 State of the art
6.3.1 Partitioning
6.3.2 Encoding of optional variables via avatars
6.3.3 A folk technique for non relational domains
6.4 The CLIP abstraction
6.4.1 Abstraction definition
6.4.2 Composing inclusion and projection
6.4.3 Operator definitions
6.4.4 Abstract transformers
6.5 The integer case
6.5.1 Losing soundness
6.5.2 Losing parametricity
6.6 Bridging the gap with partitioning: the ℘-CLIP abstraction
6.6.1 Abstraction definition
6.6.2 Set difference between SVIs
6.6.3 Operator definitions
6.6.4 Widening operator
6.6.5 Abstract transformers
6.6.6 Conclusion
6.7 Unbounded maps
6.8 Conclusion
7 Tree abstraction 
7.1 Introduction
7.1.1 Trees and terms
7.1.2 Outline of the chapter
7.2 Syntax and concrete semantics
7.2.1 Terms and numerical terms
7.2.2 Syntax of the tree manipulating language
7.2.3 Concrete semantics of the language
7.2.4 Example
7.3 Background – (Tree) regular languages
7.3.1 Regular languages
7.3.2 Tree regular languages
7.3.3 Implementation remarks
7.4 State of the art
7.4.1 Using (Tree) Regular languages
7.4.2 Tree languages
7.4.3 Numerical terms
7.5 Natural term abstraction by tree automata
7.5.1 Value abstraction
7.5.2 Abstract transformers
7.5.3 Environment abstraction
7.6 Natural term abstraction by numerical constraints
7.6.1 Value abstraction
7.6.2 Abstract semantics of operators
7.7 Building up the full abstraction
7.7.1 Product
7.7.2 Removing redundant information
7.7.3 Factoring away the numerical component
7.7.4 Functional evaluation of tree expressions
7.8 Implementation and example
7.9 Conclusion
8 Conclusion 
8.1 Summary of the thesis
8.2 Concluding example
8.3 Future works