Abstract
We have experimented with modeling some of the key concepts of the VDM specification language inside the functional programming language Haskell. For instance, VDM’s sets and maps are directly available as data types defined in standard libraries; we merely needed to define some additional functions to make the match complete. A bigger challenge is posed by VDM’s data type invariants, and pre- and post-conditions. For these we resorted to Haskell’s constructor class mechanism, and its support for monads. This allows us to switch between different modes of evaluation (e.g. with or without property checking) by simply coercing user defined functions and operations to different specific types.
Alexandra Mendes
Assistant Professor
My research focuses on encouraging a wider adoption of software verification by creating tools and methods that hide the complexities of verifying software. Recently, I started work on usable security, in particular on the impact of formal verification on the use and adoption of formally verified security software products. Much of my most recent work overlaps with the area of software engineering. For more details, see selected publications and some of my projects. Follow me on Twitter or add me on LinkedIn.