Validating safety arguments with Lean

DOI10.1007/978-3-030-92124-8_2zbMATH Open1522.68337OpenAlexW4206207168MaRDI QIDQ6041273FDOQ6041273

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

Recommendations

• Belief Functions for Safety Arguments Confidence Estimation: A Comparative Study
• Integration of formal proof into unified assurance cases with Isabelle/SACM
• D-S theory for argument confidence assessment
• Safety case confidence propagation based on Dempster-Shafer theory
• scientific article; zbMATH DE number 2087595

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

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

Cited In (1)

• Belief Functions for Safety Arguments Confidence Estimation: A Comparative Study

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

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q6041273)