Translating Scala Programs to Isabelle/HOL

TL;DR

This paper introduces a trustworthy connection between the Leon verification system for Scala and the Isabelle proof assistant, enabling enhanced verification capabilities and confidence in program correctness.

Contribution

It presents a method to translate Scala programs verified in Leon into Isabelle/HOL, combining automated and interactive theorem proving for improved assurance.

Findings

Integration of Leon and Isabelle enhances verification confidence

Allows leveraging Isabelle's rich library for Scala program verification

Facilitates manual proof development with semi-automated tactics

Abstract

We present a trustworthy connection between the Leon verification system and the Isabelle proof assistant. Leon is a system for verifying functional Scala programs. It uses a variety of automated theorem provers (ATPs) to check verification conditions (VCs) stemming from the input program. Isabelle, on the other hand, is an interactive theorem prover used to verify mathematical specifications using its own input language Isabelle/Isar. Users specify (inductive) definitions and write proofs about them manually, albeit with the help of semi-automated tactics. The integration of these two systems allows us to exploit Isabelle's rich standard library and give greater confidence guarantees in the correctness of analysed programs.