Theorem Proving and SMT Solving

Method Purpose Short description of the method's purpose and main benefits

Method description A detailed description of the method

Produces a formal proof of the correctness of a software system which can be used to provide robust evidence for certification of software systems. Properties verified are typically safety and liveness properties.

Theorem provers may be automatic or interactive, with proof tactics and libraries provided to assist the users. Theorem Provers and SMT solvers are used for verification, proving the correctness of programs, software testing based on symbolic execution, and for synthesis, generating program fragments by searching over the space of possible programs. Theorem provers like Coq, PVS and Isabelle/HOL are proof management systems that provide a formal language to write mathematical formulae and tools for proving these formulae in a logical calculus. Different theorem provers support proofs in different logics, e.g., Keymeara X supports proofs for differential dynamic logic, a logic for specifying and verifying properties of hybrid systems with mixed discrete and continuous dynamics whereas the STeP theorem prover is concerned with invariant conditions. SMT solvers like Z3 support proof strategies through providing theories of arithmetic, fixed-size bit-vectors, extensional arrays, datatypes, uninterpreted functions, and quantifiers which facilitate reasoning. Applications are primarily in extended static checking, test case generation, deductive verification, and predicate abstraction.

Method Strengths A listof the strengths of the method

Provides a formal proof of the system correctness which can be used for robust evidence for certification
Tools provide many proof tactics provided to automate proofs
Approaches available for discrete and continuous dynamics.

Method Limitations The limitations of the method

Often require interaction when proof tactics fail
Specialist knowledge required
Since provers operate on a formal model, there needs to be a separate step to show that the formal model properties actually represent the system properties

Method References Bibliography references to papers about the method.

[TPS1] KeYmaera: a hybrid theorem prover for hybrid systems (system description) A. Platzer and J.-D. Quesel, Automated Reasoning, Springer, Berlin (2008), pp. 171-178

[TPS2] Z. Manna, N. Bjoerner, A. Browne, and E. Chang, STeP: The Stanford Temporal Prover, LNCS, Vol. 915, 1995, pp. 793–794.

[TPS3] A. Rizaldi, J. Keinholz, M. Huber, J. Feldle, F. Immler, M. Althoff, E. Hilgendorf, and T. Nipkow. Formalising and monitoring traffic rules for autonomous vehicles in Isabelle/HOL. volume 10510 of LNCS, pages 50–66. Springer, 2017.

[TPS4] Deductive verification of hybrid systems using step, Z. Manna and H.B. Sipma Hybrid Systems: Computation and Control, Springer, Berlin (1998), pp. 305-318

[TPS5] P. Bagade, A. Banerjee, S.K.S. Gupta, Chapter 12 - Validation, Verification, and Formal Methods for Cyber-Physical Systems, In Intelligent Data-Centric Systems, Cyber-Physical Systems, Academic Press, 2017

[TPS6] A Survey on Theorem Provers in Formal Methods M. Saqib Nawaz, Moin Malik, Yi Li, Meng Sun and M. Ikram Ullah Lali, https://arxiv.org/pdf/1912.03028.pdf

Method Dimensions

Evaluation Environment Type Type of environment where the method is applied. It can be more than one type of environment. (Dimension 1)

Evaluation Type Type of evaluation performed with that method. If a method is hybrid, more than one type can be selected. (Dimension 2)

Type of Component Under Evaluation Type of components that can be evaluated with that method. It can be more than one type. (Dimension 3)

Evaluation Stage The evaluation stage where the method is used. (Dimension 5)

Purpose of the Component Under Evaluation The type of purpose that can be evaluated by a method. It can be more than one type. (Dimension 6)

Type of Requirement Under Evaluation The type of requirements that a method is able to evaluate. It can be more than one type. (Dimension 7)

Evaluation Performance Indicator The type of evaluation criteria or KPI that a method is able to improve. It can be more than one type. (Dimension 8)

Relations

Related Methods A method could be related to other methods.

Tools A method can use zero or more tools.

Part Method A method (when it is a combination: Combination of method artefact that is a specialization of a V&V Method) could be composed of a set of V&V Methods.

Test Case or Verification and Validation activity Test Case or V&V activity performed in a Use Case. We will link to the method to the test cases where the method is used.

Standards A method can be linked with standards.

Context

Workflow

Contents

There are currently no items in this folder.