From 9439a5405216a8603d1da27f0cf36f77e3d31b28 Mon Sep 17 00:00:00 2001 From: Michael Tautschnig Date: Tue, 14 Feb 2023 14:04:40 +0100 Subject: [PATCH] Clarify the analysis technique used by Kani (#2195) --- docs/src/getting-started.md | 6 ++++-- docs/src/limitations.md | 3 ++- 2 files changed, 6 insertions(+), 3 deletions(-) diff --git a/docs/src/getting-started.md b/docs/src/getting-started.md index 3f43d31f29d9..4377c0b91106 100644 --- a/docs/src/getting-started.md +++ b/docs/src/getting-started.md @@ -1,9 +1,11 @@ # Getting started -Kani is an open-source verification tool that uses automated reasoning to analyze Rust programs. +Kani is an open-source verification tool that uses [model checking](./tool-comparison.md) to analyze Rust programs. Kani is particularly useful for verifying unsafe code in Rust, where many of the Rust’s usual guarantees are no longer checked by the compiler. Some example properties you can prove with Kani include memory safety properties (e.g., null pointer dereferences, use-after-free, etc.), the absence of certain runtime errors (i.e., index out of bounds, panics), and the absence of some types of unexpected behavior (e.g., arithmetic overflows). Kani can also prove custom properties provided in the form of user-specified assertions. +As Kani uses model checking, Kani will either prove the property, disprove the +property (with a counterexample), or may run out of resources. Kani uses proof harnesses to analyze programs. Proof harnesses are similar to test harnesses, especially property-based test harnesses. @@ -15,7 +17,7 @@ Releases are published [here](https://github.com/model-checking/kani/releases). Major changes to Kani are documented in the [RFC Book](https://model-checking.github.io/kani/rfc). There is support for a fair amount of Rust language features, but not all (e.g., concurrency). -Please see [Limitations - Rust feature support](./rust-feature-support.md) for a detailed list of supported features. +Please see [Limitations](./limitations.md) for a detailed list of supported features. Kani releases every two weeks. As part of every release, Kani will synchronize with a recent nightly release of Rust, and so is generally up-to-date with the latest Rust language features. diff --git a/docs/src/limitations.md b/docs/src/limitations.md index 993d7cecd48c..46be19c73fb6 100644 --- a/docs/src/limitations.md +++ b/docs/src/limitations.md @@ -1,7 +1,8 @@ # Limitations Like other tools, Kani comes with some limitations. In some cases, these -limitations are inherent because of the techniques it's based on. In other +limitations are inherent because of the techniques it's based on, or the +undecidability of the properties that Kani seeks to prove. In other cases, it's just a matter of time and effort to remove these limitations (e.g., specific unsupported Rust language features).