banner

Menu:

Links:

- LinkedIn Profile
- Studio Berezin Film
- Radical Change Grp.
- Writing the Mind
- Aiki Jujutsu
- 5Rhythms
- Scary Cow
- Deviant Art

What's new:

Dec 24, 2009:
The Devil in The Detail
Released the director's cut online [watch it]

Sep 21, 2009:
My Movie Screening
Oct 4, 3pm at Victoria Theatre, San Francisco [Watch Trailer]

Feb 10, 2009:
Post: Power Plant (Tree)
Electricity-producing trees - next gen solar / wind power sources? [Read post]

Sep 21, 2008:
Post: There is no secret!
Some people make it, and some people don't. What's the secret? [Read post]

July 2, 2008:
Update: no more office phone.
Good-bye Synopsys!

Research Interests

Last updated: Aug 24, 2003

Short Overview

Background / Experience

Research interests

Practical Experience

Combination of Decision Procedures (2001 - 2005)

When I joined the Hardware Verification Group at Stanford in Fall 2001, I discovered for myself a powerful theory for combination of decision procedures, - a research area closely related to my thesis work, only more focused on the decision procedure side rather than model checking or theorem proving. In some sense, in my thesis I only considered one single decision procedure: a model checker, whereas with the combination theory many more decision procedures can be added to a theorem proving engine to enhance its power.

One such engine, the Cooperating Validity Checker, a successor of Stanford Validity Checker, has been developed in this group. I got involved in developing new decision procedures for the tool, adding more features, and cleaning up the code. Eventually, we decided to retire the codebase of CVC and replace it with the third-generation validity checker called CVC Lite. As the name suggests, it is a much lighter implementation of the same framework, with the emphasis placed on code readability and maintainability, clean APIs, and, of course, efficiency. CVC Lite was first publicly released in August 2003.

Combination of Model Checking and Theorem Proving (1998 - 2001)

