Tools and Interoperability

Interoperable Tools

The verified software challenge is aimed at scaling up the technology to a point where it can be applied to the [[specification]]?, design, development, and maintenance of large software systems. Many building blocks need to be put in place in order to take on this challenge. These include

1. A body of theory consisting of logics for capturing domain knowledge, specifications, and proofs, and formal semantics of the specification and programming languages, the domain knowledge, and logics.
2. Expressive programming languages that are based on rigorous semantic definitions.
3. A collection of detailed formal specifications of critical systems and libraries
4. A repository of verified software that can be used to benchmark progress as well as bootstrap the wider verification effort.
5. An integrated suite of tools for generating and checking properties of specifications and programs, constructing counterexamples and test cases, and for transforming and optimizing specification and code.

All of these building blocks are important to the overall enterprise, but the integrated tool suite is at the core of effort. The current set of tools have had some significant successes but most of these tools are still in the experimental stage. Scaling up current verification technology will require dramatic improvements in the functionality, efficiency, and robustness of the individual tools, novel tool combinations, and new ways of applying these tools to the verification problem. Newer tools will aggressively exploit parallelism and modularity. Many of these tools have applications beyond verification in areas such as modeling, planning, compiler optimization, workflow, and the semantic web.

While it is essential to have robust and efficient design and analysis tools, much more is needed to achieve reliable software. These include a thorough understanding of the domain in which the software operates, the potential risks and hazards, scalable and composable architectures that preserve system safety by design, novel approaches to constructing and maintaining software that blend multiple concerns, and languages, type systems, and semantics that are well-matched with the application domains.

Scalable performance is an important consideration for effective tool support. Many verification algorithms are quadratic, cubic, or exponential in their worst-case complexity, but natural problems do not always exhibit worst-case behavior. On the other hand, verification is quite data-intensive and so techniques overcoming memory latency bottlenecks will be critical for fully exploiting increased processor speeds. Multicore CPU architectures must be effectively utilized in the design and implementation of verification algorithms.

While scaling up performance, it is also important to scale down the size of the verification problems through abstraction, projection, and decomposition. High-performance tools are can be used effectively to scale down problems while preserving accuracy.

A Catalog of Verification Tools

The verification vista is quite vast and verification tools cover a broad swathe from models and specifications to code, and from [[lightweight tools]]? for analyzing specific properties or [[generating test cases]]? to the more comprehensive systems that employ [[model checking]]? or [[theorem proving]]? techniques. Some forms of [[program analyses]]? are used for identifying optimizations such as dead code, constant folding, and common subexpression elimination. Other analyses are used to check for common runtime errors such as mismatched types, uninitialized variables, division by zero, null-pointer dereferencing, numeric overflows and underflows, and out-of-bounds array references. At the extreme end are tools that establish correctness properties. Model checking tools are used to establish temporal properties of transition systems, typically high-level models of software systems rather than the software itself. Decision procedures and interactive theorem provers can be used to prove that a program meets its specification. Some of the tools may be used incrementally as a given program or model is constructed or edited, while others are applied to the entire description.

For the Verified Software challenge, we need the full spectrum of capabilities to be smoothly integrated so that we can leverage their strengths to build a verification framework that is more than the sum of its parts. We briefly survey the range of tools, and examine the challenges and opportunities in integrating these tools in order to scale the individual capabilities.

