3 papers
cs.PL2022
Traits for Correct-by-Construction Programming
Tobias Runge, Alex Potanin, Thomas Thüm +1
We demonstrate that traits are a natural way to support correctness-by-construction (CbC) in an existing programming language in the presence of traditional post-hoc verification (…
cs.PL2019
Sound Invariant Checking Using Type Modifiers and Object Capabilities
Isaac Oscar Gariano, Marco Servetto, Alex Potanin
In this paper we use pre existing language support for type modifiers and object capabilities to enable a system for sound runtime verification of invariants. Our system guarantees…
cs.PL2019
Iteratively Composing Statically Verified Traits
Isaac Oscar Gariano, Marco Servetto, Alex Potanin +1
Static verification relying on an automated theorem prover can be very slow and brittle: since static verification is undecidable, correct code may not pass a particular static ver…