WJUG August 2015: Verifying Software with Whiley

12 views
Skip to first unread message

John Hurst

unread,
Aug 12, 2015, 3:14:14 AM8/12/15
to wellington-jug...@googlegroups.com, nzj...@yahoogroups.com, David Pearce, Nigel Charman
Hello.

I am pleased to announce the Wellington Java User Group meeting for August 2015.

Verifying Software with Whiley

Wednesday, August 26: 5:00 for 5:!5-6:30pm

Whiley is a programming language being developed at Victoria University of Wellington, New Zealand (see http://whiley.org). Whiley currently compiles to the JVM and is fully inter-operable with Java. Whiley is being designed to help eliminate software errors.  Whiley programs can be "verified" at compile time, and doing this prevents a range of common errors impossible (e.g. divide-by-zero, array out-of-bounds, etc). Unfortunately, the act of verifying a program presents its own challenges.

The Whiley project has been running since 2009 and, more recently, has been undergoing a number of changes to its syntax.  In this talk, I will look at what verification means in Whiley using a series of interesting examples.  I will also look at how the language is evolving and what is influencing this (e.g. embedded systems, Rust, etc).

Speaker: David Pearce

David (@whileydave) graduated with a PhD from Imperial College London in 2005, and took up a lecturer position at Victoria University of Wellington, NZ. David's PhD thesis was on efficient algorithms for pointer analysis of C, and his techniques have since been incorporated into GCC. His interests are in programming languages, compilers and static analysis.

Since 2009, he has been developing the Whiley Programming Language (whiley.org) which is designed specifically to simplify program verification. Prior to that, David developed the Java Compiler Kit (JKit), which is an open source Java Compiler aimed at simplifying static analysis.

David has previously interned at Bell Labs, New Jersey, where he worked on compilers for FPGAs; and also at IBM Hursely, UK, where he worked with the AspectJ development team on profiling systems.

You find out more about David's work on his personal homepage: http://www.ecs.vuw.ac.nz/~djp/

Venue

This meeting is hosted by:
Victoria University of Wellington
Government Buildings
Lecture Theatre: GBLT4
15 Lambton Quay
Wellington

The Java User Group thanks our host!

Please extend an invitation to attend to any interested friends or colleagues. As always, there is no cost involved!

Regards

John Hurst

Reply all
Reply to author
Forward
0 new messages