Validating safety arguments with Lean

DOI10.1007/978-3-030-92124-8_2zbMath1522.68337OpenAlexW4206207168MaRDI QIDQ6041273

Marsha Chechik, Ramy Shahin, Alessio Di Sandro, Logan Murphy, Torin Viger

Publication date: 26 May 2023

Published in: Software Engineering and Formal Methods (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1007/978-3-030-92124-8_2

zbMATH Keywords

theorem provingstrategiesassuranceLeansafety cases

Mathematics Subject Classification ID

Specification and verification (program logics, model checking, etc.) (68Q60) Models and methods for concurrent and distributed computing (process algebras, bisimulation, transition nets, etc.) (68Q85) Theorem proving (automated and interactive theorem provers, deduction, resolution, etc.) (68V15)

Cites Work

• A formally verified compiler back-end
• The Lean Theorem Prover (System Description)
• Formal verification of parallel programs

This page was built for publication: Validating safety arguments with Lean