Write a Blog >>
ECOOP 2021
Sun 11 - Sat 17 July 2021 Online
co-located with ECOOP and ISSTA 2021
Tue 13 Jul 2021 15:35 - 16:05 at FTfJP - FTfJP Workshop-1

One of the main factors of the increasing power of deductive verifi- cation tools are modern SMT solvers. Unfortunately, SMT solvers usually do not produce proof artifacts that could be inspected or checked. KeY is a formal platform for the deductive verification of Java programs which produces explicit, browsable proofs. SMT solvers can be driven from within KeY, but this unfortunately breaks these proof transparency intentions. In this paper, we describe how we integrated a translation of proof obligations to Z3 (There …) with the replay of proof transcripts reported by Z3 inside KeY (… and Back Again). We describe the conceptual and the engineering challenges we encountered for this round trip and present solutions for them. The replay technique has been implemented in KeY, and in the evaluation, we demonstrate the feasibility of the approach for first- order proof instances and investigate the effects of proof replay on the proof run time and size.

Reconstructing Z3 Proofs in KeY: There and Back Again (FTfJP_slides_Wolfram_Pfeifer_Reconstructing_Z3_Proofs.pdf)1.22MiB

Tue 13 Jul

Displayed time zone: Brussels, Copenhagen, Madrid, Paris change

14:00 - 16:35
FTfJP Workshop-1FTfJP at FTfJP
14:00
5m
Talk
Welcome
FTfJP

14:05
30m
Talk
Refactoring traces to identify concurrency improvements
FTfJP
P: Indigo Orton University of Cambridge, UK, Alan Mycroft University of Cambridge, UK
14:35
30m
Talk
A Generic Type System for Featherweight Java
FTfJP
Ulrich Schöpp fortiss GmbH, P: Chuangjie Xu fortiss GmbH
15:05
30m
Talk
Source code patches from dynamic analysis
FTfJP
P: Indigo Orton University of Cambridge, UK, Alan Mycroft University of Cambridge, UK
15:35
30m
Talk
Reconstructing Z3 Proofs in KeY: There and Back Again
FTfJP
P: Wolfram Pfeifer Karlsruhe Institute of Technology (KIT), Jonas Schiffl , Mattias Ulbrich Karlsruhe Institute of Technology
File Attached
16:05
30m
Talk
Using Dafny to Solve the VerifyThis 2021 Challenges
FTfJP
P: Marie Farrell University of Liverpool, Rosemary Monahan National University of Ireland, A: Conor Reynolds Maynooth University