High Assurance (for Security or Safety) and Free-Libre / Open Source Software (FLOSS)... with Lots on Formal Methods / Software Verification

This paper discusses some relationships between high assurance software (for security or safety) and free-libre / open source software (FLOSS). In particular, it shows that many tools for developing high assurance software have FLOSS licenses, by identifying FLOSS tools for software configuration management, testing, formal methods, analysis implementation, and code generation. It particularly focuses on formal methods, since formal methods are rarely encountered outside of high assurance. However, while high assurance components are rare, FLOSS high assurance components are even rarer. This is in contrast with medium assurance, where there are a vast number of FLOSS tools and FLOSS components, and the security record of FLOSS components is quite impressive. The paper then examines why this is the circumstance. The most likely reason for this appears to be that decision-makers for high assurance components are not even considering the possibility of FLOSS-based approaches. The paper concludes that in the future, those who need high assurance components should consider FLOSS-based approaches as a possible strategy. The paper suggests that government-funded software development in academia normally be released under a GPL-compatible FLOSS license (not necessarily the GPL), to enable others to build on what tax dollars have paid for, and to prevent the vast waste of effort caused by current processes. Finally, developers who want to start new FLOSS projects should consider developing new high-assurance components or tools; given the increasing attacks and dependence on computer systems, having more high assurance programs available will be vital to everyone’s future.

Introduction

This paper discusses some relationships between high assurance software (for security or safety) and free-libre / open source software (FLOSS). First, let’s define these key terms.

Definitions

Free-libre / open source software (FLOSS) is software whose license gives users the freedom to run the program for any purpose, to study and modify the program, and to redistribute copies of either the original or modified program (without having to pay royalties to previous developers). It’s also called libre software, Free Software, Free-libre software, Free-libre / Open source (FLOS) software, or open source software / Free Software (OSS/FS). The term “Free Software” can be confusing, because there may be a fee for the Free Software; the term “Free” is derived from “freedom” (libre), not from “no price” (gratis). More formal definitions of open source software and free software (in the sense of libre software) are available on the web. Examples include the Linux kernel, the gcc compilation suite, the Apache web server, and the Firefox web browser. Many FLOSS programs are commercial, while many others are not.

For purposes of this paper, let’s define “high assurance software” as software where there’s an argument that could convince skeptical parties that the software will always perform or never perform certain key functions without fail. That means you have to show convincing evidence that there are absolutely no software defects that would interfere with the software’s key functions. Almost all software built today is not high assurance; developing high assurance software is currently a specialist’s field (though I think all software developers should know a little about it). To develop high assurance software you must apply many development techniques much more rigorously, such as configuration management and testing. You need to use implementation tools you can trust your life to. And in practice, I believe that you need to use mathematical techniques called “formal methods” for a product to be high assurance, for the simple reason that it’s usually hard to create truly convincing arguments otherwise. A significant fraction of this paper covers formal methods, since they are rarely encountered outside of high assurance. There isn’t a single universal definition of the term high assurance, and products have been labelled “high assurance” without having any formal methods applied to them. But this definition should be sufficient for my purpose. Other terms used for this kind of software are “high integrity” and “high confidence” software.

Usually high assurance software is developed because of serious safety or security concerns. Strictly speaking, software by itself has no safety or security properties -- it can only be safe or secure in the context of a larger system. A nice discussion of this issue from the safety point of view is in Nancy Leveson’s book Safeware (see section 8.3). But software tends to control safety and security systems, and such software is often called “safe software” or “secure software”. For this paper I’ll talk about the security or safety of the software, with the understanding that this only makes sense if you understand the system that the software will be part of.

For purposes of this paper, the identity of the software’s supplier is not part of the definition of high assurance. By supplier, I mean the provenance (origin) and pedigree (lineage -- who the software passed through) of the software. By keeping the supplier identity out of the definition of high assurance, I can concentrate on technological issues. In reality, there may be some people who you wouldn’t trust even if they’d “proved” their code correct... so in practice it’s quite reasonable to ask questions like, “Who developed or modified the software? Can I trust them?” For both FLOSS and proprietary software, provenance and pedigree can be considered in exactly the same way -- in both cases, you’d consider who originally developed the software (in terms of each change), and who controlled the software from development through deployment to you. In particular, you’d consider who has rights to modify the software repository, and whether or not you trusted them. You might also consider how well the development environment itself is protected from attack. Don’t be fooled into thinking that FLOSS is “riskier” than proprietary software because it can be legally modified by anyone. Anyone can modify a proprietary program with a hex editor, too -- but that doesn’t mean you’ll use that modified version. The issue with suppliers is who controls your supply chain, and FLOSS often has an advantage in provenance and pedigree (because it is often easier with FLOSS to determine exactly who did what, and who has modification rights). But provenance and pedigree issues have to be handled on a case-by-case basis, and trying to cover those issues as well would over-complicate this paper. For example, the whole issue of “who trusts who” varies depending on the organizations and the circumstances. In an ideal world this wouldn’t matter, because the proofs would be true and could be rechecked everywhere. Given the massive move to globalization, I think that would be worth trying to make who created the software irrelevant. In any case, let’s concentrate on the technical aspects in this paper.

Contrasting levels of assurance

More generally, assurance is simply the amount of confidence we have that the software will do and not do the things it should and should not. Sometimes the things it should not do, what I call "negative requirements" , are the most important. Any particular piece of software can be considered by someone to be low, medium, or high assurance. This is obviously a qualitative difference; two products could be in the same assurance category, yet one be more secure than another.

For purposes of this paper, let’s define medium assurance to be software which doesn’t reach high assurance levels, but where there has been significant effort expended to find and remove important flaws through review, testing, and so on. Note that when creating medium assurance software, there’s no significant effort to prove that there are no flaws in it, merely an effort to find and fix the flaws.

Medium assurance software must undergo testing and/or peer review to reduce the number of flaws. Such mechanisms can be really valuable in reducing flaws, and eliminate a great many of them, but the normal method of using these mechanisms won’t guarantee their absence. You can eliminate some types of flaws completely by some activities, e.g., you can completely eliminate buffer overflows by choosing almost any programming language other than C or C++... but doing so would not eliminate all flaws! In particular, testing by itself is impractical to prove anything about real software. After all, exhaustively testing a program that just adds three numbers would take 2.5 billion years (assuming each number was 32 bits, you could run the program a billion times per second, and you used 1,000 computers for testing). Real programs are much more complicated than this, which is why testing by itself can’t reach the highest levels of assurance.

The differences between medium and high assurance (as I mean the terms in this paper) seem to confuse people, so let me contrast them directly. When developing a high assurance program, the program is presumed to be wrong (guilty) until a preponderance of evidence proves that it’s correct. When a medium assurance program is being developed, it is spot-checked in various ways throughout its development to try to detect and remove some of its worst defects. Medium assurance software development normally leave some defects in the program afterward. Few like the presence of latent defects, but few people are willing to pay for (or invest the time) for high assurance development techniques today in most software.

It’s reasonable to think that as technology improves, high assurance programs will become more common. But even today there are some situations where medium assurance is not enough. Typically this is where people’s lives, or the security of a nation, is at stake. In such cases, some of today’s customers need serious evidence that there are no critical defects of any kind. They need something different: High assurance.

High assurance challenges and standards

Ideally, all software would be high assurance, but ideally we’d all live in mansions. It’s very difficult to create truly high assurance software. The configuration management and testing requirements are usually more severe (and time-consuming) than those for other kinds of software. Applying formal methods requires significant mathematical training that most software developers don’t have, and can be very time-consuming.

Because of these challenges, high assurance software is usually only developed for critical security or safety components. When creating critical security or safety components, a number of regulations are often imposed.

High assurance software for security is the point of the Common Criteria for IT Security Evaluation (ISO standard 15408) when you select EAL 6 or higher -- and EAL 6 is really a compromise! For purposes of this paper, medium assurance software is in the EAL 4 to 5 range of the Common Criteria, so Red Hat Linux and Microsoft Windows would both be considered medium assurance products. I consider EAL 2 (or less) to be low assurance; EAL 3 is a compromise, but it’s basically low assurance.

Here are some other standards that are often mentioned in the security or safety world, which often impact this kind of development:

• Security: Besides the Common Criteria, the older (superceded) Orange Book defined a set of requirements; level B3 had a number of requirements aimed at high assurance, and level A1 extended them even further. (Again, A1 was clearly high assurance, with the next highest level B3 being a kind of compromise.) While not officially required, the FAA and DoD have developed Safety and Security Extensions for Integrated Capability Maturity Models. In the U.S. national intelligence world, another software security standard is DCID 6/3; its confidentiality protection level 5 imposes many requirements (see the DCID 6/3 manual if you want to know what each level means).
• Safety: RTCA DO-178B (Software Considerations in Airborne Systems and Equipment Certification), particularly its Level A, is often mentioned in this context (DO-178B is known to have problems -- following it by rote will not necessarily lead to highly assured systems, according to a draft ASSC DO-178B study). Other oft-noted standards related to software and safety are ARINC-653 (Avionics Application Software Standard Interface), EUROCAE ED-12B (Software Consideration in Airborne Systems and Equipment Certification), the U.S. Department of Defense’s MIL-STD-882, and the UK Ministry of Defence’s Def Stan 00-55 (Requirements for Safety Related Software in Defence Equipment). The U.S. Food and Drug Administration has its General Principles of Software Validation; Final Guidance for Industry and FDA Staff for medical devices (including parts of devices or producers of devices).

Organization of paper

The rest of this paper looks at FLOSS tools that can be used to create high assurance components (there are many), and FLOSS components that are high assurance themselves (they are rare). It then contrasts this situation with medium assurance -- there are many medium assurance FLOSS tools, and FLOSS components with impressive results. The paper then speculates why this is the circumstance, and then concludes.

