Mon 15 Jul 2019 10:45 - 11:45 at Epernay - Session One

This talk will give an overview of the JayHorn verification tool, a model checker for sequential Java programs annotated with assertions expressing safety conditions. JayHorn is fully automatic and based to a large degree on standard infrastructure for compilation and verification: it uses the Soot library as front-end to read Java bytecode and translate it to the Jimple three-address format, and the state-of-the-art Horn solvers SPACER and Eldarica as back-ends that infer loop invariants, object and class invariants, and method contracts. Since JayHorn uses an invariant-based representation of heap data-structures, it is particularly useful for analysing programs with unbounded data-structures and unbounded run-time, while at the same time avoiding the use of logical theories, like the theory of arrays, often considered hard for Horn solvers. The development of JayHorn is ongoing, and the talk will also cover some of the future features of JayHorn, in particular the handling of strings. The talk presents joint work with Daniel Dietsch, Temesghen Kahsai, Rody Kersten, Huascar Sanchez, Martin Schäf, and Valentin Wüstholz.

Mon 15 Jul

Displayed time zone: Belfast change

10:45 - 12:15
Session OneFTfJP at Epernay
Invited Talk - JayHorn: A Java Model Checker
Philipp Ruemmer Uppsala University
CallƐ: An Effect System for Method Calls
Isaac Oscar Gariano , James Noble Victoria University of Wellington, Marco Servetto Victoria University Wellington, New Zealand