Mon 15 Jul 2019 16:45 - 17:00 at Epernay - Session Three

Through an example about linked lists we show how a sequential program with classes can be translated to first-order logic independent of loop invariants.

Mon 15 Jul

Displayed time zone: Belfast change

15:30 - 17:00
Session ThreeFTfJP at Epernay
15:30
30m
Full-paper
Towards Deductive Verification of C11 Programs with Event-B and ProB
FTfJP
Sadegh Dalvandi University of Surrey, Brijesh Dongol University of Surrey
16:00
30m
Full-paper
Specifying I/O using Abstract Nested Hoare Triples in Separation Logic
FTfJP
Willem Penninckx KU Leuven, Amin Timany imec-Distrinet KU-Leuven, Bart Jacobs KU Leuven
16:30
15m
Short-paper
Analysis of MiniJava Programs via Translation to ML
FTfJP
Martin Lester University of Reading
16:45
15m
Short-paper
Translating Classes to First-Order Logic: An Example
FTfJP