Patent ID: 8996435
Filing Date: 2015-03-31
Classification: G06F,G06N

Abstract:
1. A computer-implemented method performed by a computerized device, comprising: obtaining a set of candidates of invariants with respect to a model, the model comprising a transition relation axiom and an initial axiom, wherein states of the model are represented by values of variables, wherein the transition relation axiom and the initial axiom are defined over the variables, wherein the transition relation axiom defines values of the variables in a cycle based on values of the variables in a previous cycle, wherein the initial axiom defines values of the variables at an initial cycle; for each candidate, adding to the model a first auxiliary variable, thereby increasing the number of bits used to represent each state of the model, and modifying the transition relation axiom to define a value of the first auxiliary variable as being implied from the candidate being held in a predetermined cycle, wherein said adding is performed by a computer; and iteratively trying to prove an inductive step with respect to a subset of the candidates, wherein in response to determining that a candidate is not held inductively removing the candidate from the subset of the candidates, wherein determining that the candidate is not held inductively is performed based on values of the first auxiliary variables, wherein said iteratively trying to prove is performed by the computer.