Deductive Verification

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

Method description A detailed description of the method

Deductive software verification expresses the correctness of the source code as a set of mathematical statements, called verification conditions. A human user typically contributes in two ways:

formalising an informally stated specification for the source code, and
providing (if necessary) guidance to a verification system to show formally the conformance of the source code to the specification.

Properties to be verified are typically expressed in specification languages that combine first-order logic and some theories (arithmetic, sets, arrays, bit vectors) to allow modelling the programming language while still allowing proof automation. These properties are verified in a modular way (e.g. method contracts using the Design by Contract paradigm, loop invariants, class invariants, lemmas, assumptions, assertions) and include both behavioural properties, e.g., calculates the longest repeated substring, and safety properties, e.g., null de-reference, out-of-bounds errors, termination, arithmetic overflow.

Weakest precondition/strongest postcondition calculus proof obligations are then discharged using either automated or interactive theorem provers such as those listed below:

Interactive theorem provers (such as HOL, ACL2, Isabelle, or Coq) where the user is responsible for finding a proof, and in particular for providing values for quantifier instantiations.
Automatic theorem provers where the proof is extracted from the specification, annotations, and the program
Satisfiability Modulo Theories (SMT) solvers (Z3, Yices, Alt-Ergo, CVC3)

Method Strengths A listof the strengths of the method

Used to prove safety and behavioural properties of source code.
Static verification detects runtime errors.
High degree of automation using SMT solvers.
When tools silently infer a particular fact (a termination measure, for instance), it reduces the burden on the user (but may appear as a gap in reasoning to an outsider)

Method Limitations The limitations of the method

Knowledge about the background theory implemented in a tool is often needed to understand a solution.
Some tools require interactive theorem proving such as ghost code or inductive proofs via lemma functions.
Some systems expose an explicit proof object (i.e., a derivation in a certain calculus) and this is typically too fine-grained to communicate easily.
In some systems the user only works with the annotated source code which often does not make the argument structure explicit.

Method References Bibliography references to papers about the method.

[DEV1] Filliâtre, J. Deductive software verification. Int J Software Tools Technology Transfer 13, 397 (2011). https://doi.org/10.1007/s10009-011-0211-0

[DEV2] Hähnle R., Huisman M. (2019) Deductive Software Verification: From Pen-and-Paper Proofs to Industrial Tools. In: Computing and Software Science. LNCS, vol 10000. Springer, Cham. https://doi.org/10.1007/978-3-319-91908-9_1

[DEV3] Towards deductive verification of control algorithms for autonomous marine vehicles S Foster, M Gleirscher, R Calinescu- arXiv preprint arXiv:2006.09233, 2020 - arxiv.org

[DEV4] Luo Z., Siegel S.F. (2018) Symbolic Execution and Deductive Verification Approaches to VerifyThis 2017 Challenges. In: ISoLA 2018. LNCS, vol 11245. Springer, Cham. https://doi.org/10.1007/978-3-030-03421-4_12

[DEV5] Oortwijn W., Huisman M. (2019) Formal Verification of an Industrial Safety-Critical Traffic Tunnel Control System. In: Integrated Formal Methods. IFM 2019. Lecture Notes in Computer Science, vol 11918. Springer, Cham. https://doi.org/10.1007/978-3-030-34968-4_23

[DEV6] Marieke Huisman, Rosemary Monahan, Peter Müller, Andrei Paskevich, Gidon Ernst. VerifyThis 2018: A Program Verification Competition. [Research Report] Université Paris-Saclay.2019

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.