US 12,190,131 B2
Method and system for function call and variable access based relaxed backward slicing
Priyanka Darke, Pune (IN); Shrawan Kumar, Pune (IN); Venkatesh Ramanathan, Pune (IN); and Sakshi Agrawal, Pune (IN)
Assigned to TATA CONSULTANCY SERVICES LIMITED, Mumbai (IN)
Filed by Tata Consultancy Services Limited, Mumbai (IN)
Filed on Mar. 11, 2022, as Appl. No. 17/654,427.
Claims priority of application No. 202121013172 (IN), filed on Mar. 25, 2021.
Prior Publication US 2022/0342680 A1, Oct. 27, 2022
Int. Cl. G06F 9/445 (2018.01)
CPC G06F 9/44589 (2013.01) 18 Claims
OG exemplary drawing
 
1. A processor implemented method comprising:
receiving, via one or more hardware processors, an input program, a source code having an entry function, wherein the entry function comprises (i) a set of distinct function calls called directly from the entry function and (ii) a set of global variables accessible in the entry function;
generating, via the one or more hardware processors, a set of partitions corresponding to the entry function based on a slicing criteria, wherein each partition of the set of partitions comprises one or more functions satisfying the slicing criteria;
generating, via the one or more hardware processors, a set of slice points for each of the partition of the set of partitions based on (i) control and data flow information of the entry function and (ii) one or more distinct function calls in the entry function of the set of distinct function calls corresponding to the one or more functions in the corresponding partition;
generating, via the one or more hardware processors, a set of program slices with respect to the entry function, wherein each program slice corresponds to at most one set of slice points corresponding to the respective partition;
generating, via the one or more hardware processors, a verification result for each program slice of the set of program slices using a verifier tool; and
composing, via the one or more hardware processors, a verification result of the input program based on the generated verification result for each program slice.