All entries for November 2005
November 23, 2005
In 1986, Moshe Vardi wrote a paper with P. Wolper on automata theoretic approach to automatic program verification in which authors suggested that program verification can be explained as an automata theoretic activity where we are interested in checking wheter intersection of two automata (program M and negation of specification P) is empty. If the intersection is empty, it implies that program satisfies the specification, otherwise, in case of intersection being not empty, a lasso shaped trace is found which represents the infinite behavious of the system which do not adhere to system specification. This lasso shaped trace is then used for counterexample generation.
In short following statements are equal:
1. Implementation M satisfy the specification P.
2. Specification P characterizes all the traces produced by M, and possibly some more.
3. Comp(M) –> Comp(P)
4. M intersection (not P) = null set
Just now I was thinking about it and came up with the term — catching bugs with a lasso as in fact it exactly does the same. So If I would have to write a paper on that idea, I would have given it the name — "Catching bugs with a Lasso." :)
 Moshe Y. Vardi, Pierre Wolper: An Automata–Theoretic Approach to Automatic Program Verification (Preliminary Report) LICS 1986: 332–344
November 01, 2005
I wish you all a very happy Diwali and a prosperous new year.