Research On Generation Of Loop Invariants

Software has been used widely in various areas as the carrier of information systems. Any vulnerability or incorrect development in software will cause highly serious failures. It can increase the confidence with enough testing which will be very expensive. Unfortunately, it still cannot guarantee that the software to be tested is fully reliability even with lots of testing. Formal methods are based on strict mathematically and logically basis. It can ensure that the software meets its given specifications through proving of correctness, which greatly improves the reliability of software.A key issue in program proving is finding sufficient loop invariants to assist the automatic process. However, writing loop invariants manually is boring and error-prone. Thus, the research on how to analysis and generate loop invariants automatically becomes an important issue in the area of formal methods. This dissertation focused on the generation of loop invariants and mainly covers the subjects of theory of formal methods and generation technologies for invariants.(1)We summarized the main theories of formal methods to analysis programs. It is focused on the core theory, the main problem to resolve and classical tools. Then we point out the difficulty of formal proof.(2) We summarized recent research and common technologies for generating loop invariants. They are described and compared from many aspects, including the kinds of programs to be analyzed, the way how they work and their shortcomings.(3) Based on conditional assignment and adaptive template an approach to generate invariants is proposed in this dissertation. Many semantic factors are considiered here, not only loop itself but also specifications, asserts etc.. It infers potential loop invariants according to CFG, PDG and value analysis which are then resolved by theory prover. It can run automatically and insert invariants as ACSL comments into C codes as output.(4)Based on the method above, a plugin named looplnv is designed and implemented with the platform Frama-C and APRON. According to the experiments on some selected programs, it can generate more invariants comparing with other tools and most of the programs can be proved successfully.