Integration of formal proof into unified assurance cases with Isabelle/SACM

DOI10.1007/s00165-021-00537-4OpenAlexW3088867746MaRDI QIDQ2065527

Mario Gleirscher, Simon Foster, Tim Kelly, Ran Wei, Yakoub Nemouchi

Publication date: 11 January 2022

Published in: Formal Aspects of Computing (Search for Journal in Brave)

Full work available at URL: https://arxiv.org/abs/2009.12154

zbMATH Keywords

proof assistantsintegrated formal methodsassurance casescommon criteriasafety cases

Mathematics Subject Classification ID

Computer science (68-XX)

Uses Software

• Isabelle
• Isabelle/HOL
• Isabelle/jEdit
• Sledgehammer
• Z
• seL4
• Isabelle/UTP
• Archive Formal Proofs
• Isabelle/DOF

Cites Work

• Unnamed Item
• Unnamed Item
• Isabelle/HOL. A proof assistant for higher-order logic
• Unifying theories of time with generalised reactive processes
• Refinement to imperative HOL
• Using the Isabelle ontology framework -- linking the formal with the informal
• Unifying theories of reactive design contracts
• Interaction with formal mathematical documents in Isabelle/PIDE
• Hybrid relations in Isabelle/UTP
• Towards a UTP Semantics for Modelica
• The Tokeneer Experiments
• Automatic Proof and Disproof in Isabelle/HOL
• Unifying Heterogeneous State-Spaces with Lenses
• Building Formal Method Tools in the Isabelle/Isar Framework
• Guarded commands, nondeterminacy and formal derivation of programs
• Proving the Correctness of Multiprocess Programs
• Differential Hoare Logics and Refinement Calculi for Hybrid Systems with Isabelle/HOL
• Combinators for bi-directional tree transformations