Formal Verification: Ideas and Challenges
I believe that the greatest challenge in formal verification is not to be able to verify a design of a certain size or complexity, but rather to be able to catch up, get ahead, and continue to stay ahead of the state-of-the-art in the designs. The grand challenge is not a specific milestone to achieve, but rather a direction to follow for an extended period of time.
Ideally, formal verification should be a part of the design process. Of course, the only way we can stay in the design loop is to adjust the verification methodology at least as fast as the designers change the design.
In my opinion, the major problem in formal verification today are inadequate tools. Most tools support only a small range of hard-wired methodologies, are hard and inconvenient to use, and virtually impossible to modify or extend. Hence, everyone who wants to try a new methodogy is forced to write a new tool, often from scratch, spending months if not years just to try out a handful of ideas. As a result, we often get yet another tool with a hard-wired methodology, idiosyncratic input language or API, and no life after graduation of the author.
Compare this with a flexibility of any real-world programming language, where one can come up with an idea, code it up, test quickly, find out why it fails, and go on to the next idea. Would it be great if formal verification methodologies can be prototyped and tested this fast?
Challenge: Fast Prototyping Tools
My observation is that most advances in formal verification happen in the following pattern:
- Slews of new ideas and methodologies are generated on an ongoing basis;
- These ideas are implemented as tools, and tested on real-world examples;
- Only a tiny fraction of these ideas work well in practice;
- The implementation of tools (or prototypes) is by far the major bottleneck in this process.
Hence, an important challenge is to speed up the process of prototyping and testing new methodologies.
Where we are now
- At the moment, we have plenty of tools, theories, and technologies available to us in the form of ideas, papers, stand-alone tools, and practical experiences of individual researchers.
- Most of the practically valuable methodologies come from combining existing ideas.
- Currently, testing a new idea is very expensive and time-consuming.
What we need
- We need a common framework to put these ideas, tools, and experiences together conveniently, easily, and fast, so that bad ideas are filtered out faster, and the rare gems are found more often.
How to get there
- Examine the best working methodologies, find out what are the major components, how they are connected (similarities), as well as what varies in the component parameters, and in their interconnections (differences).
- Put together a library of most frequently used components, implemented in a flexible programming environment. Users should be able to connect and tune the components, and with minimal effort duplicate most of the existing working methodologies.
Prior Art
The idea of a fast prototyping environment is not a new one, and researchers have been trying various ideas: SAL project at SRI, Bogor model checking environment at Kansas State University, and various other projects. PVS can be considered one of such prototyping tools, to a certain degree.
In general, most of the tools that are widely used are either very efficient domain-specific black-box engines, or highly flexible, and better yet scriptable, prototyping environments.
Challenges in Combination of Decision Procedures
Validity checkers, or automated theorem provers based on combination of decision procedures, are becoming the efficient black-box engines used in many formal verification methodologies. By their very nature, these engines must have easy-to-use, convenient interfaces to be added to larger tools. The design and possibly setting standards for such interfaces is one of the main challenges in this area. The next set of equally important problems is the efficiency and expressive power of these engines.
State of the art
- Theory of combining decision procedures has been worked out well for disjoint signatures, both in unsorted and in many-sorted logics.
- There is a solid technology for integrating state-of-the-art SAT solvers into combination framework. In the worst case (tight integration instrumented with proof production), the slow-down is 10x-20x compared to the fastest SAT solver implementations.
- Soundness and proof production has been worked out in CVC Lite; decision procedures are based on efficient inference rules.
- Reasonable user API and input language exist (can be improved further)
- Simple, efficient, and general solution for partial functions, subtypes, and undenoting terms in the logic (terms like x/0).
- Concrete model generation (counterexamples) are currently being tested; we believe to have a good practical solution for a Nelson-Oppen framework. It is still not very efficient though.
- Reasonable architecture of the tool: the result of careful design decisions and disciplined programming.
What we need
- The SAT solver heuristics are suboptimal in the presence of decision procedures; no good solution exists yet.
- Many trade-offs between code complexity and efficiency of implementation; no generally accepted good recipe exists.
- To be investigated (I do not know of any practical solutions):
- Combination of interpolating algorithms
- Combination of widening operators (for model checking software)
- Abstraction/refinement with decision procedures
- Support for interactive proofs and/or high-level scriptable strategies
- Practically efficient theory and architecture for combining DPs with overlapping signatures
Individual Decision Procedures
The main challenges in writing a decision procedure for a combination framework is that the decision procedure must be:
- online (incremental);
- proof-producing (for conflict analysis in the SAT solver);
- propagate all disjunction of equalities (for completeness of Nelson-Oppen combination);
- backtracking.
In addition, the decision procedures must be reasonably efficient, and in some cases (when the underlying algorithm is provably inefficient) be able to give up early, if the user asks so.
State-of-the-art
To date, we have efficient algorithms for the following decision procedures and/or functional modules:
- Uninterpreted functions
- Records and tuples
- Mutable arrays
Implementations exists, but not as efficient as could be:
- Arithmetic (linear and non-linear, mixed integer and real)
- Bitvectors
- First-order quantifiers
- Symbolic simulation
Experimental versions:
- Recursive datatypes
- Transitive closure for binary relations