Copenhagen Programming Language Seminar

Tales of Applied Formal Methods

Joseph Kiniry
University College Dublin

Tuesday March 24 2009, 13:00-14:00
The IT University, Rued Langgaards Vej 7, DK-2300 Auditorium 4


Many software geeks only dig code; many formal methods researchers are all about the mathematics. My research group is full of folks that search for that delicate balance between practicality and formality. In my group we see spirit for OpenBSD kernel hacking and ardor for category theory mingling like a good cocktail in the same researcher! In this talk, I'll discuss our research ethos and some of our past projects that evidence this somewhat unusual perspective on applied formal methods across a number of domains.

Topics I'll cover include verification foundations, infrastructure, and tools; higher-order and first-order theorem proving; and case studies in dependable software engineering, including developing e-voting systems to shame governments into rejecting e-voting, and teaching formal methods to undergraduate students using ninja stealth. Projects that I'll reflect upon include ESC/Java2, PVS, SMT solvers, FreeBoogie, Votail, and the Mobius Program Verification Environment. To give an in-depth view of some recent research, I'll dive into the CLOPS system, which integrates feature modeling, DSLs, and command-line tools, and discuss our new novel type system for the EBON specification language, written using Literate PVS.

Scientific host:Lars Birkedal Administrative host: Annette Enggaard. All are welcome.
The Copenhagen Programming Language Seminar (COPLAS) is a collaboration between DIKU, ITU, KVL and RUC.
COPLAS is sponsored by the FIRST Graduate School.
To receive information about COPLAS talks by email, send a message to prog-lang-request@mail.it-c.dk with the word 'subscribe' as subject or in the body.

For more information about COPLAS, see http://www.coplas.org