First-Order Theorem Proving for Program Analysis and Theory Reasoning

Ioan Dragan

Short abstract:

Analyzing and verifying computer programs is an important and challenging task. Banks, hospitals, companies, organizations and individuals heavily depend on very complex computer systems, such as Internet, networking, online payment systems, and autonomous devices. These systems are integrated in an even more complicated environment, using various computer devices. Technically, software systems rely on software implementing complicated arithmetic and logical operations over the computer memory. If this software is not reliable, the costs to the economy and society can be huge. Software development practices therefore need rigorous methods ensuring that the program behaves as expected.

Formal verification provides a methodology for making reliable and robust systems. This is achieved by using program properties to hold at intermediate points of the program. Using these properties one can prove that program are correct, hence they contain no errors. Providing such properties manually requires a considerable amount of work by highly skilled personnel and makes verification commercially not viable. Formal verification therefore requires non-trivial automation for generating valid program properties, such as loop invariants.

In this talk we present the use of first-order theorem proving for generating and proving program properties. After introducing the method we also present Lingva, a tool designed in order to automatically generate invariants for loops that handle arrays and show experimentally that the generated invariants summarize the intended behavior of the considered loop. Our work is based on the recently introduced symbol elimination method for invariant generation, using a saturation-based first-order theorem prover.