This was my Ph.D. thesis work, whose primary goal was to bridge model checking with theorem proving. In fact, that's how it has all started: I was trying to come up with an idea of how to make the two mostly disjoint methodologies work together without imposing many restrictions on each other. At some point, I realized that what is holding theorem proving apart from model checking is merely its main data structure: the Gentzen's sequent, the intermediate representation of HOL formulas in the proof. Modifying the sequent to include a model (Kripke structure), and changing the logic from HOL to some temporal logic, possibly first- or higher-order, allows us to introduce model checking transformations as first-class citizens into the new proof system. Every such transformation becomes simply a new inference rule in the new proof system. This was the main idea of a happy marriage of model checking and theorem proving. The actual details of what the proof system is and how it combines the two are in one of my papers (not published yet, ask me, I'll send you a copy). You can also get an idea by reading the SyMP manual. SyMP is my tool that implements such a proof system.

However, the next thing that comes to mind after reading the previous paragraph is the following question: what is the fundamental change that we made to theorem proving that allowed it to be specialized to model checking type of problems? It was the sequent, the logic, and the proof system that needed a change. Then what if our new proof system will not be adequate for some other problem domain, say, security protocol analysis? The answer now should be almost obvious: Find a suitable form of the sequent for this new problem domain, appropriate logic for the properties, and design a proof system on top of them. This prompted the idea of a more general framework, although indecently simple when explained, but amazingly useful in practice.

The framework is the following. Imagine a generic proof system: some sequent comprised of several components that we do not need to know about at the moment, and a proof system consisting of a set of abstract inference rules that somehow can take a current sequent and generate new sequents that, if proven, would imply the validity of the current one. We surely do not need to know more about the proof system to explain how a proof in this system can be constructed: take the initial sequent which is a statement of a theorem we want to prove, start applying rules to it, building a proof tree until it is complete (the leaves of the tree are proven by the rules that do not generate any new sequents; we call those rules axioms, or decision procedures, whatever's appropriate in each particular case).

This is exactly what is happening in my SyMP tool. The prover core does not (and should not) know anything about the underlying sequent, specification language, concrete proof system, or the problem domain. It only knows how to apply the rules as abstract entities, and provides an interactive user interface and some automatic proof search capabilities for doing so.

All the knowledge about the actual proof system is implemented in a proof system module. There can be several different proof system modules plugged in, the prover will not see any difference. Each proof system can be designed for some very specific purpose or a problem domain. This makes the tool highly extensible and potentially applicable to a wide variety of problem domains from hardware to software verification, from solving Rubic's cube puzzles to validating security protocols, etc.

Since the tool provides the proof management and an interactive user interface, all the developer has to do is to implement an input specification language (which includes the way the model and its properties are specified), and a bag of transformations that enable one to prove the properties. The module then is dropped into the SyMP system, and you instantly get access to all of your transformations through the standardized user interface, and the prover will help you make sure your proofs are complete, will record them, allow you to edit the proofs and re-apply them to other properties, etc.

Currently, SyMP has two proof systems. The Default proof system, which is being designed as a very general proof system dedicated to combination of model checking and theorem proving. The other proof system Athena is an emerging module for validating security protocols. Its implementation is carried out by Alex Groce, and it is a reimplementation of the Athena technique invented by Dawn Song.

Compositional Proof System (1995 - 1997)

Once upon a time, I was working on my Compositional Proof System . This system was designed to derive properties of compound systems from (already proved) properties of its components. To understand the general idea, let me describe a typical verification problem. Given a number of communicating finite-state machines and their desired properties (often expressed in some modal or temporal logic), determine if this system satisfies the properties. The way the verification usually works is the following. One builds a huge finite automaton out of this system, whose states are tuples of states of all the processes in the system, and runs a model checking algorithm on it. Obviously, the state space is expected to grow exponentially in the length of the textual description. That's what usually happens in practice. Although recently very efficient data structures were developed (like OBDDs, BMDs, HDDs, etc.), in many practical applications they all grow nearly exponentially, and it is still virtually impossible to verify completely, e.g., a whole microprocessor, even a small one.

My Compositional Proof System is designed so that one can derive properties of a compound system from the properties of its components. The derivation process can be done (almost) automatically in a special purpose theorem prover. The properties of the components can be either derived from the properties of their subcomponents recursively, or simply checked by any appropriate model checking algorithm. Since I never require to build a whole state space of the model, the model checking step can be done on small processes (say, up to 10^4 - 10^8 states), what is now a routine and very fast procedure. Then the prover tries to derive properties of the parallel composition. The complexity of the last step does not depend on the size of the model, and since formulas tend to be small (to be easily understood by humans), this step also should not take too much time. In short, this opens a way to fast verification of virtually any arbitrarily large systems.

Another big advantage of using this kind of theorem proving is the ability to prove certain properties by induction on the number of parallel processes. Therefore, we can check a device with replicated components of any size in just one pass of verification.

In summer 1996 I implemented my Compositional Proof System in PVS, a general purpose proof checker and theorem prover. I proved the soundness of the system using PVS, so it is reliable beyond any doubt (and you shouldn't doubt in the soundness of PVS, of course :). As an example, I verified the liveness property of the Milner's Scheduler with arbitrary number of processes using the induction technique. Model checking was applied only to the atomic processes, which in this case had only 5 or less states (which is indeed trivial!). The rest of the verification was done by deriving of properties in the Proof System. This example showed that the system is powerful enough to prove many useful properties. In addition, the inference process can be easily automated in a special purpose theorem prover, which I am going to write. And what is even more important, the prover may be able to provide a counter example in case the specification is not derivable. This proved to be a really useful feature in previous model checkers (e.g. SMV), and would be definitely important in our case.

I am also working on generalizing the system to the first order logic to be able to reason about data paths as well as control flow in a "natural" way. This extension is described in a paper draft "A Compositional Proof System for The First Order Modal mu-Calculus and Value Passing CCS" (together with Dilian Gurov). Ask me if you want this paper, I'll send it to you.

Model Checking of Timed Automata (1993 - 1995)

In 1992 I joined a research group in Novosibirsk (Russia) working on theory of formal verification, modal logics and model checking. Since then, formal verification became my primary research interest. The same year I developed a small but not quite trivial theory of model checking with discrete time, and later generalized it to multiple clocks. In essence, the time properties were pretty much regular expressions, so no wonder it all worked out nicely. As an illustration to this theory, I implemented an explicit-state model checker and verified several examples like timed alternating bit protocol, message arbiter, etc.

In 1993 I directed my research mostly into the development of compositional verification. I created two algorithms of efficient formula decomposition for the modal mu-calculus and the parallel composition operator in CCS.

Meanwhile, in summer 1994 me and my advisor (at that time N.V. Shilov) presented a paper "An Approach to Effective Model-Checking of Real-Time Finite-State Machines in Mu-Calculus" in St.-Petersburg, describing my model checking algorithm for multiple clocks. Same summer I attended the Summer School "Deductive Program Design" in Marktoberdorf (Germany).

In January 1995, being a visitor at Danish Technical University, I came up with an interesting and promising idea of compositional verification. This started a research project which I was developing till about 1997. Later I realized that it only looks nice on paper, but will never fly in practice, and turned the wheel in another direction.