Bringing Down the Cost of Verification
Please log in to watch this conference skillscast.
Producing formally verified software is expensive, as it is a time consuming, often tedious process, which requires expert skills not widely available. If we want to reduce these costs, we need to automate as much of the process as possible, and we need to make the technology more accessible to developers without specialised skills in verification. This talk explores some of the issues of verification, in particular in the context of file systems and presents a language based approach to systems code verification. Using a strict, purely functional language with linear types, and a verifying compiler results in a significant reduction of the costs involved.
YOU MAY ALSO LIKE:
Bringing Down the Cost of Verification
Gabriele Keller
Gabriele Keller has recently been appointed as chair of the Software Technology Group at Utrecht University. Before moving to the Netherlands, she co-founded the Programming Languages & Systems Group at the University of New South Wales, and was a Principal Researcher at Data6 (formerly NICTA) in the Trustworthy Systems project.