What types of string properties are verifiable in polynomial time?
Verifying a property of strings over an alphabet $\Sigma$ is precisely the same problem as checking whether a string is part of a language, called the Entscheidungsproblem or decision problem.

Language : $\Sigma^* \mapsto \{0,1\}$

What you are interested in are 'properties of strings' or in other words 'classes of languages'.

The class you are probably looking for is 'P', which contains all languages for which the decision problem can be solved in polynomial time on a deterministic Turing machine. Interestingly this class is the same as the class of languages for which the decision problem can be solved by polynomial circuits.

All C programs which contain constantly bounded loops belong to P for example (they can easily be turned into a polynomial circuit).
From there you can extend the language to include other loops that terminate in polynomial time. You have to be careful with nested loops. There are special Hoare-type logics for this purpose.