Introduction about Calysto

Calysto is a scalable and precise static checker for general purpose code, as it is written today — meaning that it does not require users to write interface specifications and pre/post-conditions. Calysto checks pointer properties and user provided assertions.

Calysto works on the SSA form, and as such is language independent. However, interpretation of library functions (like C-lib and STL) as well as trace reporting is language-dependent (for instance, demangling C++ and Java names). Currently, trace reports are readable only for languages that do not mangle names (like C).

Since specifications rarely exist, and software is usually a flux of synchronizations between the actual code and mental models of all the programmers working on the project, it is a bit inappropriate to claim that general applications, like Linux kernel, can be formally verified. So, I consider Calysto a bug hunting companion, rather than a formal verification tool.

Story

Callisto was a hunting companion of Artemis — goddess of hunt in Greek mythology. Calysto is an intentionally misspelled version (so that it’s easier to find).

Main Features

• Calysto runs on Single Static Assignment (SSA) form, and as such is language independent. Only the rule files will need to be specified independently for each language-library combination.
• Calysto is bit-precise, path-sensitive, context-sensitive, and field-sensitive (what I call *-sensitive).
• Calysto currently handles loops and pointer arithmetic in an unsound manner, but that will change in the future, at least for some classes of loops. The basic framework is flexible enough to be extended.
• Calysto exploits structure available in the software at several levels of granularity, which significantly improves the scalability.
• Calysto is based on the LLVM compiler framework.
• Calysto owns a lot of its scalability to close integration with the Spear.

Calysto-generated Verification Conditions

Calysto-generated benchmarks are downloadable from the SMT-LIB website, under Benchmarks, QF_BV category. Benchmarks are named Spear benchmarks, although, more accurately, they should have been named Calysto benchmarks. Using Spear and Spear tools, SMT-LIB benchmarks can be converted into various formats, like DIMACS CNF and Spear format.

Availability

I'm not planning to make Calysto available. The focus of my research was on solving the technical problems, not on making the tool user friendly, so understanding the reports requires deep understanding of how the tool works. Thus, supporting the tool would be extremely time-demanding. With significantly more (engineering) work, this could have been solved in a more user-friendly manner. Also, I haven't been working on Calysto for quite a while, so it's out of sync with LLVM. While I was at Cadence, I was planning to make an improved production version of Calysto, but those plans were axed by the unfortunate downsizing.

If you want to find out more about Calysto, check out my thesis, the CAV07 structural abstraction paper, and the ICSE08 Calysto paper.

Acknowledgments

I'd like to thank numerous people that helped me during Calysto development and testing. Harlan Stenn from ISC provided incredibly quick and detailed feedback on the NTP bug reports that Calysto generated. Jesse Smith did the same for Bftpd. I also received feedback from numerous other developers, to which I'm all grateful.