Symbolic model checking with dynamic model pruning

A computer software product having one or more recordable medium having executable instructions stored thereon which, when executed by a processing device, causes the processing device to:

• receive a first state machine property to evaluate;
• generate, from the first state machine property, a first assumption including a first state predicate;
• generate a reduced next state function from a first next state function involving the first state predicate by applying the first assumption;
• produce, for a model, a transition relation that includes the reduced next state function;
• and
• propagate the first assumption according to a second state machine property to generate a second assumption.

A method comprising:

• producing, from a first property, a first assumption including a first state predicate;
• producing a reduced next state function from a first next state function involving the first state predicate by applying the first assumption;
• producing, for a model, a transition relation that includes the reduced next state function;
• and
• propagating the first assumption according to a second property to generate a second assumption.

A verification system comprising:

• means for producing, from a first property, a first assumption including a first state predicate;
• means for producing a reduced next state function from a first next state function involving the first state predicate by applying the first assumption;
• means for propagating the first assumption according to a second property to generate a second assumption;
• and
• means for producing, for a model, a transition relation that includes the reduced next state function.

A verification system comprising:

• a recordable medium to store executable instructions;
• a processing device to execute executable instruction;
• and
• a plurality of executable instructions to cause the processing device to:
• produce, from a first property, a first assumption including a first state predicate;
• produce, for a model, a first transition relation that includes the first state predicate;
• reduce the first transition relation according to the first assumption;
• and
• propagate the first assumption to generate a second assumption according to a second state predicate.