Para : parameterized path reduction, acceleration, and SMT for reachability in threshold-guarded distributed...

Area of Science:

• Computer Science
• Distributed Systems
• Formal Verification

Background:

• Automatic verification of fault-tolerant distributed algorithms (FTDAs) is complex due to parameterized conditions and system sizes.
• Existing bounded model checking (BMC) techniques require improvements for verifying state-of-the-art FTDAs.

Purpose of the Study:

• To enhance the efficiency and completeness of automatic verification for FTDAs.
• To develop a novel technique for verifying complex FTDAs that were previously intractable.

Main Methods:

• Encoding bounded executions of counter systems over integer counters in SMT (Satisfiability Modulo Theories).
• Introducing a new reduction technique exploiting acceleration and FTDA structure to prune the search space.
• Applying data and counter abstraction followed by bounded model checking.

Main Results:

• Successfully verified the safety of seven state-of-the-art FTDAs that were previously out of reach.
• The new SMT-based approach with aggressive pruning significantly improves verification capabilities.

Conclusions:

• The proposed SMT-based verification technique offers a more powerful and scalable approach for FTDAs.
• This advancement enables the verification of complex distributed systems, enhancing their reliability.