FACTum is a framework to support the verification of component-based systems combining model checking and interactive theorem proving. In FACTum, the verification of overall system properties is split into two steps: First, suitable contracts are specified for the components (represented by gray boxes) and verified against their implementation. Since single components are usually of limited complexity, this step can be fully automated using model checking techniques. In a second step the contracts are combined to verify overall system properties. This step is usually more complex and usually requires manual interaction. Thus, in FACTum, we use interactive theorem proving to reason about the combination of contracts.

Keywords for this software

Anything in here will be replaced on browsers that support the canvas element

References in zbMATH (referenced in 1 article )

Showing result 1 of 1.
Sorted by year (citations)

  1. Marmsoler, Diego; Gidey, Habtom Kashay: Interactive verification of architectural design patterns in FACTum (2019)