Programming Languages and Verification

Programming language is a medium of communication between the user and the computer. Some of the types of programming languages are:

#Assembly language, that lets user view the machine code in an understandable form.

#Compiled language, that are processed by compilers such as C++, BASIC

#Object-oriented language, that contains data and fields that can be accessed and modified in a program.

#Machine language, that computer can directly execute but hard for the user to understand.


To ensure reliability and accuracy of programs that are created with programming languages, different verification techniques needs to be applied, other than simple tests.

There are various methods of verification.

One of them is formal verification. It can be either static or dynamic. The precision of algorithm used in the program are checked using formal methods of Mathematics. It is used in places where proof by exhaustion is seemingly inefficient, such as checking cryptographic protocols, combinational circuits, digital circuits with internal memory and source code

Types of formal verification are:

# Model Checking, where a formal model is built accordingly and its various transitions and states are being assessed. These checking can be done through implementation techniques such as state space enumeration, abstract interpretation and symbolic simulation. Problem with such approach is that it cannot be applied to huge programming systems.

#Deductive verification, where the program is reviewed first and the number of specifications of the program is identified. The derived mathematical proof obligations are given as input to the theorem provers such as automatic theorem provers and satisfiability modulo theories solvers. In case the proof obligations turn out to be true, this will imply that the program is working correctly in the provided specifications


#What is the most efficient form of verification?

#Why can't verification be applied to apps before release in markets?

Useful links below:

Understanding Programming Languages

Effect of Formal Verification on Software Testing

Types of programming languages