Method and system for source code verification using machine learning based strategy prediction

A system for source code verification, comprising:

• a memory storing instructions;
• one or more communication interfaces;
• and
• one or more hardware processors coupled to the memory via the one or more communication interfaces, wherein the one or more hardware processors are configured by the instructions to:
• receive a source code further comprising a plurality of function properties to be verified;
• slice by using at least one sequence slicer among a plurality of sequence slicers, the source code into a plurality of slices, wherein the sequence slicer includes of a slice analyzer and a shallow slicer, wherein the slicer analyzer performs a scalable slicing of the source code with respect to calls in an entry function main and the shallow slicer slices the source code and allows multiple calls in the entry function main corresponding to a global variable and transitively invokes same entry function;
• extract by a feature vector generator a plurality of feature vectors from each slice among the plurality of slices based on a true boolean value, a false boolean value and a plurality of boolean features, wherein each of the plurality of feature vectors indicates syntax and semantics of the source code;
• generate by a neural network a plurality likelihood of success values by applying a plurality of verification techniques over each feature vector among the plurality of feature vectors, wherein an input node in the neural network represents each feature vector, and an output node represents a likelihood of success value generated of each verification technique corresponding to the input node, wherein the neural network includes three layers including a first layer with a first predefined number of neurons, a second layer with a second predefined number of neurons and a third layer with a third predefined number of neurons, and trained using a rectified linear unit (Relu), softmax activation functions and a mean-squared-error loss function,
• wherein the neural network translates an input feature vector representing the source code into a plurality of likelihood of success values li, 1≤i≤10 of a corresponding verification technique in a verification portfolio on the source code, and each output node ni of the neural network represents one verification technique Ti and corresponding likelihood of success value li generated by the neural network at that node ni is the likelihood of success of the corresponding verification technique Ti;
• predict a verification strategy by the neural network by sorting the plurality of likelihood of success values of each verification technique corresponding to each feature vector in decreasing order and applying the verification strategy over each slice to be verified;
• and
• display a verification result as one of a verification successful(S) when each slice is successfully verified by the verification strategy, a verification failure (F) when each slice is verified by the verification strategy and at least one of the plurality of function properties fails in each slice, and an unknown (U) when each slice is not verified for the verification strategy run out of time or memory.

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

• receiving a source code further comprising a plurality of function properties to be verified;
• slicing by using at least one sequence slicer among a plurality of sequence slicers, the source code into a plurality of slices, wherein the sequence slicer includes of a slice analyzer and a shallow slicer, wherein the slicer analyzer performs a scalable slicing of the source code with respect to calls in an entry function main and the shallow slicer slices the source code and allows multiple calls in the entry function main corresponding to a global variable and transitively invokes same entry function;
• extracting by a feature vector generator, a plurality of feature vectors from each slice among the plurality of slices based on a true boolean value, a false boolean value and a plurality of boolean features, wherein each of the plurality of feature vectors indicates syntax and semantics of the source code;
• generating by a neural network, a plurality likelihood of success values by applying a plurality of verification techniques over each feature vector among the plurality of feature vectors, wherein an input node in the neural network represents each feature vector, and an output node represents a likelihood of success value generated of each verification technique corresponding to the input node, wherein the neural network includes three layers including a first layer with a first predefined number of neurons, a second layer with a second predefined number of neurons and a third layer with a third predefined number of neurons, and trained using a rectified linear unit (Relu), softmax activation functions and a mean-squared-error loss function,
• wherein the neural network translates an input feature vector representing the source code into a plurality of likelihood of success values li, 1≤i≤10 of a corresponding verification technique in a verification portfolio on the source code, and each output node ni of the neural network represents one verification technique Ti and corresponding likelihood of success value li generated by the neural network at that node ni is the likelihood of success of the corresponding verification technique Ti;
• predicting a verification strategy by the neural network, by sorting the plurality of likelihood of success values of each verification technique corresponding to each feature vector in decreasing order and applying the verification strategy over each slice to be verified;
• and
• displaying a verification result as one of a verification successful(S) when each slice is successfully verified by the verification strategy, a verification failure (F) when each slice is verified by the verification strategy and at least one of the plurality of function properties fails in each slice, and an unknown (U) when each slice is not verified for the verification strategy run out of time or memory.