1 citations · 1 across the 6 of their papers we have counts for
6 papers
Semantically Separating Nominal Wyvern for Usability and Decidability
Yu Xiang Zhu, Amos Robinson, Sophia Roshal +4
The Dependent Object Types (DOT) calculus incorporates concepts from functional languages (e.g. modules) with traditional object-oriented features (e.g. objects, subtyping) to achi…
Flexible Correct-by-Construction Programming
Tobias Runge, Tabea Bordis, Alex Potanin +2
Correctness-by-Construction (CbC) is an incremental program construction process to construct functionally correct programs. The programs are constructed stepwise along with a spec…
Information Flow Control-by-Construction for an Object-Oriented Language Using Type Modifiers
Tobias Runge, Alexander Kittelmann, Marco Servetto +2
In security-critical software applications, confidential information must be prevented from leaking to unauthorized sinks. Static analysis techniques are widespread to enforce a se…
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 (…
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…
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…