''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.