Tata Consultancy Services Limited

Priyanka Darke

Venkatesh Ramanathan

Bharti Chimdyalwar

Shrawan Singh Kumar

Ulka Shrotri

Tanha Shah

Tukaram Bhagwat Muske

Venkatesh R

Advaita Datar

Asia Akhtar

Punit Shah

Mohammad Afzal

Vijay Suman Pasupuleti

Avriti Chauhan

Prasad Bokil

Sakshi Agrawal

This disclosure relates generally to the field of program slicing, and, more particularly, to a method and system for function call and variable access based relaxed backward slicing. The method discloses a slicing criterion which focuses only on functions called from an entry function. The slicing criteria uses control and data flow information to slice the given entry function with respect to functions called from the body of the entry function and eventually remove all functions not called directly or indirectly from the entry function. The variables modified by calls in the entry function are considered through side-effect while identifying control and data dependence chain within body of entry function. The proposed technique identifies partitions of functions based on the variables accessible in and functions called from the entry function. Thus, unrelated sets of functions with respect to the entry function are computed and divided into different partitions.

Method and system for function call and variable access based relaxed backward slicing

A system and a method for verification of a source code are provided. There as many techniques available that can be used for verification of software codes, however, it is difficult to determine appropriate technique that can be utilized for verification of a given software code. In an embodiment, the system receives a source code encoded with one or more specifications to be verified. A static analysis of the source code is performed to identify program features of the source code. The program features may include, but are not limited to, multiple return paths, loops with an unstructured control flow, loops with arrays, short ranges and numerical loops. Based on the identification of the program features, verification techniques are applied to the source code for the verification. Each verification technique of the one or more verification techniques is applied for a predetermined period of time and in a predefined order.

System and method for software verification

Software verification is a vital process to ensure reliability and robustness of software systems. The software verification is associated with verifying one or more properties associated with a piece of code. Conventional methods are unable to verify properties of piece of code with loops, especially in the presence of loops with a large, unknown or infinite bound, or a large number of complex conditions. The system receives an abstracted piece of code corresponding to an original piece of code to check whether the abstracted piece of code hence the original piece of code is safe or not. The system applies model checking over the abstracted piece of code to check one or more property assertions associated with an abstracted piece of code. If the property assertion fails in model checking, a trace leading to the violation of the one or more property assertions is identified and analyzed.

Method and system for counter example guided loop abstraction refinement

This disclosure relates generally to method and system for verifying properties of source code. Verifying sufficient subset of properties by identifying implication relations between their verification outcomes is time consuming because of increased size of source code with large number of properties. The proposed disclosure processes the received source code for verifying properties by analyzing the source code to merge the plurality of properties into a plurality of groups based on a grouping technique. Then, slice for each group among the plurality of groups are created. Further, each slice created for each group is verified; verification for the one or more properties within each group is performed simultaneously. The system groups the properties thereby providing efficient and scalable system for verifying properties which reduces cost with increased efficiency and improved performance.

Method and system for verifying properties of source code

Loop abstraction includes determining an original loop within the source code. The original loop includes a control statement and a loop body such that the original loop causes the loop body to be repeatedly executed based on the control statement. Further, output variables in the original loop and a number of blocks associated with the original loop are identified. The number of blocks is indicative of a count of unconditionally executed statement sets in which at least one output variable is computed. An abstract loop corresponding to the original loop is generated by adding a modified expression for accelerated assignment for each output variable in a subset of the output variables, and replacing the control statement with a bounded control statement. The original loop is replaced with the abstract loop for generating an abstract source code for the model checking.

Loop abstraction for model checking

An automated system and method for test data generation for software testing. The present application relates to management of software testing by generating test data automatically. Further the system and method generate test data automatically with respect to two coverage criteria Boundary Value Coverage (BVC) and Masking Boundary Value Coverage (MBVC) in the white-box setting.

Growing community of inventors

Pune, India

Priyanka Darke