Induction-based Verification of Timed Systems / vorgelegt von Tobias Isenberg, M.Sc. Paderborn, 2016
Content
- List of Figures
- List of Tables
- Introduction
- Background
- Timed Automata Verification via IC3 with Zones
- SMT-Encoding
- Variables
- Encoding of the Initial States
- Encoding of Clock Constraints
- Encoding of Integer Constraints
- Encoding of Invariants
- Encoding of Clock and Integer Updates
- Encoding of Edges
- Encoding of Transition Relation
- Encoding of Safety Property
- Usage of the Encodings in the Queries
- State Extraction
- Zone Abstraction
- Algorithm
- Evaluation
- Benchmark Models
- Implementation
- Heuristics for ordering Literals
- Experiments
- Inductive Strengthening Experiments
- Summary
- Incremental Inductive Verification of Parameterized Timed Systems
- Restrictions
- Symmetry
- Specification via Templates
- Decidability
- Basic Approach
- Optimizations
- Evaluation
- Related Work
- Summary
- Verification of Extended Parameterized Timed Systems
- Inductive Verification of Reconfigured Models
- Adaptation of the Formula
- Approach in Summary
- Experiments
- Experiments with Addition
- Experiments with Deletion
- Experiments with Large Models
- Experiments with Constants
- Counterexample Experiment
- Related Work
- Summary
- Conclusion
- Discussion
- Future Work
- IC3 with Zones - Technique
- Parameterized Timed Systems - Technique
- General Reconfigurations - Technique
- Summary
- Experimental Results
- Proofs
- Bibliography