Title
Validating Safety Arguments with Lean
Abstract
Safety Assurance Cases (ACs) are structured arguments which demonstrate that a system fulfills its safety requirements. However, the reasoning used in ACs is often presented informally and thus difficult to rigorously evaluate. To protect against the acceptance of ACs based on fallacious reasoning, our previous work has proposed a framework for formalizing fragments of ACs and verifying their reasoning using the Lean Theorem Prover. This work expands on the use of Lean to automatically validate fragments of ACs, identifies challenges faced by AC developers who wish the leverage theorem proving software, and demonstrates our approach to mitigating these challenges.
Year
DOI
Venue
2021
10.1007/978-3-030-92124-8_2
SOFTWARE ENGINEERING AND FORMAL METHODS (SEFM 2021)
Keywords
DocType
Volume
Assurance, Safety cases, Strategies, Theorem proving, Lean
Conference
13085
ISSN
Citations 
PageRank 
0302-9743
0
0.34
References 
Authors
0
5
Name
Order
Citations
PageRank
Logan Murphy100.34
Torin Viger202.37
Alessio Di Sandro31167.84
Ramy Shahin400.34
Marsha Chechik500.34