Witnessing the elimination of magic wands

Area of Science:

• Formal methods
• Software verification
• Programming language theory

Background:

• Separation logic is a powerful formalism for reasoning about heap-manipulating programs.
• Magic wands in separation logic specify incomplete resources but introduce undecidability challenges.
• Existing static verification tools often lack support for magic wands.

Purpose of the Study:

• To present a novel approach for static verification of programs using separation logic with magic wands.
• To address the undecidability issues associated with magic wands in program verification.
• To integrate this approach into the VerCors toolset for verifying Java programs.

Main Methods:

• Introducing the concept of a 'witness' to circumvent the undecidability of magic wands.
• Encoding specifications with magic wands into equivalent specifications without magic wands.
• Translating annotated Java programs to Chalice, then to BoogiePL for proof obligation generation.

Main Results:

• A method to handle magic wands in static verification by using witnesses.
• Successful encoding of magic wands and abstract predicates with permission parameters.
• Demonstration of the approach on the tree delete algorithm and linked list iterator verification.

Conclusions:

• The witness-based approach effectively handles magic wands in static verification.
• This method enhances the capabilities of static verification tools like VerCors.
• The approach is applicable to complex data structure algorithms and program verification tasks.