International Journal of Recent Trends in Engineering & Research

online ISSN

DYNAMATE : Automatic Checking loop invariants using Mutation, Dynamic Analysis and static checking

Publication Date : 12/04/2016

Author(s) :

p.sasidhar reddy , c.silpa.

Volume/Issue :
Volume 2
Issue 4
(04 - 2016)

Abstract :

Automatic program verification, proving program correct still requires substantial expert manual effort. One of the biggest burden is providing loop invariants properties that hold for every iteration of a loop. Compared to other requirement elements such as pre -and post conditions, loop invariants tend to be difficult to understand and to express. The proposed system automates the functional verification of incomplete correctness of programs with loops by inferring the required loop invariants. In this approach it combines complementary techniques such as test case generation, dynamic invariant detection, and static verification. This approach can be implemented by a tool called DYNAMATE. DYNAMATE improves the flexibility of loop invariant inference by combining static (proving) and dynamic (testing) techniques. The DYNAMATE tool presented in this process combines different techniques with the overall goal of providing fully automatic verification of programs with loops

No. of Downloads :