Proving JDK's Dual Pivot Quicksort Correct. - Bernhard Beckert; Jonas Schiffl; Peter H. Schmitt; Mattias Ulbrich (VSTTE, 2017)

Smart Contracts: Application Scenarios for Deductive Program Verification. - Bernhard Beckert; Jonas Schiffl; Mattias Ulbrich (FM Workshops (1), 2019)

Specifying Framing Conditions for Smart Contracts. - Bernhard Beckert; Jonas Schiffl (ISoLA (3), 2020)

Formal Analysis of Smart Contracts: Applying the KeY System. - Jonas Schiffl; Wolfgang Ahrendt; Bernhard Beckert; Richard Bubel (20 Years of KeY, 2020)

Reconstructing z3 proofs in KeY: there and back again. - Wolfram Pfeifer; Jonas Schiffl; Mattias Ulbrich (FTfJP@ECOOP, 2021)

Continuous Secure Software Development and Analysis. - Sophie Schulz; Frederik Reiche; Sebastian Hahner; Jonas Schiffl (SSP, 2021)

Towards Correct Smart Contracts: A Case Study on Formal Verification of Access Control. - Jonas Schiffl; Matthias Grundmann; Marc Leinweber; Oliver Stengele; Sebastian Friebe; Bernhard Beckert (SACMAT, 2021)

Deductive Verification of Floating-Point Java Programs in KeY. - Rosa Abbasi; Jonas Schiffl; Eva Darulova; Mattias Ulbrich; Wolfgang Ahrendt (TACAS (2), 2021)

Static Capability-Based Security for Smart Contracts. - Jonas Schiffl; Alexander Weigl; Bernhard Beckert (DAPPS, 2023)

Are Formal Contracts a Useful Digital Twin of Software Systems? - Jonas Schiffl; Alexander Weigl (FMDT@FM, 2023)

Combining rule- and SMT-based reasoning for verifying floating-point Java programs in KeY. - Rosa Abbasi; Jonas Schiffl; Eva Darulova; Mattias Ulbrich; Wolfgang Ahrendt (Int. J. Softw. Tools Technol. Transf., 2023)

A Practical Notion of Liveness in Smart Contract Applications. - Jonas Schiffl; Bernhard Beckert (FMBC@CAV, 2024)

Scar: Verification-Based Development of Smart Contracts (Tool Paper). - Jonas Schiffl; Bernhard Beckert (FMBC, 2025)