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
Times are displayed in time zone: Greenwich Mean Time : Belfast change

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