Sun 23 Jun 2019 09:30 - 10:00 at 212B - Session I Chair(s): Neville Grech

New languages and virtual machines are proposed at an alarming rate, followed by new versions of them every few weeks, together with programs in these languages that are responsible for actions of potentially significant value. Many bugs and exploits, for example in the new cryptocurrency space, are due to flaws or weaknesses of the underlying programming languages or virtual machines. Formal analysis and verification tools are therefore needed immediately for such languages and virtual machines. The usual post-mortem approach to formal language semantics and verification, where the language is firstly implemented and used in production for many years before a need for formal semantics and verification tools naturally arises, simply does not work anymore. We present recent academic and commercial results in developing languages and virtual machines that come directly equipped with formal analysis and verification tools. The main idea is to generate all these automatically, correct-by-construction from a formal specification in the K Framework. We will also give a demo of the K framework by means of a simple language.

Sun 23 Jun

Displayed time zone: Tijuana, Baja California change

09:30 - 11:00
Session IDPA at 212B
Chair(s): Neville Grech University of Athens
09:30
30m
Talk
The K Framework
DPA
Sandeep Dasgupta University of Illinois at Urbana-Champaign, USA
10:00
30m
Talk
MetaDL and Beyond: Custom Program Analyses in Datalog
DPA
Christoph Reichenbach Lund University
10:30
30m
Talk
Datafun: A higher-order functional Datalog
DPA
Michael Arntzenius University of Birmingham, UK