1. Mechanized support for specification languages and logics: These are used for capturing the requirements or to model specific aspects of the software or its execution environment at a high level of abstraction. Examples of these include Z, VDM, B, ASM, and PVS. Some of these languages can be used as general-purpose formalisms capturing mathematics. These languages need not be executable, but in some cases, they do have executable subsets. Specification logics include various Hoare logics, temporal logics with real-time and hybrid extensions including Unity, TLA (temporal logic of actions), and fair transition systems, process algebras, and automata.
2. Assertion languages: Code verification requires assertions that are inserted at control points, and contracts that capture pre/post-condition claims at entry and exit points to procedures and methods. These assertions are typically in a side-effect free subset of the corresponding programming language, as illustrated by JML. Verification condition (VC) generators are used to construct proof obligations stating that the precondition together with the program statement guarantees the postcondition. Assertions are also used to specify class invariants that must be preserved by the application of any method to an object of that class.
3. Parsers and syntax analyzers: These ensure that the input specifications, code, assertions, etc., are syntactically well-formed, and render the input into abstract syntax or an intermediate form that is amenable to analysis. Typical examples are static single assignment form (SSA), SUIF, the CIL (C Intermediate language) format for C, the Boogie language for object-oriented languages, and SAL for hardware and software transition systems.
4. Semantic analyzers: The Verified Software project employs a range of automation from highly automated tools that verify the absence of common runtime errors, compute useful invariants and generate test cases, to semi-automated tools that check assertions, contracts, refinement, and specifications. The semantic analyzers here include type checkers, static and dynamic analyzers, and test case generators. These include ASTREE, WPDS, TVLA, CCured, Polyspace, Temporal Rover, and BANE.
5. Theorem provers: Deductive capabilities can be used to discharge the proof obligations that arise in semantic analysis and in the development of specifications and proofs, and in bounded model checking and test generation. Theorem proving support can range from highly efficient decision procedures to proof search tools and interactive proof checkers. Examples include decision procedures like CVC-Lite, MathSAT, ICS, Yices, UCLID, and Barcelogic, proof search procedures like Vampire, E, Otter, Snark, and SATURATE, and interactive proof checkers like ACL2, HOL, HOL-Lite, Isabelle, and PVS.
6. Model checkers: Model checking used to analyze finite-state systems and their extensions for temporal properties and state equivalence. Examples include SPIN, SMV, nuSMV, SAL, Bandera, Cadena, Java Pathfinder, Blast, and CMC, and timed/hybrid model checkers like UPPAAL, Kronos, HyTech, and Chiron.
7. Code generators: These compile executable high-level specifications to running code in some programming language. Some theorem proving systems like Coq, Isabelle, HOL, ACL2, and PVS support such code generation for executable fragments. Various model checkers also support some degree of code generation. They also have the reverse capability so that they can convert low-level code into checkable models. Program refinement and synthesis frameworks like KIDS/Specware and the B tool target the interactive development of code by composing high-level descriptions.
8. Implementation languages for analysis tools: Only a few languages are used in implementing analysis tools. These include C/C++, Java, Lisp, oCaml, Haskell, Prolog, and Twelf, and also scripting languages like Scheme, Python, and Ruby.
9. Libraries: These provide the most useful and flexible functionality for building useful formal applications. Libraries include BDD packages like CUDD, polyhedral and arithmetic manipulation packages such as Omega, linear programming packages, and the ASD+SDF.

There is a great deal of synergy between the different tool classes. For example, explicit-state and symbolic model checkers employ automata over infinite strings to represent properties stated in linear-time temporal logic. Many decision procedures such as those for S1S, SkS, WS1S, and Presburger arithmetic exploit reductions to automata. Binary decision diagrams are used to represent automata transitions as well as sets of automata states. Abstract interpretation and model checking both rely on iterative computation of fixpoints. In model checking, the state space is restricted to be finite so that the model has to be scaled down but it is explored exhaustively. Abstract interpretation operates on the original state space but employs widening (approximation) to achieve convergence. Ground decision procedures are used to automatically construct abstract finite models from concrete ones. These same procedures can be used to invalidate abstract counterexamples that have no concrete counterpart, to refine the abstractions to rule out such spurious counterexamples, and to generate test cases corresponding to the concretely feasible counterexamples. Decision procedures can also be used for bounded model checking and k-induction. Model checkers (symbolic, bounded, and explicit) can be used to generate test cases. Model checkers for timed and hybrid systems also make use of decision procedures for difference logic and real arithmetic.

Goals

The broad goal is that of achieving a robust and interoperable suite of tools that deliver in the above categories. These tools must deliver evidence in the form of counterexamples and witnesses whenever possible. Verified versions of the tools should also be included for use as reference implementations, as well as tool generators that can be used to synthesize tools from the given semantic definitions. The larger goals are

