Michael Homer

See:

Recent Publications

Dafny vs. Dala: Experience with Mechanising Language Design by James Noble, Julian Mackay, Tobias Wrigstad, Andrew Fawcet, Michael Homer in FTfJP

Dala is a design for a concurrent dynamic object-oriented language. A key goal of Dala’s design is to avoid data races, by ensuring threads do not share mutable state. In this paper we discuss our experience using the program verification tool Dafny to validate Dala’s design. We explain how we modelled salient features of Dala in Dafny, and how Dafny did (or did not) assist our confidence in Dala’s design.

View the author copy.
Michael Homer — 2024 c7f3d658