On-The-Fly safety checking - customizing program certification and program restructuring / vorgelegt von Marie-Christine Jakobs, Master of Science. Paderborn, 2017
Content
- List of Figures
- List of Tables
- Introduction
- Software Markets Easily Accessible to Everybody
- Assuring Correctness Properties in Global OTF Markets
- Thesis Contribution
- Thesis Outline
- Programs and Their Verification
- Configurable Program Certification
- Overview of Configurable Program Certification
- Producer Verification and Certificate Construction
- Consumer Certificate Validation
- Properties of the Consumer Certificate Validation
- Evaluation
- Discussion
- Optimization of Configurable Program Certification
- Reduction of the Certificate Size
- Certificate Partitioning
- Combination of Reduction and Partitioning
- Evaluation
- Discussion
- Related Work
- Programs from Proofs
- Overview of Programs from Proofs
- Producer Verification of the Original Program
- Program Generation
- Consumer Verification of the Generated Program
- Reverification of the Generated Program
- Evaluation
- Discussion
- Related Work
- Integration of PfP and CPC
- Motivation
- The Naïve Combination
- Certificates for Generated Program from Producer Proof
- Evaluation
- Discussion
- Related Work
- Conclusion
- Proofs
- Outstanding Proofs for Chapter 2
- Outstanding Proofs for Chapter 3
- Outstanding Proofs for Chapter 4
- Outstanding Proofs for Chapter 5
- Outstanding Proofs for Chapter 6
- Evaluation Results
- Results Basic Configurable Program Certification
- Results Optimized Configurable Program Certification
- Results Programs from Proofs Approach
- Results Integration of PfP and CPC
- Bibliography