• A powerful suite of scalable analysis tools including static analyzers, dynamic analyzers, hazard analyzers, test case generators, type checkers, decision procedures, model checkers, model extractors, code generators, and special-purpose and general-purpose theorem provers.
• A usable set of design tools for refinement, interface checking, and code generation.
• Various standard intermediate formats with formal semantics that can be used to communicate semantic content between the tools.
• Semantic front-ends that map the semantics of widely used modeling and programming languages into a form that is amenable to analysis.
• Standardized libraries of useful syntactic and semantic operations such as those for multi-precision arithmetic, BDDs, automata (MONA and WPDS), polyhedra, linear programming, and theorem proving.
• A large collection of benchmarks spanning a wide range of applications and case studies.
• An evidential tool bus for integrating different tools through the exchange of semantic information and evidence.

We see the technology developing in the following layers * Basic libraries for syntactic and semantic manipulation

• Tools for static and dynamic analysis, model checking, SAT solving, decision procedures, and rewriting, with open, scriptable interfaces.
• Verification systems developed as tool chains on a tool bus for test case generation, refinement code generation, counterexample-guided abstraction refinement, extended static analysis.
• Integrated verification environments (IVEs) that are connected to integrated development environments (IDEs) to provided added verification capability.

We look at the short-term and long-term challenges in building a coherent tool infrastructure for the verified software project.

Libraries

Short-term challenges

In the next five years, a big priority is to develop the functionality, efficiency, and robustness of the basic libraries so that they serve as a foundation for building scalable analysis tools. These capabilities include

• Standardized interfaces: The application programmer interfaces (APIs) of the various libraries need to have similar calling conventions so that they are both interchangeable and interoperable.
• Robustness: The tools should offer support for error diagnoses and recovery so that these capabilities can be lifted to the higher-level applications.
• Efficiency: The use of advanced algorithmic ideas and heuristic optimizations can yield an order of magnitude improvement in the core functions relative to processor speed increases.
• Embedding of libraries in programming languages used for building tools

Long-term challenges

• Special-purpose hardware support for critical operations.
• Any-time algorithms that deliver reasonable partial results with respect to time and other resource limitations can be used to develop effective approximate analyses methods.
• Interoperability between libraries
• Verified libraries: Libraries can themselves serve as useful challenges for the verified software project.

Tools

Short-term challenges

• Scalable analysis tools that establish the absence of common runtime errors, race conditions, and deadlocks at the rate of 100KLOC/minute to 1MLOC/minute. Symbolic model checkers that can handle 1000 state bits in under a minute. SAT solvers and decision procedures that can be applied to bounded model checking and k-induction problems of 100 to 500 transitions.
• Modular analysis techniques that can efficiently analyze a single procedure or module.
• Property generators, such as shape analyzers, invariant generators, environment generators that operate at 10KLOC/minute to 100KLOCs/minute.
• Combination analysis techniques that allow information exchange between multiple analyses to achieve enchanced accuracy.
• Standardized formats for representing the inputs and outputs of analyzers.
• Scriptable interfaces that can be used to build custom applications from these tools.
• Evidence production in terms of counterexamples, witnesses, and proofs.
• A diverse range of benchmarks that can be used to measure performance and compare different tools and techniques.
• Special-purpose analyzers that can check for memory leaks, information flow, security, timing channels, deadlocks, and race conditions. These tools are developed in conjunction with compositional methods and type systems for specialized properties.

Long-term Challenges

• Powerful automation that enables efficient fully automatic verification of a large class of properties.
• High level of interoperability between tools so that custom applications can be quickly constructed by integrating individual tools.
• The pervasive use of analysis tools in the requirements capture, design, development, refinement, debugging, verification, and maintenance of software systems.
• Verified tools built on verified libraries.
• Extensive benchmarking so that tools are optimized on a range of realistic examples.
• Novel applications in Artificial Intelligence, Computational Biology, Computer Mathematics, Computer Security, Electronic Commerce, Problem Solving Environments, and Education.

Verification Systems

An integrated verification system is built around a programming environment with support for annotations, advanced typechecking, static analysis, dynamic analysis, refinement, code generation, model generation, model checking, interface checking, test case generation