Werner Dietl

Posted by on Monday, June 18, 2012 · Leave a Comment 

Verification Games: Making Verification Fun

VCLA will be hosting a RiSE seminar talk by Werner Dietl on June 20th, 2012.

DATE:Wednesday, June 20, 2012
TIME:11:00 – 12:00
VENUE:Library E185.1, Argentinierstrasse 8, 4th floor

ABSTRACT

Program verification is the only way to be certain that a given piece of software is free of (certain types of) errors --- errors that could otherwise disrupt operations in the field. To date, formal verification has been done manually, by specially-trained engineers. Labor costs have heretofore made formal verification too costly to apply beyond small, critical software components.

Our goal is to make verification more cost-effective by reducing the skill set required for program verification and increasing the pool of people capable of performing program verification. Our approach is to transform the verification task (a program and a goal property) into a visual puzzle task --- a game --- that gets solved by people. The solution of the puzzle is then translated back into a proof of correctness. The puzzle is engaging and intuitive enough that ordinary people can through game-play become experts.

This talk presents the status of the Verification Games project and our Pipe Jam prototype game.

The accompanying tutorial Developing and using pluggable type systems  will take place at the same day from 14:00 to 16:00 at the same venue.

Abstract:
 
A pluggable type system extends a language’s built-in type system to confer additional compile-time guarantees. We will explain the theory and practice of pluggable types. The material is relevant for researchers who wish to apply type theory, and for anyone who wishes to increase confidence in their code. After this session, you will have the knowledge to: analyze a problem to determine whether pluggable type-checking is appropriate; design a domain-specific type system; implement a simple type-checker (in as little as 4 lines of code!); scale a simple type-checker to more sophisticated properties; and better appreciate both object-oriented types and flexible verification techniques.
 
While the theory is general, our hands-on exercises will use a state-of-the-art system, the Checker Framework, that works for the Java language, scales to millions of lines of code, and is being adopted in the research and industrial communities. Such a framework enables researchers to easily evaluate their type systems in the context of a widely-used industrial language, Java. It enablesnon-researchers to verify their code in a lightweight way and to create custom analyses. And it enables students to better appreciate type system concepts.

Filed under Talks · Tagged with

Comments are closed.