Tools to create high assurance components

It turns out that there are a lot of FLOSS tools that can be used to help develop high assurance software. To prove that, I’ve identified a few important tool categories, and for each category I identify several FLOSS tools. The tool categories I discuss below are configuration management tools, testing tools, formal methods (specification and proof) tools, analysis implementation tools, and code generation tools.

There are many other categories of tools, and many other specific FLOSS tools, that are not listed below. But the discussion below should prove my point that there are many FLOSS tools that can be used to help develop high assurance components.

Configuration management tools

There are many FLOSS software configuration management (SCM) tools, indeed, I’ve written a review of several FLOSS SCM tools. (I’ve also written a paper discussing SCM and security.)

CVS is an old and still very widely-used SCM tool. I suspect that most software worldwide, both proprietary and FLOSS, is still managed by CVS as of 2006. Subversion (SVN) is the SCM tool rewritten as a replacement for CVS, and it’s widely used, too. But the list of FLOSS SCM tools is amazingly long, including GNU Arch, git/Cogito, Bazaar, Bazaar-NG, Monotone, mercurial, and darcs (see my paper for a longer list). Clearly, there’s no problem finding a FLOSS SCM tool.

Testing tools

All developers test their software, but high assurance software requires much more testing to gain confidence in it. But again, there’s a massive number of FLOSS tools that support testing. In fact, there are so many FLOSS tools for testing that there’s a website (opensourcetesting.org) dedicated to tracking them; as of April 2006 they list 275 tools! This ranges from bug-tracking tools like Bugzilla, to frameworks for test scripts like DejaGnu.

Many high assurance projects are required to meet specific measurable requirements on their tests. One common measure of testing is “statement coverage” (aka “line coverage”), the percentage of program statements that are exercised by at least one test. One problem with the statement coverage measure is that statements that have decisions, such as the “if” statement, can cause different paths. Thus, another common measure of testing is “branch coverage” the percentage of “branches” from decision points that are covered. Branch coverage has its weaknesses too, so there are many other test measures as well -- but statement and branch coverage are the two most commonly-used measures, so we’ll start with them.

Some experts believe that unit testing (low-level tests) should achieve 100% statement coverage and 100% branch coverage, with the simple argument that if you’re not even covering each statement and each branch, your testing is poor. Most others argue, however, that 80%-90% in each is adequate -- because the effort to create tests to meet the last percent is very large and less likely to find problems than by spending the effort in other ways. No matter what, in my opinion you should create your tests first and then measure coverage -- don’t write your tests specifically to get good coverage values. That way, you’ll often gain insight into what portions of the code are hard to test or don’t work the way you thought they would. That insight will help you create much better additional tests to bring the values up to whatever your project requires.

(Oh, and why measure both statement and branch coverage? It turns out it's possible to meet one without the other. For example, an "if" statement with a "then" clause but no "else" caluse might have all its tests yield true.. in which case all the statements are covered, but not all the braches are covered (the "false" branch is not covered). Normally, when you cover all branches you cover all statements, but there are special cases where that is not true. For example, if your program (or program fragment) doesn't contain any branches, or if there is an exception handler without any branches in its body, you can have all branches covered but not all statements covered. Exception handlers might be considered a branch, but that interpretation is not universal.)

There have been several recent developments in testing that improve test efficiency:

• QuickCheck is QuickCheck (BSD license) is a combinator library written in Haskell, designed to assist in software testing by generating test cases for test suites. As noted in Wikipedia, "The author of the program being tested makes certain assertions about logical properties that a function should fulfill; these tests are specifically generated to test and attempt to falsify these assertions." The assertions are also useful for documenting the program. Although the original was created for Haskell, re-implementations exist for Scheme, Common Lisp, Python, Ruby, Standard ML, and many other languages.
• One of the most important recent developments in testing has been developed by NIST, and is to be released as a FLOSS tool. NIST's NIST's Automated Combinatorial Testing for Software work has developed new algorithms to efficiently create a minimum number of tests that nevertheless cover various levels of combinatorials. This means that you can efficiently create test suites that really do a good job of testing all combinations.

Even in the case of test case measurement, there are FLOSS tools that can meet this need. There are several FLOSS “test coverage” tools, such as gcov, that can report which statements or which branches were not exercised by your test suite.

Formal methods tools

Many software developers have no idea what “formal methods” are. Yet my definition of high assurance implies that we’ll usually need to use “formal methods” to create high assurance software. This section explains what formal methods are, shows that there are lots of FLOSS tools even in this area, and then discusses some of the implications.

Formal methods: Introduction

Formal methods, broadly, are the application of rigorous mathematical techniques to software development (see An International Survey of Industrial Applications of Formal Methods for a lengthier definition and discussion). Ideally, we’d like a rigorous mathematical specification stating exactly what we want the program to do and not do, and then prove all the way down to the machine code that the software meets the specification. This is normally hard to do, so various compromises are often made. Many have identified three different broad levels of the use of formal methods, in order of increasing cost and time:

• Level 0: A formal specification is created (a specification using mathematics), and the program is then developed from this informally. This has been called “formal methods lite”. Creating formal specifications is not easy, because you’re trying to take ambiguous, poorly-defined ideas and turn them into a rigorously defined specification. Still, creating a formal specification often doesn’t take too much time (for someone trained in how to do it), and they do tend to help clarify what the real issues are. This is the cheapest way to use formal methods, and many argue it’s the most cost-effective way to use formal methods.
• Level 1: The mathematical approaches are used further, beyond a specification but not all the way into code. Two common ways are to (a) refine the specification down deeper to a mathematically-defined design or a more detailed model, and/or (b) prove important properties of the specification and/or model (either by hand or with automated help using a theorem prover or model checker).
• Level 2: Theorem provers and/or model checkers may be used to fully prove that the actual code matches the design specification. This is usually very expensive, and when done at all this is often done with only the most critical portions (where no other way can give enough confidence).

The “levels” are a little misleading, because you can actually do things partially (perhaps only a part of the software is formally specified), and level 1 is somewhat ambiguous. But these levels give the basic flavor; there is a trade between rigor and effort.

Now we come to the decision of where to draw the line, and this isn’t an easy decision. For purposes of this paper, to count as “high assurance” there needs to be some carefully-reasoned explanation as to why the running code meets its key requirements. How much effort is needed for this justification depends on the risk you’re willing to take, and where you perceive the risks to be. Thus, while level 0 may be less costly, that is often not enough, so high assurance development often moves into level 1 and uses a focused application of level 2 on the parts that cannot be shown correct otherwise. Almost no one tries to prove all code down to the machine code; typically developers with such concerns will check the machine code by hand to ensure that it corresponds with the source code. Some may prove down to the source code, or at least the parts of the source code that are most worrisome. Others may use proofs to a detailed software design, and then use other less rigorous arguments to justify the source code. You can even back off further, using formal methods only for the specification (level 0), or not at all. In all cases, though, there needs to be some careful reasoning that convinces others that the code actually meets the key requirements, typically by showing a stepwise refinement from specification through to the code. Mantras such as “correct by construction” come into play in these kinds of systems.

We would love to formally prove that every line of code, down to the machine code, is correct; doing so has lots of benefits. Why is it so costly? Simply put, creating proofs is incredibly hard to do; often tools and knowledgeable humans must work together to create them. To prove code correct, you generally must write the code and proofs simultaneously (so that the code is in a form that is easier to prove). Requiring proofs also creates limits on the size of programs (and thus their functionality), because our ability to do proofs does not scale that well. Years ago, the old historical rule of thumb for the largest amount of code that can be reasonably proven correct all the way down to the code level was about 5,000 lines of code. Cleanly-separated components can be verified separately (e.g., a computer’s boot and initialization programs might be separable from an operating system kernel), and that helps. This rule of thumb is (I believe) historical; the tools for verifying code have improved, and good tools (including languages designed for provability) can help today’s developers go significantly beyond this scale. SPARK Ada’s developers in particular claim they can go way beyond this. But it’s not clear where the upper bounds really are, and it’s clear that formally proving code gets harder as the software gets larger. Typical operating systems have millions of lines of code and are growing fast, so no matter what the upper bound is, there is a real gap between typical commercial demands for functionality and the ability of today’s formal methods tools to verify it. Don’t expect Windows, MacOS, the Linux kernel, or *BSD kernels to be formally proved down to their code level. Proving only general models of code (instead of the system itself) eliminates this problem, but as I noted above, this doesn’t show that the code itself is highly assured.

Note that all formal methods have a basic weakness: They must make assumptions, because you have to start somewhere. In any such system, humans have to check the assumptions very, very carefully. If you start with a false assumption, a "proof" could produce an invalid conclusion. This problem -- that your assumptions may be invalid -- is a key reason that testing and other activities are still needed for high assurance software, even if you use formal methods extensively.

Another trade-off in formal methods is between expressiveness and analyzability. Fundamentally, any formal method has some sort of language, a set of axioms, and inference rules (the rules that let you determine if something else is true). A language that is extremely flexible (expressive) typically tends to be harder to analyze. As a result, there are many different languages, each better and different things.

