A simpler explanation:
Taking a note from Feynman, I want to use less jargon. I understand that
it is useful, and that there are a lot of interesting distinctions that it
can draw, and that it can dramatically improve communication between two
people who speak it. But I think it also removes the knowledge, even in
our own heads, from reality... simple things becomes complex, even when
they are not. Thus this is an attempt to explain my research in simple
terms, without in any way sacrificing correctness.
I am working with tools that can prove things about programs. However, in
general it is impossible to reason about programs in any meaningful way.
They are just too complex. Thus we use flowcharts to describe the behavior
of a program. These flowcharts are called automata (singular automaton).
We can use these flowcharts both to describe programs, and also to
describe properties we want programs to have. Such properties might be
safety properties, saying that the program never enters a bad state, or
fairness properties, saying that the program eventually responds to an
input.
We are often interested in describing possibly infinite behaviors, like
termination or how programs communicate over a network. To do this, we use
flowcharts that loop back on themselves, so you don't always reach an end.
One category of these flowcharts over infinite behaviors are Buechi
automata.
If we have an automaton that specifies a property, it is natural to check
that a program satisfies this property. In order to do this, we have to
create the complement of the property automaton. This complement describes
exactly the behaviors that are prohibited by the property. If the property
automaton requires that the program never goes to a bad state, the
complement of the property automaton describes every possible way the
program could go to a bad state. Once we have the complement, we can look
for some program behavior that is described by the complement. This is a
counterexample to the correctness of the program. Because the complement
describes /every/ way the program could go bad, if we can't find a
counterexample, we can be sure that the program is correct... at least
with respect to this specific property.
Looking for this counterexample is called testing containment, as we are
seeing if the behaviors described by one automaton (the program) are
contained in the behaviors described by another automaton (the
property).
Comments and suggestions on this effort are greatly welcome! Contact me at
rice.edu or gmail.com.