2 papers
cs.LO2021
Proving and Disproving Programs with Shared Mutable Data
Georg Schmid, Viktor Kunčak
We present a tool for verification of deterministic programs with shared mutable references against specifications such as assertions, preconditions, postconditions, and read/write…
cs.PL2020
Coming to Terms with Your Choices: An Existential Take on Dependent Types
Georg Stefan Schmid, Olivier Blanvillain, Jad Hamza +1
Type-level programming is an increasingly popular way to obtain additional type safety. Unfortunately, it remains a second-class citizen in the majority of industrially-used progra…