Verifying non-terminating programs with IO in F*
We present a work-in-progress definition of an F* effect for writing, specifying, and verifying functional correctness for higher-order programs with input-output. We then extend this effect to support potentially non-terminating programs. Crucially we do not stop at partial correctness where the specification only concludes about terminating runs, but instead rely on infinite traces to also reason about infinite runs. We aim to use this to verify meaningful properties of infinite loops, such as the main loop of a web server. As F* does not natively support coinduction, we encode specifications about infinite traces using an impredicative encoding of an infinite loop at the level of specifications.
Sun 11 SepDisplayed time zone: Belgrade, Bratislava, Budapest, Ljubljana, Prague change
16:00 - 17:30
|Dependent Temporal Type-and-Effect System with Delimited Continuations|
|Enabling Safe Shared-Memory Interoperability in WebAssemblyVirtual|
|Verifying non-terminating programs with IO in F*|
Cezar-Constantin Andrici MPI-SP, Theo Winterhalter MPI-SP, Cătălin Hriţcu MPI-SP, Exequiel Rivas Tallinn University of TechnologyPre-print File Attached