Structural Temporal Logic for Mechanized Program Verification

Eleftherios Ioannidis, Yannick Zakowski, Steve Zdancewic +1

Mechanized verification of liveness properties for infinite programs with effects and nondeterminism is challenging. Existing temporal reasoning frameworks operate at the level of…