For more information about formal methods, you can see the Wikipedia information on formal methods (particularly the main article on formal methods, automated theorem proving, and model checking), the Formal Methods Virtual Library, the NASA Langley Formal Methods Site, and the Formal Methods Education Resources. QPQ (“QED Pro Quo”) is intended to be an “online journal for publishing peer-reviewed source code for deductive software components”, and has links to various tools and papers. Aleksey Nogin’s “A Review of Theorem Provers” has a nice short summary comparing theorem provers. The Seventeen Provers of the World compares 17 proof assistants for mathematics, and some of which are relevant to software development. Most surveys seem to be old, unfortunately. A quick overview is available from the CMU 1996 paper “Strategic Directions in Computing Research Formal Methods Working Group” as E. Clarke and J. Wing’s 1996 “Formal Methods: State of the Art and Future Directions” [PDF]. I can point out “Notes on PVS from a HOL perspective” by Michael J.C. Gordon (1995), An Analysis of two Formal Methods: VDM and Z (1997), and Vienneau’s 1993 “A Review of Formal Methods” (even the full version is incomplete for its time, but at least it is easy to read). The History of the HOL System explains some of the convoluted history of LCF, HOL, and their various derivatives, and also notes some other systems. "Formal Methods for IT Security" (May 2007) has quick overview of tool types (one quibble: I agree that automatic theorem provers like prover9 take less effort than interactive tools like PVS and HOL, but automatic tools don't give less assurance - it's just that they cannot be effectively used on certain classes of problems). The “Handbook of Automated Reasoning” (Edited by J. Alan Robinson and Andrei Voronkov) is a survey. A short 2003 survey of tools commented on many tools, and the Formal Methods Framework report (1999) summarizes many tools. DACS’ list of formal methods literature is old, but it’s nicely focused on key works. Ingo Feinerer's "Formal Program Verification: A Comparison of Selected Tools and Their Theoretical Foundations" (2005) is a much more recent comparsion of formal methods tools (in this case, of the Frege Program Prover, KeY, Perfect Developer, Prototype Verification System). Griffioen and Huisman's 1998 work compares PVS and Isabelle; Zolda's 2004 work compares Isabelle and ACL2. Formal Methods Europe is an independent association with aim of stimulating the use of, and research on, formal methods for software development; their website has some summaries (though it has a very anemic list of tools as of May 2006). The mathematically-oriented papers Information technology implications for mathematics: a view from the French riviera and Deliverable 4.1: Survey of Existing Tools for Formal MKM compares tools’ mathematical foundations (these have the informal look of notes not intended for the masses, but they are still interesting). Johann Schumann’s Automated Theorem Proving in High-Quality Software Design discusses integrating automated theorem provers into larger development approaches and tools. High-Integrity System Specification and Design by Bowen and Hinchey is a collection of older key essays. Bowen and Hinchey’s “Ten Commandments of Formal Methods ...Ten Years Later” (IEEE Computer, January 2006) discusses previously-identified lessons learned (their “ten commandments” of their IEEE Computer April 1995 article) and argues that they have generally stood the test of time. Two oft-referenced formal methods advocacy pieces were published in IEEE Software: “Seven Myths of Formal Methods” by Anthony Hall (Sep/Oct 1990) and “Seven More Myths of Formal Methods” by Bowen and Hinchey (July 1995). Richard Sharpe argues that formal methods may be increasingly used in the future. Palshikar’s “An introduction to model checking” is a gentle introduction to that topic. Tony Hoare and Jay Misra have proposed a “Grand Challenge” effort to speed maturation of formal methods -- for their pitch, see Verified software: theories, tools, experiments (July 2005). The VSETTE conference of October 2005 has a response to this proposal, focusing on systemic methods for specifying, building, and verifying high-quality software. Shankar’s presentation The Challenge of Software Verification gives interesting comments on this challenge. The paper Formal specification and verification of data separation in a separation kernel for an embedded system (Constance L. Heitmeyer, Myla Archer, Elizabeth I. Leonard, and John McLean of the Naval Research Laboratory) describes a very promising approach to proving all the way down to the code. These tools generally presume that you already understand the basics of formal logic; if you don't, books such as P. D. Magnus' "forall x" may be of use to you. (A serious problem in the U.S. is that many software developers have never studied discrete math, including logic, even though that's the basis of their field; few would allow a civil engineer to design a bridge without first learning calculus.) No doubt there are many other sources of information. Peter Gutman's article on "Verification Techniques" (a chapter of his thesis) is a much more pessimistic view of verification techniques, and has important insights on the limitations of formal methods and some other verification techniques.

After I wrote this paper, I discovered the very interesting list Free software tools for formal verification of computer programs by David Mentré. You should definitely take a look at this paper as well if you're interested in the topic! Trac's list of Theorem Proving systems identifies their licenses, many of which are FLOSS.

Here are some other lists of formal methods related tools:

• The Caml Maths and Logic list includes a number of tools, some of which are FLOSS.
• Formal methods links by Mark Utting
• ANL's list
• Database of Existing Mechanized Reasoning Systems (at Stanford) (Warning: Extremely outdated list)
• Tigris is an open source community focused on building better software engineering tools (for collaborative software development). They don't specifically focusing on formal methods, but they have interesting tools like Delta (BSD license) which minimizes "interesting" files subject to a test of their interestingness (e.g., to isolate a small failure-inducing substring of a large input that causes your program to exhibit a bug). Many of their tools can usefully work with the tools listed below.

Note - don’t treat “formal methods” as a checklist item for high assurance (oh look, some math, we’re done!). The point in high assurance is to identify the risk areas, and then use tools (like formal methods) to convincingly show that there isn’t a problem. There is more than a little overlap between those developing high assurance software and the research community; applying these techniques can be difficult for some domains, if you need to get really high levels of confidence for complex systems.

Formal methods: Categories of tools

There are many different kinds of formal methods tools, which I will group into these categories:

• Specification tools: These help you write and check specifications written using a formal notation (such as Z, VDM, B, etc.). These tend to be designed for people who are working at level 0 or level 1; they are often connected with other tools to go to level 1 or 2.
• Theorem provers/proof checkers: Theorem provers take a set of assumptions and rules, and try to prove claims about them using traditional mathematical proof techniques (generally they need human help). They vary on many factors, such as what information they can use (from specifications or general theorems down to program code or annotations). Proof checkers check a proof created elsewhere.
• Model checkers: These try to prove claims, but unlike theorem provers, model checkers do this by trying to find all possible circumstances (states) and showing that they meet the criteria.
• Other: Other tools exist which don’t easily fit into these categories.

Note that these are very rough and imprecise categories. All formal methods tools must support some kind of specification notation, tools often have multiple capabilities, and there is a general trend of combining these tools into larger interoperable capabilities. A general discussion about issues in integrating tools is in the paper “PVS: Combining Specification, Proof Checking, and Model Checking”. Thus, any categorization is imperfect, but hopefully this division will help.

There are some interesting competitions, particularly for the automated tools. Here are the CASC results of 2008 using TPTP, for example.

It turns out that there are many FLOSS tools that support using formal methods, in all of those categories, as the following sections will show.

Formal methods: Specification tools

All formal tools have some sort of specification language, but some languages are often focused on higher-level specifications -- helping users enter, syntactically check, and cleanly display the specifications with a minimum of effort. These are often used for level 0 and 1 type of work (though they can be used for more -- often by devising connections to other tools). Here is a partial list of specification languages, and FLOSS tools that support them:

• Z. Z is pronounced “zed” even in the U.S., and in 2002 was standardized as ISO/IEC standard 13568:2002(E). There are several toolsuites that support Z. The Community Z tools (CZT) project is developing and coordinating FLOSS projects that develop Z support tools. fuzz (MIT license) is a type-checker for Z. ZETA (GPL + public domain) is an environment for developing specification documents based on Z. “It provides an integration framework for tools to edit, analyse and animate Z specifications and formalisms which are mapped to Z.” It supports type-setting, type checking, and “execution” of pure Z. ProofPower (GPL license, except for the Ada plug-in) is a suite of tools supporting specification and proof in Higher Order Logic (HOL) and in the Z notation. Jaza (GPL) is an "Animator" for the Z formal specification language, developed at the University of Waikato (primarily by Mark Utting). More information about Z is available at Z User Group, including the Z User Group virtual library.
• Alloy. Alloy is a tool that's hard to categorize. Alloy implements a specification language that's intentionally similar to Z, but makes it very easy to analyze and find counter-examples for. Its analysis capabilities are far beyond what a "pretty printer" or "type checker" can do, but it can't prove arbitrary properties; see its description for more information. You give up some capabilities, but receive a massive ease-of-use bonus in return.
• CASL. The "Common Framework Initiative for algebraic specification and development" (CoFI) is a voluntary organization for an open collaborative effort to produce a Common Framework for Algebraic Specification and Development. In particular, they have produced the Common Algebraic Specification Language (CASL), a specification language that is designed to be a careful selection of known constructs, intended to be expressive, simple, and pragmatic. Their goal was to create a language suitable for specifying requirements and design for conventional software packages; it has restrictions to various sublanguages, and extensions to higher-order, state-based, concurrent, and other languages. Hets (LGPL-like license), the successor of the CATS tool, supports CASL, several extensions of CASL, and Haskell. Hets is a parsing, static analysis and proof management tool for combining various tools for different specification languages; its "single" language is the heterogeneous specification language HetCASL. Hets includes parsing, static analysis, and proof support.
• VDM-SL (Vienna Development Methodology - Specification Language). Overture is a set of FLOSS tools (both current and under development) to support the VDM++ specification language (an enhanced version of VDM). VDM-SL is standardized by ISO/IEC as ISO/IEC 13817-1: 1996. VMD is really a whole method, of which VDM-SL is the specification language piece. VDM seems to be less active than Z to me, but that is simply an impression and may not be true.
• Unified Modeling Language (UML) Object Constraint Language (OCL). UML is defined by the Open Management Group (OMG); UML version 2.0 added OCL. KeY (GPL license) supports formal specification and verification of programs in conjunction with UML. UML OCL is part of the UML standard; KeY can then analyze the constrains. The target language of KeY based development is Java CARD, a proper subset of Java for smart card applications and embedded systems. KeY currently requires the use of a proprietary UML tool, but this does not seem fundamental to KeY; it should be possible to integrate KeY into a FLOSS UML tool as well.
• B method. The RODIN Project (Common Public License and Eclipse Public License) is developing a platform focused on the B method, as is Brillant (LGPL license). The virtual library for the B-method has more information about B.
• ProMela. ProMela is a language for specifying distributed software systems; it was originally developed for the model-checking tool Spin, and the DiVinE tool supports it too. See the text below for more about these tools.

