Validating safety arguments with Lean

DOI10.1007/978-3-030-92124-8_2MaRDI QIDQ6041273zbMATH OpenOpenAlexFDO

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

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)

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

Cites work

• A formally verified compiler back-end
• Formal verification of parallel programs
• The Lean theorem prover (system description)

Cited in

(2)

• Evolution of Formal Model-Based Assurance Cases for Autonomous Robots
• 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)