Method and system for counter example guided loop abstraction refinement

A system (100) comprising:

• at least one memory (104) storing programmed instructions;
• one or more Input/Output (I/O) interfaces (112);
• and one or more hardware processors (102) operatively coupled to the at least one memory (104), wherein the one or more hardware processors (102) are configured by the programmed instructions to:
• receive an abstracted piece of code corresponding to an original piece of code, wherein the abstracted piece of code comprises a plurality of base cases and inductive steps, wherein the inductive steps corresponds to a plurality of abstracted loops associated with the abstracted piece of code, and wherein each of the plurality of base cases and inductive steps are associated with a first set of property assertions to be verified;
• simultaneously perform a bounded model checking on the abstracted piece of code to verify a property assertion from the first set of property assertions corresponding to a base case from the plurality of base cases and inductive steps, wherein the abstracted piece of code is safe when the property assertion holds for the base case and inductive steps;
• and
• refine the abstracted piece of code when the abstracted piece of code is unsafe corresponding to the inductive steps until all causes leading to violation of a plurality of property assertions are analyzed, comprising:
• obtaining an error trace in the abstraction using bounded model checking, wherein the error trace comprises a violation causing path corresponding to the property assertion from the first set of property assertions in the abstraction;
• checking validity of the error trace on the original piece of code by utilizing a verification technique to obtain one of a valid error trace and an invalid error trace;
• identifying a plurality of trace conditions, corresponding to the body of the plurality of abstracted loops by using the error trace, when the invalid error trace is obtained, wherein the plurality of trace conditions comprises a subset of conditions evaluated to true in the error trace;
• negating the plurality of trace conditions to obtain a second set of property assertions;
• obtaining the plurality of property assertions by performing a union of the first set of property assertions and one or more property assertions from the second set of property assertions;
• further refining of the abstraction based on the plurality of property assertions by annotating the property assertions into the original piece of code and applying loop abstraction using induction technique to obtain a refined abstracted piece of code;
• and
• bounded model checking of the refined abstracted piece of code to check whether the piece of code is safe.

One or more non-transitory machine readable information storage mediums comprising one or more instructions which when executed by one or more hardware processors causes:

• receiving, by one or more hardware processors, an abstracted piece of code corresponding to an original piece of code, wherein the abstracted piece of code comprises a plurality of base cases and inductive steps, wherein the inductive steps corresponds to a plurality of abstracted loops associated with the abstracted piece of code, and wherein each of the plurality of base cases and inductive steps are associated with a first set of property assertions to be verified;
• simultaneously performing, by the one or more hardware processors, a bounded model checking on the abstracted piece of code to verify a property assertion from the first set of property assertions corresponding to a base case from the plurality of base cases and the inductive steps, wherein the abstracted piece of code is safe when the property assertion holds for the base case and inductive steps;
• refining, by the one or more hardware processors, the abstracted piece of code when the abstracted piece of code is unsafe corresponding to the inductive steps until all causes leading to violation of a plurality of property assertions are analyzed, comprising:
• obtaining an error trace in the abstraction using bounded model checking, wherein the error trace comprises a violation causing path corresponding to the property assertion from the first set of property assertions in the abstraction;
• checking validity of the error trace on the original piece of code by utilizing a verification technique to obtain one of a valid error trace and an invalid error trace;
• identifying a plurality of trace conditions, corresponding to the body of the plurality of abstracted loops by using the error trace, when the invalid error trace is obtained, wherein the plurality of trace conditions comprises a subset of conditions evaluated to true in the error trace;
• negating the plurality of trace conditions to obtain a second set of property assertions;
• obtaining the plurality of property assertions by performing a union of the first set of property assertions and one or more property assertions from the second set of property assertions;
• further refining of the abstraction based on the plurality of property assertions by annotating the property assertions into the original piece of code and applying loop abstraction using induction technique to obtain a refined abstracted piece of code;
• and
• bounded model checking of the refined abstracted piece of code to check whether the piece of code is safe.