Practical Extensions of Multi-Property Verification
Combining and tuning techniques for verifying multiple properties in practice
This talk explores practical extensions of verification techniques that check multiple properties within a single workflow, with a focus on empirical evaluation and configuration tuning.
The presentation covers:
- a comparison of instrumentation and specification automata for property formalization;
- further refinements of the multi-aspect verification method;
- sequential combinations of multi-aspect verification with on-the-fly decomposition;
- the impact of the number of checked properties on verification performance and results.
The talk is based on extensive experiments and highlights practical trade-offs encountered when scaling multi-property verification to real-world programs.