Formal methods: Theorem Provers/Proof Checkers

Here are FLOSS theorem provers and checkers (increasingly they are combined with model checkers, in which case I list them here and not under model checkers):

• ACL2 (GPL license) is an industrial-strength theorem prover, part of the Boyer-Moore family of provers (winner of the 2005 ACM Software System Award). It takes expressions using LISP notation and tries to automatically prove the expression. ACL2 is one of the more commonly-used such tools for industrial-strength proving of real world programs, though it’s certainly not the only one. I’ve talked to users of ACL2, who claim that ACL2 strikes a nice balance between trying to do everything automatically (which sadly isn’t practical yet) and forcing users to do everything “by hand” (which is painful) -- it tries to do much automatically, while still making it easy to control. ACL2 is the intellectual successor of the Nqthm theorem-prover. This family has been used to prove correctness for many processor designs, microcodes, and machine object codes, including AMD microprocessors and pieces of the Berkeley string library. See Boyer and Yu’s and Boyer and Moore’s “Mechanized Formal Reasoning...” for work at the machine code level, where they found 3 defects at the machine code level (the same idea works for bytecode, too). I should note that this family of tools (ACL2/Nqthm) is rather different from other tools. ACL2’s developers claim that it only takes several months to become an effective ACL2 user for someone who has “a bachelor’s degree in computer science or mathematics, has some experience with formal methods, has had some exposure to Lisp programming and is comfortable with the Lisp notation, is familiar with and has unlimited access to a Common Lisp [implementation], is willing to read and study the ACL2 documentation, and is given the opportunity to start with “toy” projects”.

  ACL2 is powerful enough to be very useful, and has been used for many important commercial projects. ACL2 directly supports mathematical induction, meaning that ACL2 can directly handle computer programs with loops or recursion (something many other theorem-provers cannot handle as directly and thus must handle in other ways). ACL2’s defchoose and defun-sk abilities add the ability to handle “there-exists” and “for all” statements to ACL2, which the ACL2 developers say adds “all the abilities of full first order logic” (but see below for the limits in how they can be applied; ACL2’s support for the quantifiers (for-all and there-exists) is limited). ACL2 supports encapsulation (the “encapsulate” form lets you describe general properties of a function, instead of having to define all functions), so you do not have to define an executable function to use ACL2. ACL2 supports some capabilities of second-order logic (higher-order functions, though not variables).

  ACL2 is one of the strongest of any theorem-prover in its support of executability; you can interactively enter runnable LISP functions, and begin proving properties about them. That is really powerful! There are good LISP compilers, so the execution can be really fast (especially if you use the usual LISP speedup tricks, such as tail recursion, arrays, and declaring numeric types). It also supports “single threaded objects”, which you can use to make models with state run much faster.

  ACL2 has weaknesses (and perceived weaknesses) as well, though there is ongoing work to address many of them:

  • It is not well integrated into other tools. For one, there’s no strong connection with higher-level specification languages like Z or B. There’s little support to call out to other tools like other proof checkers or model checkers (e.g., Otter/Mace/Prover9) -- such integration would make it possible to use their capabilities to automatically prove theorems when ACL2 cannot find the proof without help. The latter would be very useful because although many find ACL2’s theorem prover relatively easy to guide, ACL2 needs to be guided in cases where other theorem provers could automatically find the proof. For more information see the work on Ivy and Mu-Calculus in “Computer-Aided Reasoning: ACL2 Case Studies”, which could perhaps be the basis for connecting ACL2 to other theorem provers (like Otter/Prover9) and model checkers.
  • ACL2 doesn’t have a lot of support for reasoning about quantifiers (for-all and there-exists). Certifying Compositional Model Checking Algorithms in ACL2 (by Ray, Mattherws, and Tuttle) identifies several ACL2 weaknesses: its logic “has little support for modeling or reasoning about infinite sequences” and does not “permit recursive function definitions with quantifiers in the body”. They also note how these weaknesses could be eliminated; note that this work would also help integrating ACL2 with other tools.
  • ACL2 does not support typing well. ACL2 is basically untyped, and functions essentially have to be defined for all types that exist in ACL2 -- even if that’s unnecessary. “Guards” make execution faster if certain typing restrictions are met, and constructs like (declare (type ...)) and initial requirements can specify type requirements, but ACL2 is not really focused on supporting types. There have been discussions about these issues, such as Vernon Austel’s “Adding a typing mechanism to ACL2” and Manolios and Moore’s “Partial Functions in ACL2” (describing a “defpun”), and Kaufmann and Sumners’ “Efficient Rewriting of Operations on Finite Structures in ACL2”.
  • LISP’s notation is regular but different than what many are used to. In LISP, function names always precede operations, and parentheses are used (* (+ 2 1) 3) is “(2+1)*3”. For those who prefer more conventional notations (such as using infix operators), there are some solutions. There are tools to (1) “pretty-print” results (including using infix notation) and to (2) accept statements in a more conventional infix syntax (this is IACL2, aka Infix ACL2). IACL2 works, but it is not as portable, and its input notation does not support some of ACL2’s advanced capabilities. Maturing IACL2 to support all ACL2 features, and improving its documtation so that users could just use the syntax directly, would be valuable in my opinion.

  If you are thinking about using ACL2, I highly recommend getting two books by the tool’s creators. These are Computer-Aided Reasoning: An Approach, which describes how to use the tool, and Computer-Aided Reasoning: ACL2 Case Studies, which gives worked examples on various problems. They are absurdly pricey in hardback (around $215-$224 each!), so buy softcovers from the authors instead.

• PVS Specification and Verification System (GPL License, as of the 4.0 release of December 2006) is one of the other major theorem provers/verifiers, and it's also FLOSS. As they say, "PVS is a verification system: that is, a specification language integrated with support tools and a theorem prover. It is intended to capture the state-of-the-art in mechanized formal methods and to be sufficiently rugged that it can be used for significant applications."
• Symbolic Analysis Laboratory (SAL) (GPL license) is a framework for combining different tools to calculate properties of concurrent systems. At its heart is a language devised by SRI, Stanford, and Berkeley, for specifying concurrent systems in a compositional way. Here's how they describe it: 'It is supported by a tool suite that includes state of the art symbolic (BDD-based) and bounded (SAT-based) model checkers, an experimental "Witness" model checker, and a unique "infinite" bounded model checker based on SMT solving. Auxiliary tools include a simulator, deadlock checker and an automated test generator.'

  mCRL2 (BOOST license) stands for micro Common Representation Language 2. "It is a specification language that can be used to specify and analyse the behaviour of distributed systems and protocols and is the successor to μCRL. It is a formal specification language with an associated toolset. Using its accompanying toolset systems can be analysed and verified automatically. The toolset can be used for modelling, validation and verification of concurrent systems and protocols. The toolset supports a collection of tools for linearisation, simulation, state-space exploration and generation and tools to optimise and analyse specifications. Moreover, state spaces can be manipulated, visualised and analysed.
  
  "mCRL2 is based on the Algebra of Communicating Processes (ACP) which is extended to include data and time. Like in every process algebra, a fundamental concept in mCRL2 is the process. Processes can perform actions and can be composed to form new processes using algebraic operators. A system usually consists of several processes (or components) in parallel."

• Otter/MACE (public domain), developed at the Argonne National Laboratory, is the “first widely used high-performance theorem prover” (according to Wikipedia). It includes a built-in model checker (MACE2). This is very powerful theorem prover, and has proved theories unsolved by mathematicians. A sister project even proved a 60-year-old conjecture, the Robbins problem, and made the New York Times; many mathematicians failed to find the proof, yet Otter handles it easily. That makes Otter noteworthy, but Otter has since been superceded by Prover9/Mace4, noted next.
• Prover9/Mace4 (GPL license) is a combination of two programs: Prover9 is an automated theorem prover for first-order and equational logic, (based on resolution/paramodulation), while Mace4 searches for finite models and counterexamples. Prover9 is a successor of the Otter Prover, with a tagline "the future of theorem proving". You can check the proofs produced by Prover9 using Ivy, a preprocessor and proof checker proved using ACL2. I've used this one personally - if you have a problem that's easily expressed in its language, this is a very good tool.

  SPASS (GPLv2) is an automated theorem prover for first-order logic with equality. It can be used for the "formal analysis of software, systems, protocols, formal approaches to AI planning, decision procedures, and modal logic theorem proving." SPASS+T (GPLv2) is an extension of SPASS that "enlarges the reasoning capabilities of SPASS using some built-in arithmetic simplification rules and an arbitrary SMT procedure for arithmetic and free function symbols as a black-box." Unfortunately, SPASS+T requires Yices (proprietary) or CVC Lite (license currently unacceptable to distributors due to a dangerous legal clause), so it cannot be included in the main repostitory of a typical Linux distribution.

