随着因特网的发展和计算机的普及，软硬件的发展给人们提供了各种便利高效的手段。“软件危机”出现以来，软件的正确性是人们非常重视的一个问题，计算机领域的科学家们也对如何正确的开发和验证软件进行了一系列研
究，其中，软件的形式化验证被称为解决“软件危机”的重要手段。

With the universal of the Internet and the proliferation of computers, the development of hardware and software provide people with a variety of convenient and efficient means. Since the emergence of ”Software crisis”, program correctness is an issue that people take very seriously. The scientists also study how to properly develop and validate software. Among a series of studies, the formal verification of software is known as an important mean to solve the ”software crisis”.
In the formal verification, the current study is mainly based on the Hoare logic. One of the most complex problem in formal verification is loop invariant generation. Many scientists have proposed a variety of solutions to solve it. This paper mainly studies the formula learning based approach in loop invariant derivation, which was a relatively new idea in recent years.
1. Give a systematic summary of the important basic theory of the formal verification. This article describes the important basis for structured programs’verification, which are axiomatic semantics and Hoare logic, as well as the significance and analyse of the loop invariant.
2. Analysis of the core algorithm in the formula learning based derivation of loop invariant,which is the boolean function learning algorithm CDNF.Propose two improved boolean function learning algorithm using minterm theory, and implement the new two algorithms and the original algorithm. We use the abstracted loop invariants to experiment them, and analyse the impact factors to the boolean function learning algorithm. And what’s more, we verify the correctness and higher efficiency of the improved algorithm.
3. Summarize the frame of the function learning based loop invariant derivation algorithm. Describe predicate abstraction techniques, static analysis technology and SMT solving techniques,which were used in the frame. And analyse the algorithm for converting various parts of the joints.
4. Put forward our own learning algorithm using improved boolean function learning algorithm in the loop invariant derivation. we describe how to apply the design in detail, analysis of the feasibility and design tools and methods needed in the improve the algorithm. Lastly ,we verify high portability of the improved boolean function learning algorithm.And analyze the advantages and disadvantages of algorithmic learning based invariant derivation.