Predicate abstraction for hyperliveness verification

Area of Science:

• Formal methods
• Computer science
• Software verification

Background:

• Temporal hyperproperties analyze system behaviors across multiple execution traces.
• Existing verification methods for infinite-state systems are limited, primarily to k-safety properties.
• Analysis of temporal hyperproperties in infinite-state systems has historically been restricted.

Purpose of the Study:

• To present an automated method for verifying ∀ᵏ∃ˡ-safety properties in infinite-state systems.
• To extend the scope of verifiable temporal hyperproperties beyond k-safety.
• To enable the verification of complex properties like generalized non-interference and program refinement.

Main Methods:

• The verification method employs strategy-based instantiation for existential trace quantification.
• A program reduction technique is utilized within the verification process.
• The method operates within the framework of fixed predicate abstraction.

Main Results:

• An automated verification approach for ∀ᵏ∃ˡ-safety properties in infinite-state systems is successfully developed.
• The method effectively handles properties involving combined universal and existential quantification over traces.
• The approach supports the verification of hyperliveness properties, including generalized non-interference and program refinement.

Conclusions:

• The presented method significantly advances the automated verification of temporal hyperproperties in infinite-state systems.
• This work broadens the applicability of formal verification techniques to a wider range of complex system properties.
• The developed technique provides a foundation for analyzing and ensuring the correctness of advanced system behaviors.