String analysis based on three-valued logic

An apparatus comprising:

• a computer readable storage medium storing computer readable program code executable by a processor, the computer readable program code comprising:
• a property translator configured to express a property of a string in a computer software application as a three-valued logic shape predicate;
• a shape analyzer configured to perform a three-valued logic shape analysis using the three-valued shape predicate to reach a fixpoint solution;
• and
• a fixpoint solution evaluator configured to evaluate the fixpoint solution to determine a three-valued logic value of the property, wherein the three-valued logic shape predicate uses a binary successor predicate to enforce order between characters of the string and a unary is-letter [z] predicate template denote a value of each character in the string where z is a letter of the string instantiating the three-valued logic shape predicate.

A computer program product for performing string analysis, the computer program product comprising:

• a non-transitory computer readable storage medium having computer readable program code embodied therein, the computer readable program code configured to:
• express a property of a string in a computer software application as a three-valued logic shape predicate;
• perform a three-valued logic shape analysis using the three-valued shape predicate to reach a fixpoint solution;
• and
• evaluate the fixpoint solution to determine a three-valued logic value of the property, wherein the three-valued logic shape predicate uses a binary successor predicate to enforce order between characters of the string and a unary is-letter [z] predicate template denote a value of each character in the string where z is a letter of the string instantiating the three-valued logic shape predicate.

The method for deploying a computer program product, comprising integrating computer readable program code into a computing system, wherein the code in combination with the computing system performs the following:

• expressing, by use of a processor, a property of a string in a computer software application as a three-valued logic shape predicate;
• performing a three-valued logic shape analysis using the three-valued shape predicate to reach a fixpoint solution;
• and
• evaluating the fixpoint solution to determine a three-valued logic value of the property, wherein the three-valued logic shape predicate uses a binary successor predicate to enforce order between characters of the string and a unary is-letter [z] predicate template to denote a value of each character in the string where z is a letter of the string instantiating the three-valued logic shape predicate.