Formal verification or formal proof - formal proof of conformity or non-conformity of a formal subject of verification with its formal description. The subject matter is algorithms, programs, and other evidence.
Due to the routine of even simple formal verification and the theoretical possibility of their full automation, formal verification usually means automatic verification using a program .
Content
- 1 Justification
- 2 Applications
- 3 Theoretical background
- 4 Approaches to formal verification
- 5 Evidence-based programming
- 6 Automatic proof verification
- 7 See also
- 8 Literature
Justification
Software testing cannot prove that a system, algorithm or program does not contain any errors and defects and satisfies a certain property. Formal verification can do this.
Applications
Formal verification can be used to verify systems such as software presented in the form of source codes, cryptographic protocols , combinatorial logic circuits , digital circuits with internal memory.
Theoretical Foundations
Verification is a formal proof on an abstract mathematical model of the system, under the assumption that the correspondence between the mathematical model and the nature of the system is considered to be initially given. For example, to build a model or mathematical analysis and proof of the correctness of algorithms and programs.
Examples of mathematical objects often used for modeling and formal verification of programs and systems are:
- formal semantics of programming languages, for example , , ( Hoar logic ), mathematical semantics of programs
- type theories and systems - first of all, systems with dependent types (see lambda cube )
- separation logic (extension of Hoar logic)
- state machine
- labeled state and transition model
- Petri net
- temporary machine
- hybrid machine
- process calculus
- structured algorithms
- structured programs
Formal Verification Approaches
The following approaches to formal verification exist:
- formal semantics of programming languages
- writing programs that are correct in construction (see dependent type , lambda cube , )
- model checking
- logical inference
- symbolic execution
- abstract interpretation
- systematic analysis of algorithms and programs
- evidence-based programming technologies
Evidence Based Programming
Evidence-based programming - a technology used in academic circles in the development of computer programs in the 1980s with evidence of correctness - evidence of the absence of errors in programs (understanding, within the framework of this theory, errors as inconsistencies between the program and the algorithm it implements).
Automatic proof verification
The proof can be fully automated only for a very small circle of simple theories, therefore, its automatic verification and, for this, the transformation to the verified form are important.
To maintain rigor when verifying evidence, the verifier should also verify the verifier, which requires another verifier, and so on. The resulting endless chain of verifiers could be minimized by constructing a verifier verifying itself, which has the ability to turn around to be applicable in practice.
See also
- Formal verification of cryptographic protocols
- Contract programming
- Logic of Hoar
- Software testing
- Security through language ( English Language-based security )
Literature
- P. Grogono, Programming in Pascal, M.: Mir, 1982, p.295, (Testing and verification).