• SRI's New Automated Reasoning Kit (SNARK) (MPL) is an "automated theorem-proving program being developed in Common Lisp. Its principal inference rules are resolution and paramodulation. SNARK's style of theorem proving is similar to Otter's [and Prover9's]. Some distinctive features of SNARK are its support for special unification algorithms, sorts, nonclausal formulas, answer construction for program synthesis, procedural attachment, and extensibility by Lisp code. SNARK has been used as the reasoning component of SRI's High Performance Knowledge Base (HPKB) system, which deduces answers to questions based on large repositories of information, and as the deductive core of NASA's Amphion system, which composes software from components to meet users' specifications, e.g., to perform computations in planetary astronomy. SNARK has also been connected to Kestrel's SPECWARE environment for software development." Note that it directly supports numbers (Prover9 does not).
• LEO-II (BSD) is a "standalone, resolution-based higher-order theorem prover designed for fruitful cooperation with specialist provers for natural fragments of higher-order logic. At present LEO-II can cooperate with the first-order automated theorem provers E, SPASS, and Vampire. LEO-II is implemented in Objective CAML and its problem representation language is TPTP THF."
• csisat (Apache 2.0 license) is a Tool for LA+EUF Interpolation. That is, it is "an interpolating decision procedure for the quantifier-free theory of rational linear arithmetic and equality with uninterpreted function symbols. Our implementation combines the efficiency of linear programming for solving the arithmetic part with the efficiency of a SAT solver to reason about the boolean structure."
• Zenon (new BSD) is an "automated theorem prover for first order classical logic (with equality), based on the tableau method. Zenon is intended to be the dedicated prover of the Focal environment, an object- oriented algebraic specification and proof system, which is able to pro- duce OCaml code for execution and Coq code for certification. Zenon can directly generate Coq proofs (proof scripts or proof terms), which can be reinserted in the Coq specifications produced by Focal. Zenon can also be extended, which makes specific (and possibly local) automation possible in Focal." Note in particular that Zenon generates proofs in a Coq-checkable format.
• Otter-λ (Otter-lambda) (MIT-style license) is "a theorem-proving program. It accepts as input a list of axioms and a theorem to try to prove, and if successful, it outputs a proof of that theorem from those axioms... Otter-λ is a first-order theorem prover (Otter) augmented by lambda calculus and an algorithm for untyped lambda unification."
• KeYmaera (GPL) is "a verification tool for hybrid systems and built as a hybrid theorem prover for hybrid systems. KeYmaera separates the overall verification workflow into two phase. In the first phase you specify the hybrid system that you would like to verify along with its correctness properties. In the second phase, you can use KeYmaera and its automatic proof strategies to verify the specified property of the hybrid system." It depends on the proprietary tool Mathematica.
• JAPE (GPL) is a configurable, graphical proof assistant. It allows user to define a logic, decide how to view proofs, and so on. It works with variants of the sequent calculus and natural deduction.
• LoTREC (CeCILL License) is "a generic tableau theorem prover for modal logic. It is a suitable educational tool for students and researchers for creating, testing and analysing tableau method implementations."
• Metis (GPLv2) is "an automatic theorem prover for first order logic with equality". Its website reports these features: "Coded in Standard ML (SML), with an emphasis on keeping the code as simple as possible; Compiled using MLton to give respectable performance on standard benchmarks; Reads in problems in the standard .tptp file format of the TPTP problem set; Outputs detailed proofs in TSTP format, where each proof step is one of 6 simple rules; Outputs saturated clause sets when input problems are discovered to be unprovable." MLton is an "open-source, whole-program, optimizing Standard ML compiler" (released under a BSD-style license).
• MaLARea (GPLv2+ except for snow) is a metasystem for "automated theorem proving in large theories where symbol and formula names are used consistently. It uses several deductive systems (now E,SPASS,Paradox,Mace), as well as complementary AI techniques like machine learning (the SNoW system) based on symbol-based similarity, model-based similarity, term-based similarity, and obviously previous successful proofs... The basic strategy is to run ATPs on problems, then use the machine learner to learn axiom relevance for conjectures from solutions, and use the most relevant axioms for next ATP attempts. This is iterated, using different timelimits and axiom limits. Various features are used for learning, and the learning is complemented by other criteria like model-based reasoning, symbol and term-based similarity, etc."
• Coq (LGPL 2.1 license) is a formal proof management system: a proof done with Coq is mechanically checked by the machine. (Coq does not create proofs for the most part, it checks and manages them.) Coq was used by Trusted Logic to evalute the Java Card (TM) system at Common Criteria EAL 7 (see Why and Krakatoa, which are FLOSS tools for verifying Java programs and can use Coq). Coq supports defining functions or predicates, stating mathematical theorems and software specifications, interactively developing formal proofs of these theorems, and checking these proofs by a small certification “kernel”. Coq is based on a logical framework called “Calculus of Inductive Constructions”. If you want to learn more about Coq, consider the book "Interactive Theorem Proving and Program Development Coq'Art: The Calculus of Inductive Constructions". There many tools that run on top of Coq, too. Coq has been used by Xavier Leroy (main developer of OCaml) to write a certified compiler ( compcert) that guarantees that semantics of a C source program is kept up to PowerPC assembly. The specification of the compiler back-end is available as GPL software (though unfortunately not the Coq proofs). Although the compcert work is not entirely FLOSS, the fact that it exists shows that complete formal methods can be applied to a nontrivial software project.
• Agda is in an interesting transition. Agda 1 (MIT license) is "an interactive proof editor, or proof assistant, developed in Chalmers University of Technology, in the tradition of succession of such proof assistants (ALF, Cayenne, Alfa). Its input language, called Agda language (or simply Agda), is based on a constructive type theory á la Martin-Löf, extended with dependent record types, inductive definitions, module structures and a class hierarchy mechanism." A research development of its successor, the Agda2 language and its interactive proof editor (MIT license, with a few pieces GPL), is going on. Agda2 is "a dependently typed programming language with good support for programming with inductively defined families of types."
• Matita (GPL, in Debian) is an "experimental, interactive theorem prover under development at the Computer Science Department of the University of Bologna. Authoring interface Matita is based on the Calculus of (Co)Inductive Constructions, and is compatible, at some extent, with Coq. It is a reasonably small and simple application, whose architectural and software complexity is meant to be mastered by students, providing a tool particularly suited for testing innovative ideas and solutions. Matita adopts a tactic based editing mode; (XML-encoded) proof objects are produced for storage and exchange. The graphical interface has been inspired by CtCoq and Proof General. It supports high quality bidimensional rendering of proofs and formulae transformed on-the-fly to MathML markup."
• E equational theorem prover (GPL license) is a high performance automatic theorem prover for full first-order logic with equality. Here's Here's another link for the E Equational Theorem prover
• PTTP (BSD-style) (Prolog Technology Theorem Prover) is a theorem prover based on model elimination. The term “Prolog” here is a little misleading; PTTP extends Prolog to the full first-order predicate calculus. There are two implementations; the Lisp version is faster (and is intended here). PTTP is extremely fast and has low memory requirements, at a cost of being unable to solve difficult theorems (the author recommends using Otter for difficult problems that are intractable for PTTP).
• Isabelle (BSD-like license) is a generic theorem proving environment developed at Cambridge University and TU Munich, building on Standard ML. It’s an “LCF-style theorem prover” -- that means its ideas are descended from the old “Logic for Computable Functions” (LCF) theorem prover, via another system called HOL (see below). In these kinds of theorem provers (including Isabelle, HOL 4, and HOL Light), you “drive” (control) how it tries to prove things using commands written in the programming language Standard ML (it does not automatically find a proof for you, but lets you command it and it does the manipulations for you).
• HOL 4 (BSD-like license) is an HOL-based automated proof system for higher order logic. Joseph A. Goguen claims that Cambridge University’s HOL (now HOL 4) is “Perhaps the most widely used theorem proving system today”. Again, you “drive” the prover using a programming language. It has support for induction and infinite data sets.
• HOL Light (BSD-like license) is similar to HOL 4 (which is derived from HOL Light), but is an unusually light theorem-proving system running on OCaml (Objective Caml). You still need to drive the program to make a proof; HOL Light includes a MESON command which is an automated proof search method called “model elimination” -- this automated search sometimes works, instead of guiding the proof by hand.
• MetaPRL (GPL license) is (1) “a general logical framework where multiple logics can be defined and related”, and (2) “a system implementation with support for interactive proof and automated reasoning”. It has a “semantic connection to programming languages, that allows the system to be used as a logical programming environment, where programs are constructed as a mixture of specifications, implementations, and verifications.” An extract from their website should explain its purpose best: “The MetaPRL system was implemented with the purpose of supporting relations between logics. There is a huge investment in formal work in systems like PVS, HOL, Coq, ELF, Nuprl, and others. These systems use different logics and different methodologies, but they have common goals and their results share fundamental mathematical underpinnings. Mathematical developments are expensive; our first goal is to expose the logical foundations that the systems share, to allow the results to be shared between systems... Work is underway to relate the PVS, HOL, Isabelle, and Nuprl mathematical foundations.” MetaPRL is part of the Cornell Prl Automated Reasoning Project, and is thus related to NuPrl. MetaPRL is built using OCaml.
• Maude Sufficient Completeness Checker (GPL license) is an experimental tool designed to check that operations are defined on all valid inputs, given a Maude-based specification (see below).
• Interactive Mathematical Proof System (IMPS) (special license, MIT-like plus requirement to identify changes) is “intended to provide organizational and computational support for the traditional techniques of mathematical reasoning. In particular, the logic of IMPS allows functions to be partial and terms to be undefined. The system consists of a database of mathematics (represented as a network of axiomatic theories linked by theory interpretations) and a collection of tools for exploring, applying, extending, and communicating the mathematics in the database.” It was developed by MITRE.
• LeanCoP (GPL license) is a compact theorem prover written in Prolog for classical first-order logic which is based on the connection calculus. It's actually only a few lines long! It's certainly not as powerful as some of the other provers listed here (although it does perform more strongly than you might expect), but its short length might make it a good starting point for special purposes, or for learning a little about how these tools work. (Originally there was no license statement, but on 2006-05-31 Jens Otten sent me an email saying he intended to license under the GPL shortly; on 2008-05-21 I confirmed that there's a license statement.)
• Gandalf (GPL license) is an automated theorem proving (ATP) system. It has won several times in the CASC contest.

I have not included some tools in this list because I can't confirm that they have a FLOSS license. Twelf has a "license" statement that doesn't give anyone the right to use the program, yet requires that users use it legally, so theoretically it's illegal to use it. I received an email that they had decided to release it under a BSD-style license, but haven't seen public evidence of that yet (hopefully that will change). MAYA (originally part of Inka, something that supports graphs and connects to various other useful components) has no license that I can find; its "mathweb" component is clearly GPL'ed, but it's unclear it's entirely GPLed, and it depends on the proprietary Allegro Common LISP. RRL has no license I can find, and I can't download it. The lesson here is that if you develop a tool, you need to clearly identify its license so that others can use it.

Formal methods: Model checkers

Here are tools that are model checkers that at least say they are FLOSS:

• Spin (Spin license, which is an issue) is a model-checking tool for formal verification of distributed software systems (using ProMeLa, its modeling language). Spin has been used in a variety of applications, e.g., to verify the control algorithms of a new flood control barrier in the Netherlands, and to verify selected algorithms for a number of space missions (including Deep Space 1, Cassini, the Mars Exploration Rovers, and Deep Impact). The big problem in model checkers is “state explosion”; Spin counters this proble using a technique called “partial order reduction”. Spin won the ACM’s prestigious Software System Award in April 2002. Here's an article about how to use Spin and Promula to verify parallel algorithms.

  However, although the front page of the Spin project says it has an open source license, and I believe that was their intent, there are significant concerns that suggest it may not be a FLOSS license at all. Spin created their own unique license, an unwise practice that is broadly discouraged (because it's so easy to get it wrong). When people create their own licenses but are serious about making them FLOSS, they generally submit it to opensource.org or the Free Software Foundation, but neither the Opensource.org license list nor the FSF license list identify the Spin license as a FLOSS license. That's rather suspicious. What's worse, the Debian-legal team noted some very serious problems with the Spin license, suggesting that it's not a FLOSS license at all. Thankfully, there are other tools available now which do not have a cloud of licensing problems hanging over them.

• DiVinE tool (libraries GPL; tools appear to be as well) is a model-checking tool for verifying concurrent systems (and is thus similar to Spin). DiVinE can itself run on a parallel distributed system, making it possible to handle larger systems than Spin can. It has its own native DiVinE modeling language, and also supports Spin’s ProMeLa language.
• Hybrid Logics Model Checker (GPL) is a model checker for the hybrid logics MCLite and MCFull.
• NuSMV 2 (LGPL license) is a model checker that is a re-implementation of SMV (so that a FLOSS version is available). NuSMV, like SMV, counters the “state explosion” problem using a construct called “BDDs”.
• Murphi (BSD-new license + must rename changed version) uses a language based on a collection of guarded commands (condition/action rules), which are executed repeatedly in an infinite loop (similar to Misra and Chandy’s Unity model). The language includes common data types (subranges, enumerated types, arrays, and records), as well as “Multiset” (for describing a bounded set of values whose order is irrelevant to the behavior) and “Scalarset” (for describing a subrange whose elements can be freely permuted). Murphi has been used to verify many hardware components and protocols.
• BLAST (Berkeley Lazy Abstraction Software Verification Tool) (BSD license) is a software model checker for C programs. BLAST checks that software satisfies behavioral properties of the interfaces it uses. Their description: "BLAST is a software model checker for C programs. The goal of BLAST is to be able to check that software satisfies behavioral properties of the interfaces it uses. BLAST uses counterexample-driven automatic abstraction refinement to construct an abstract model which is model checked for safety properties. The abstraction is constructed on-the-fly, and only to the required precision." A key limitation: It has only been tested with non-recursive programs (recursive programs require use of an untested option). It also has a licensing issue; it requires a solver, and the only ones it is written to use are Vampyre, Simplify, and Cvc. (Vampyre and Simplify aren't FLOSS; CVC was intended to be, so perhaps it will have a license change.)
• Java PathFinder (NASA Open Source Agreement) is a model checker for Java bytecode.

Formal methods: SAT Solvers

1. MiniSat (MIT license). In the SAT 2005 competition, MiniSAT all by itself won Silver in the industrial categories SAT+UNSAT and SAT. MiniSAT is a "conflict driven solver", one of main (modern) styles of SAT solvers. SatELiteGTI is the combination of SatELite (used as a preprocessor) with MiniSat (the “GTI” component). SatELiteGTI won Gold in all three industrial categories: SAT+UNSAT, SAT, and UNSAT. I cannot find the license for SatELite, but the developers are making SatELite obsolete anyway by incorporating its capabilities into their updated version of MiniSAT.
2. MarchDL (GPLv2+) is a SAT solver based on the "look-ahead" approach (one of the other main modern styles of SAT solvers). It won a prize at the 2007 SAT competition.
3. Fast SAT Solver (GPL) is a SAT solver based on genetic algorithms.
4. PicoSAT (MIT-style) is a recent and strong SAT solver. It did very well in the SAT'07 SAT Solver competition; Version 535 won the category of "satisfiable industrial instances" and came second on all industrial instances (satisfiable and unsatisfiable).
5. Vallst (Reciprocal Public License, a GPL-like but stricter OSI-certified license) is another SAT solver. It won two golds and one bronze in the SAT 2005 “world championships”.

Formal methods: SMT Solvers

The Satisfiability Modulo Theories (SMT) problem is an extension of the SAT problem (above). Basically, given expressions with boolean variables and/or predicates (functions that take potentially non-boolean values yet return boolean values), determine the conditions that would make it true (or conversely, show it's false). An SMT solver adds one or more "theories" for various predicates, e.g., it might add real numbers (adding predicates like less-than and equal-to), integers, lists, and so on. SMT solvers are sometimes implemented on top of SAT solvers.

Many other systems build on top of SMT solvers. The SMT-LIB: The Satisfiability Modulo Theories Library and SMT-COMP: The Satisfiability Modulo Theories Competition are important to many SMT solver implementors. Here is a list of SMT solvers (current and abandoned, FLOSS and not).

Examples include:

1. Ergo (Alt-Ergo) (CeCILL-C license) is an automatic theorem prover focused on program verification. It supports equational theory (=) and linear arithmetic, and it's relatively small. One significant problem is that this is licensed under the extremely rare CeCILL-C license, not the CeCILL license. I can't find a major FLOSS organization who has ruled that the CeCILL-C license is FLOSS (including the FSF, OSI, Debian, or Fedora). This license is intended to be FLOSS, but that is as yet untested.
2. Gappa (CeCILL or GPL, libraries LGPL) is a tool "intended to help verifying and formally proving properties on numerical programs dealing with floating-point or fixed-point arithmetic. It has been used to write robust floating-point filters for CGAL and it is used to certify elementary functions in CRlibm. It requires Coq support library 0.8. ("Why" can invoke Gappa.)
3. The Decision Procedure Toolkit (DPT) (Apache license) is "a system of cooperating decision procedures for answering satisfiability queries. The DPT implementation in OCaml comprises a DPLL-style SAT solver with theory-specific decision procedures".
4. Arithmetic and Boolean solver (ABSolver) (Common Public License 1.0) is a framework for combining other tools to solve mixed arithmetic and Boolean problems, and is designed to make it easy to add new solvers. ABSolver is remarkable in its ability to solve non-linear problems. However, "Efficient Solving of Large Non-linear Arithmetic Constraint Systems with Complex Boolean Structure" (Journal on Satisfiability, Boolean Modeling and Computation 1 (2007) 209–236) warns that ABSolver's "currently reported implementation uses the numerical optimization tool IPOPT (https://projects.coin-or.org/Ipopt) for solving the non-linear constraints. Consequently, it may produce incorrect results due to the local nature of the solver, and due to rounding errors."
5. Argo-lib (GPLv2) is an SMT-LIB solver. It is "a C++ library which provides a generic support for using decision procedures in automated reasoning systems and also support for several schemes for combining and augmenting decision procedures. This platform follows the SMT-lib initiative which aims at establishing a library of benchmarks for satisfiability modulo theories. ARGO-lib platform can be easily integrated into other systems, but it should also enable comparison and unifying of different approaches, evaluation of new techniques and hopefully help advancing the field. ARGO-lib follows a range of techniques and different systems. The latest version of ARGO-lib provides support for DPLL(T) scheme and for producing object-level proofs."
6. OpenSMT (GPLv3) is a "compact and open-source SMT-solver written in C++, with the main goal of making SMT-Solvers easy to understand. OpenSMT is built on top of MiniSAT (http://minisat.se)... Currently OpenSMT supports only the theory of Equality with Uninterpreted Functions [QF_UF]... In the future we plan to extend OpenSMT with other theories."
7. Fx7 (BSD-like license).
8. haRVey SMT prover has two branches: haRVey-FOL (LGPL) and haRVey-SAT (BSD license). From the website:
   • "haRVey-FOL integrates a First-Order Logic theorem prover (hence its name), i.e. the E-prover. It uses the superposition calculus as implemented by the E-prover, to determine the satisfiability of Boolean combinations of atoms with functions interpreted in a first-order theory with equality." haRVey-FOL includes a pre-processor (by Augusto Antonio Viana da Silva) that removes axioms that are not relevant for the proof of the current goal, which should make it more capable than provers without one. haRVey-FOL (aka "Harvey") depends in turn on SPASS (for some utilities) and E. Unfortunately, haRVey-FOL also depends on zchaff, which is definitely not FLOSS (and thus can't be pre-packaged into various distribution's main repositories); my hope is that a future version will be able to use miniSAT2 or some other FLOSS SAT solver.
   • "haRVey-SAT is based on congruence closure, the Nelson-Oppen framework, and rudimentary instantiation techniques to decide the satisfiability of a set of atoms written with uninterpreted symbols, linear arithmetics, some lambda-expressions, and some quantifiers. The Boolean engine is a SAT solver (zChaff or MiniSAT), hence its name." Although rv-SAT has promise, it's not appropriate for use with anything related to high assurance as of August 2008, for it says: "rv-sat is in early development stage. In particular, it is not complete for (linear) arithmetics. However, rv-sat gives only two answers: "sat" or "unsat". In the case the formula belongs to a fragment for which rv-sat is incomplete, "sat" should be understood as "rv-sat has not been able to prove unsatisfiability of the input formula". In short: "sat" should only be trusted if QF_UF. These incompleteness issues will be solved in future versions of the software."
   "Current developments aim at merging both branches, and provide one uniform tool. The main issues are the logics are different (haRVey-SAT is multi-sorted, haRVey-FOL is not) [and] there is some technical and theoretical difficulties to combine first-order provers within a Nelson-Oppen scheme. So, haRVey is still in development stage...". haRVey downloads are available (but watch out, some links are broken, so it can be hard to find).
9. STP (MIT license) is a Decision Procedure for Bitvectors and Arrays. "STP is a constraint solver (also referred to as a decision procedure or automated prover) aimed at solving constraints generated by program analysis tools, theorem provers, automated bug finders, intelligent fuzzers and model checkers. STP has been used in many research projects at Stanford, Berkeley, MIT, CMU and other universities. It is also being used at many companies such as NVIDIA, some startup companies, and by certain government agencies. The input to STP are formulas over the theory of bit-vectors and arrays (This theory captures most expressions from languages like C/C++/Java and Verilog), and the output of STP is a single bit of information that indicates whether the formula is satisfiable or not. If the input is satisfiable, then it also generates a variable assignment to satisfy the input formula. We are currently adding the theory of finite sets and the theory of uninterpreted functions to STP." There is a SourceForge home page for STP. It uses MINISAT.

Formal methods: Other Tools

Here are FLOSS tools that are don’t easily fit into the above categories:

• Alloy (GPL) implements a simple structural modeling language based on first-order logic. This is a really interesting project; its language is similar to Z, VDM, or UML constraints, but it can analyze the results completely automatically (no theorem-proving or other complexities) and display results graphically, making it unusually easy to use. The tool can generate instances of invariants, simulate the execution of operations (even those defined implicitly), and check user-specified properties of a model. “The motivation for the Alloy project was to bring to Z-style specification the kind of automation offered by model checkers. The Alloy Analyzer is designed for analyzing state machines with operations over complex states...”

  Alloy includes the Alloy Analyzer, “which is a model finder (not a model checker): given a logical formula, it finds a model of the formula. When an assertion is found to be false, the Alloy Analyzer generates a counterexample... Alloy Analyzer is essentially a compiler. It translates the problem to be analyzed into a (usually huge) boolean formula. This formula is handed to a SAT solver, and the solution is translated back by the Alloy Analyzer into the language of the model. All problems are solved within a user-specified scope that bounds the size of the domains, and thus makes the problem finite.” Because of its different approach, Alloy supports many higher-level structures (such as sets, relations, tables, and trees); “most model checking languages provide only relatively low-level data types (such as arrays and records)”. The tool is written in Java, and includes a GUI interface.

  This tool looks like it’d be very useful for specifying in some medium assurance environments, and I think it would be useful for high assurance at level 0 (with a little more strength than usual at level 0). The notation is fairly clear, and the notation is specifically designed so that assertions can be analyzed in a completely automated way (unlike today’s theorem-proving). Those are big advantages, and thus this is a good example of a “formal methods light” tool.

  However, note that it cannot prove that certain things can never happen; instead it can prove something like "X cannot happen within Y steps" (you can choose Y to be as large as you like). The phrase they use to describe it is a "model finder" approach; basically, they try to create a model that falsify the claims. Thus, while it can certainly give some confidence that the specification is right, it often cannot “prove” things to the strength that you usually want at level 1 or 2 for high assurance. Notationally, Alloy is very different from the tools called "model checking" tools; model checkers are typically designed to analyze compositions of state machines running in parallel, and usually only support arrays and records inside the state machines. In contrast, Alloy supports more abstract notations such as sets and relations. I can easily imagine this tool being combined with other tools (a theorem-prover or model checker)... this approach supports quick tests for sanity, and then you could prove in more depth if you needed to.

  Brant Hashii’s “Lessons Learned Using Alloy to Formally Specify MLS-PCA Trusted Security Architecture” describes using Alloy to model security. Pamela Zave’s “A Formal Model of Addressing for Interoperating Networks” describes using Alloy to model network addressing. A number of places use Alloy as a teaching tool as well, because its ability to easily generate graphically-displayed examples seems to help people understand its analysis results.

• Why / Caduceus / Krakatoa These are tools for verifying implementations (code, with emphasis currently on C and Java); all are released under the GPL.

  "Why" is a software verification tool; it is a general-purpose verification conditions generator (VCG) for other verification tools (including Coq and PVS), which it can call on. It can be used as a front-end for many tools, including calling out to many automated tools (so it can actually combine the results of many different tools in a useful way). On top of "Why" are two very interesting tools:

  • Caduceus is a verification tool for C programs, built on top of Why. It can even handle C programs with pointers (C pointers are notoriously hard to handle, but tools that can't handle C pointers are useless for C). At least some reports claim that Frama-C's "Jessie" tool is to replace Caduceus.
  • Krakatoa is a verification tool for Java programs, also built on top of Why.
• Frama-C (LGPL) is a framework for the development of collaborating static analyzers for the C language. Many analyzers are provided in the distribution, including a value analysis plug-in that provides variation domains for the variables of the program, and Jessie, a plug-in for computing Hoare style weakest preconditions (building on Why, above). It provides a formal behavioral specification language for C programs named ACSL. Frama-C (particularly its "Jessie" plug-in) is to eventually replace Caduceus. Like Caduceus, it can handle C pointers but currently it has trouble with unions and casts; there is work to essentially remove many of those restrictions.
• JACK: Java Applet Correctness Kit (Cecill C licence) "The Jack tool provides an environment for verification of Java and Java Card programs with JML annotations. It implements a fully automated weakest precondition calculus that generates proof obligations from annotated Java sources. Those proof obligations can be discharged using different theorem provers. An important design goal of Jack is that it is easy to use for normal Java developers, who use it to validate their own code. To allow developers to work in a familiar environment, Jack is integrated as a plugin in the eclipse IDE. Care has been taken to hide the mathematical complexity of the underlying concepts. Therefore Jack provides a dedicated proof obligation viewer, that presents the proof obligations connected to execution paths within the program. For each proof obligation, the relevant source code is highlighted. Moreover goals and hypothesis are displayed in a Java/JML like notation. Our goal is to allow formal method experts to prove the correctness of Java applets, and moreover, to allow Java programmers to obtain a high confidence in the correctness of their application. Currently proof obligations can be generated for the Simplify theorem prover (notably used by ESC/Java) and the Coq proof assistant. The Jack proof manager sends the proof obligations to the different provers, and keeps track of proven and unproven proof obligations."
• Forge / JForge (GPLv3). "Forge is a program analysis framework that allows a procedure in a conventional object oriented language to be automatically checked against a rich interface specification. The framework uses a bounded verification technique, in which all executions of a procedure are examined up to a user-provided bound on the heap and number of loop unrollings. If a counterexamples exists within the bound, Forge will find and report the complete program trace, but defects outside the bound may be missed. To facilitate modular analysis, specifications can be embedded as statements in code, an idea borrowed from the refinement calculus.

  The core Forge library... operates on programs constructed in the Forge Intermediate Representation (FIR), a simple, relational programming language. To analyze a program written in a conventional programming language, like Java or C, that program and its specification must first be encoded in FIR. We have built a command-line tool called JForge that analyzes Java code against specifications written in the Java Modeling Language (JML) by translating them both to FIR, and we have made this tool available for download as well. Others are working on a translation from C to FIR, and we welcome and encourage you to encode your own favorite language in FIR."

• Splint, formerly named LCLint (GPL license) does static analysis of C programs, and is usually used in a medium assurance mode that requires very little specification work from a developer to help find some security flaws. But splint is actually based on a long trail of research into formal methods (on “Larch” specifically), and it supports far stronger annotation and proof methods if developers choose to use them that move into high assurance.
• Daikon (MIT-style; includes some components with other OSS licenses). "Daikon is an implementation of dynamic detection of likely invariants; that is, the Daikon invariant detector reports likely program invariants. An invariant is a property that holds at a certain point or points in a program; these are often seen in assert statements, documentation, and formal specifications. Invariants can be useful in program understanding and a host of other applications... Dynamic invariant detection runs a program, observes the values that the program computes, and then reports properties that were true over the observed executions. Daikon can detect properties in C, C++, Java, Perl, and IOA programs; in spreadsheet files; and in other data sources. (Dynamic invariant detection is a machine learning technique that can be applied to arbitrary data.) It is easy to extend Daikon to other applications; as one example, an interface exists to the Java PathFinder model checker."
• Kodkod (MIT license) is a constraint solver for relational logic. It is "an efficient SAT-based analysis engine for first order logic with relations, transitive closure, and partial instances. The current prototype, which includes a finite model finder and a minimal unsatisfiable core extractor, is being used as a backend to the Karun, Forge, and Miniatur code checkers, a course scheduler, the Alloy Analyzer 4.0, a network configuration tool, etc. Unlike traditional model finders (e.g. Alloy Analyzer 3, Paradox, and MACE), Kodkod is designed to take advantage of partial instance information..."
• SATABS (BSD-old style license, but with odd notification requirement that may be non-FLOSS) is a verification tool for ANSI-C programs. It allows verifying array bounds (buffer overflows), pointer safety, exceptions and user-specified assertions.
• CCured (BSD-new license) is a “source-to-source translator for C. It analyzes the C program to determine the smallest number of run-time checks that must be inserted in the program to prevent all memory safety violations. The resulting program is memory safe, meaning that it will stop rather than overrun a buffer or scribble over memory that it shouldn’t touch.” I am skeptical that this would be used in a high assurance setting, but I can’t help but mention it.
• Deputy (revised BSD license) is "a C compiler that is capable of preventing common C programming errors, including out-of-bounds memory accesses as well as many other common type-safety errors. It is designed to work on real-world code, up to and including the Linux kernel itself. Deputy allows C programmers to provide simple type annotations that describe pointer bounds and other important program invariants. Deputy verifies that your program adheres to these invariants through a combination of compile-time and run-time checking. Unlike other tools for checking C code, Deputy provides a flexible annotation language that allows you to describe many common programming idioms without changing your data structures. As a result, using Deputy requires less programmer effort than other tools. In fact, code compiled with Deputy can be linked directly with code compiled by other C compilers, so you can choose exactly when and where to use Deputy within your C project."

  "Unlike many other safe C variants such as Cyclone and CCured, Deputy is incremental and thread safe. That is, programmers are free to add annotations and modify code function-by-function. This is possible because Deputy does not change the representation of the data visible across function boundaries, which allows “deputized” modules to interoperate with standard modules. While the initial version of the file may contain several blocks of trusted code, subsequent versions will gradually eliminate this trusted code in favor of fully annotated and checked code." [Beyond Bug-finding].

• Cyclone (GPL and LGPL) is "a safe dialect of C."
• PEP (Programming Environment based on Petri Nets) [PEP SourceForge site] (GPL) is a broad set of modelling, compilation, simulation and verification components, linked together within a Tcl/Tk-based graphical user interface. It is based on Petri Nets (which are aimed at addressing concurrency and nondeterminism).
• ManTa (GPL + public domain) is a programming/specification language, and also the name of the supporting development environment. It is fundamentally based on letting users write algebraic specifications of ADTs (abstract data types). “Its theoretical bases ensure that every program written has “mathematical meaning” (i.e. a model)” It then lets you “Evaluate expressions by using a Rewriting Motor, “Demonstrate ADT properties by using an inductive theorem prover..., [and] Generate correct code which implements an ADT in ANSI C or Ocaml.” This looks interesting, but as of May 2006 it seems to have stalled since 2001. Thankfully, any FLOSS project can get restarted by anyone else, so if there is interest, that’s all that is needed.
• FoCaL / FoCaLize (BSD-style). The FoCaL overview says "The Focal project attempts to provide a programming environment in which certified programs can be developed. This environment is based on a language including functional and object-oriented features. Moreover, this language provides means for the programmers to write formal specifications and proofs of their code, and to have them verified by a proof checker. Thanks to inheritance and refinement mechanisms, Focal allows to make several refinements of a specification until providing an efficient executable code (obtained via a translation to OCaml). Focal provides a library which implements mathematical structures up to multivariate polynomial rings and includes complex algorithms with performances comparable to the best CAS in existence."

  Another FoCaL overview adds some detail: "Focal, a joint effort with LIP6 (U. Paris 6) and Cedric (CNAM), is a programming language and a set of tools for software-proof codesign. The most important feature of the language is an object-oriented module system that supports multiple inheritance, late binding, and parameterisation with respect to data and objects. Within each module, the programmer writes specifications, code, and proofs, which are all treated uniformly by the module system. Focal proofs are done in a hierarchical language invented by Leslie Lamport. Each leaf of the proof tree is a lemma that must be proved before the proof is detailed enough for verification by Coq. The Focal compiler translates this proof tree into an incomplete proof script. This proof script is then completed by Zenon, the automatic prover provided by Focal."

  As of May 2008 it looks more like early research work, but it will probably mature over time. They seem to have focused primarily on implementing computer-aided algebra (CAS) systems so far.

• Banshee (most BSD License, some GPL) is “a toolkit that simplifies the task of building constraint-based program analyses. Program analyses are widely used in compilers and software engineering tools for discovering or verifying specific properties of software systems... the analysis designer provides a short specification file describing the kinds of constraints used in the analysis. From this specification, BANSHEE builds a customized constraint resolution engine which solves those constraints very efficiently.” Banshee is the successor of BANE (MIT license). "The pointer analysis application, which includes a C parser derived from GCC, is also included and is released under the GNU General Public License."
• iProver (GPLv3). iProver can is a general-purpose automated theorem prover, using "a modular combination of first-order reasoning with ground reasoning. In particular, iProver currently integrates MiniSat for reasoning with ground abstractions of first-order clauses... [it] can solve around 4843 problems out of 8984 in the TPTP-v3.2.0 library (with the default options)."
• Darwin (GPL). "Darwin is an automated theorem prover for first order clausal logic. It accepts problems formulated in tptp or tme format, non-clausal tptp problems are clausified using the eprover. Equality is not built into the currently implemented version of the calculus, it is instead automatically axiomatized for a given problem. Darwin is a decision procedure for function-free clause sets, and is in general faster and scales better on such problems than propositional approaches."
• Paradox (GPL license) is a tool that processes first-order logic problems and tries to find finite-domain models for them. Paradox won the SAT/Models class (generated most models) in the CASC 2003 competetion for first-order logic tools. Paradox can read problems in both TPTP and Otter syntax. It is written in Haskell, and depends on MiniSAT. Paradox is co-developed with Equinox, a first-order theorem prover.
• Proved ML (CeCILL-B license) is a variant of the ML language "which focuses both on being able to prove programs and be really usable". As of May 2008 it was not ready for serious use.
• Murphi (CMC license, BSD-like) is Finite-state Concurrent System Verifier. It was developed by David L. Dill, who's done a lot of work related to verified voting.
• Proof General (GPL) is a generic front-end for interactive theorem provers (aka "proof assistants") based on the customizable text editor Emacs. It works with Isabelle, Coq, PhoX, and LEGO, and has experimental support for other tools like HOL and ACL2.
• JMLEclipse is "an Eclipse plugin that allows the integration of JML into Eclipse's Java Development Tools (JDT)... The whole idea behind JMLEclipse is to have an open framework that can be used as frontend for different JML tools."
• Computer Algebra System (CAS). Historically, CASs have been separate programs. There are a large number of FLOSS CAS programs to choose from.

  It's worth noting the integrating program SAGE (GPL and GPL-compatible licenses), a Python-based program that integrates several CAS and other mathematical programs with the goal of "Creating a viable free open source alternative to Magma, Maple, Mathematica, and Matlab."

  Examples of specific CAS programs include:

  1. Maxima (GPL), with a GUI provided by wxMaxima (GPL). This is a large system with a very long history; it is very mature.
  2. Axiom (BSD-style library). This is a large system, also with a long history. One interesting aspect is that all values are "mathematically typed", that is, it includes a type system. "In its current state it represents about 30 years and 300 man-years of research work."
  3. Yacas (GPL). This is implemented in C++ and is designed to require relatively few resources or dependencies.
  4. GiNaC. This is meant to be embedded in C++ programs.
  5. SymPy is a simple CAS implemented in Python, where simple implementation in an easily-read language is important.
  6. GAP (Groups, Algorithms, Programming) (GPL) is a system for computational discrete algebra.
  7. Jacal (GPLv3) is "an interactive symbolic mathematics program. JACAL can manipulate and simplify equations, scalars, vectors, and matrices of single and multiple valued algebraic expressions containing numbers, variables, radicals, and algebraic differential, and holonomic functions. JACAL is a GNU package."
  8. Kayali (GPL) is a GUI front-end of a CAS system. It's a Qt-based GUI front-end to (a subset of) Maxima and gnuplot. It is implemented in Python.
• General-purpose upper ontologies. For purposes of this paper, an ontology is something that provides (1) identification of basic categories of objects (real or abstract), (2) a way of determining what kinds of entities fall into those categories, and (3) a way of determining the relationships between and among the categories. An ontology is extremely useful when handling unrestricted natural language; ontologies help you infer some of the information that is implied but unstated in ordinary text. They also help you structure problems if they have a rich set of object types. See Wikipedia's article on upper ontology and formalontology.it for more about ontologies; you should probably also know about W3C's OWL Web Ontology Language. A Comparison of Upper Ontologies (Technical Report DISI-TR-06-21) gives a brief comparison of ontologies. Some general-purpose upper ontologies are available as FLOSS:
  1. Suggested Upper Merged Ontology (SUMO) (GPL for extensions). IEEE has a working group on SUMO. For more information on SUMO, see: Niles, I., and Pease, A. 2001. Towards a Standard Upper Ontology. In Proceedings of the 2nd International Conference on Formal Ontology in Information Systems (FOIS-2001), Chris Welty and Barry Smith, eds, Ogunquit, Maine, October 17-19, 2001. SUMO's top-level item is the "Entity", which it breaks down as follows:

       Physical
          Object
              SelfConnectedObject
                 ContinuousObject
                 CorpuscularObject
              Collection
          Process
       Abstract
          SetClass
                 Relation
          Proposition
          Quantity
              Number
              PhysicalQuantity
          Attribute
     

     SUMO maps to the widely-used Wordnet (next!).
  2. Wordnet (BSD-style). is itself an ontology of words along with other information (parts of speech and definitions). Thus, Wordnet is useful as a dictionary, and it tends to be used for a lot linguistic work. Wordnet doesn't have much about interrelationships between concepts (other than synonyms/antonyms) in the way SUMO and other specs do, though, so for some purposes Wordnet is paired with other information.
  3. DOLCE - a Descriptive Ontology for Linguistic and Cognitive Engineering (LGPL) has a cognitive bias (it aims at capturing the ontological categories underlying natural language and human commonsense), and