How does automated verification of systems with infinitely many states work?

I need some help with basic definitions and intuition to understand why and how it's possible to verify systems with infinitely many states.

For example, if I consider an x86 computer, and assuming the CPU architecture is a large and finite state machine, it will have infinitely ($\aleph_0$) many possible states (sequences) it can run, so how can systems with infinitely many states be theoretically verified at all?

Infinite-state system verification is indeed a rather broad topic. First of all, all computers used nowadays can only have a finite number of states, as the amount of RAM is fixed. But that's is mainly a matter of terminology -- any verification technique that needs to iterate over all possible states is doomed from the beginning due to computation time.

Also note that you used "verification" in your title, and "to validate" in your question. These are different concepts that should not be confused. I will assume that you meant "verification".

To solve a verification problem with a large number of states, one typically constructs a proof of correctness of some sort. Such proofs do not need to refer to all possible states, rather they group sets of states by constraints that they satisfy. The description of the constraints can indeed by small, so that in the end we get a small proof.

For example consider the following function:

int comp(int parameter) {
    int p=parameter;
    if (p<0) {
        return p*p;
    } else {
        return p;
    }
}

We want to verify that the function comp never returns a negative number. If "int" is an arbitrary-length integer datatype, this program can already have an infinite number of states. To verify this program, we can perform a case split on whether "parameter" is negative or not, and then apply basic mathematical rules that we assume the integer data type to follow. What we get is a small correctness proof for an infinite-state system.

When researchers say that they work on infinite-state verification, they typically mean that they work of verifying systems in some type of modelling framework that allows to express systems with an infinite number of states - this does not mean that they can verify arbitrary such systems and their techniques are typically sound, but not complete.

StackExchange Computer Science Q#88081, answer score: 9