Extending ITL with Interleaved Programs for Interactive Verification
Gerhard Schellhorn · 2011
The talk presents extensions of ITL that make it a powerful logic to reason about interleaved programs with recursive procedures. The extensions have been implemented in the interactive theorem prover KIV.