Turing award received a method of logical verification of program code

Edmund Clarke, Allen Emerson and Joseph Siphakis, the creators of the model checking program, used to test whether This logical structure (program or "iron") is a model of this formula. The program code is analyzed to determine how it fits into the general requirements for system design.

The method was originally developed as part of a purely theoretical study, but soon found wide practical application in the development of complex integrated circuits, communication protocols, device drivers, digital controllers, etc. According to experts, the present potential of the invention is not yet fully realized.

The Turing Prize is an analogue of the Nobel Prize, but for computer scientists. As it is known, Nobel who lived a hundred years ago did not like mathematicians, therefore he forbade them to give the award to his name. Computer science as a science did not exist at that time, so in 1966, it was necessary to invent something similar, the first winner was Alan Perlis, the creator of the first compilers. The Turing Prize in the amount of $ 250 thousand is awarded by the decision of the Association of Computing Machinery (ACM). The prize is sponsored by Google and Intel.
')
via The Association for Computing Machinery