From 18afda04e6e52e5a8c049dba75e114195b88665f Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Philipp=20Schro=CC=88er?= Date: Sat, 23 Nov 2024 12:49:34 +0100 Subject: [PATCH] website: add about page and relation to CADP --- website/docs/model-checking.md | 9 ++++ website/docusaurus.config.js | 15 ++++-- website/src/pages/about.js | 94 ++++++++++++++++++++++++++++++++++ 3 files changed, 115 insertions(+), 3 deletions(-) create mode 100644 website/src/pages/about.js diff --git a/website/docs/model-checking.md b/website/docs/model-checking.md index 48435d2..51e041d 100644 --- a/website/docs/model-checking.md +++ b/website/docs/model-checking.md @@ -5,6 +5,10 @@ description: Caesar can export models to the JANI format. # Model Checking +```mdx-code-block +import Link from '@docusaurus/Link'; +``` + Caesar has some support to export probabilistic programs written in (an executable fragment of) HeyVL to [the *jani-model* format](https://jani-spec.org/). The JANI project defines exchange formats for quantitative model checking problems (and more). @@ -21,6 +25,11 @@ The encoding is sure to change in the near future. ::: + + Note: Caesar should not be confused with the set of tools in the CADP toolbox by INRIA, which includes tools like CAESAR, CAESAR.ADT, or OPEN/CAESAR. + These also enable model checking of software, but are unrelated to this project. + + ## Usage For a simple example, consider the HeyVL program below. diff --git a/website/docusaurus.config.js b/website/docusaurus.config.js index 6b3c2f2..da703d5 100644 --- a/website/docusaurus.config.js +++ b/website/docusaurus.config.js @@ -86,12 +86,17 @@ const config = { position: 'left', label: 'Docs', }, + { + to: '/about', + position: 'left', + label: 'About', + }, + {to: '/blog', label: 'News', position: 'left'}, { href: 'https://github.com/moves-rwth/caesar', label: 'GitHub', position: 'right', }, - {to: '/blog', label: 'News', position: 'left'}, {to: '/docs/publications', label: 'Publications', position: 'right'}, ], }, @@ -114,8 +119,8 @@ const config = { to: '/docs/stdlib', }, { - label: 'pGCL', - to: '/docs/pgcl', + label: 'Proof Rules', + to: '/docs/proof-rules', }, ], }, @@ -135,6 +140,10 @@ const config = { { title: 'More', items: [ + { + label: 'About', + to: '/about', + }, { label: 'News', to: '/blog', diff --git a/website/src/pages/about.js b/website/src/pages/about.js new file mode 100644 index 0000000..4fa94b9 --- /dev/null +++ b/website/src/pages/about.js @@ -0,0 +1,94 @@ +import React from 'react'; +import Layout from '@theme/Layout'; +import Link from '@docusaurus/Link'; + +export default function About() { + return ( + +
+

About Caesar

+

+ Caesar is a deductive verification infrastructure specifically designed for probabilistic programs. + That means it is a tool to provide formal guarantees for programs that incorporate probabilistic behaviours, such as drawing random numbers or making random choices. +

+

+ Probabilistic programs can be found in randomized algorithms, communication protocols, machine learning models, and many other domains. + When designing or analyzing such programs, many questions can be formulated with respect to some kind of expected value, such as the probability of reaching a certain state, the expected number of steps until a certain event occurs, or the expected value of some variable at the end of the program. + We support the use of different proof rules, from areas such as martingale analysis or domain theory, thus enabling reasoning about programs with infinite state spaces and unbounded loops. +

+

+ Caesar aims to be a verification infrastructure that combines many different techniques to formally reason about such expected values. + We want to provide a tool that automates the verification process as much as possible, while still allowing the user to guide the verification process and provide additional information when needed. + This differs from probabilistic model checkers such as Storm or PRISM, which are more "push-button" approaches that require less user interaction but struggle with e.g. infinite state spaces. +

+ +

+ Caesar is an open-source project from RWTH Aachen University (MOVES group), Saarland University (QUAVE group), Denmark Technical University (SSE section), and University College London (PPLV group). + The source code is available on GitHub. + The name "Caesar" comes from "veni, vidi, vc", where we let "vc" stand for "verification conditions". +

+ +

Main Features

+
    +
  • Verification of expected values in probabilistic programs
    • +
  • Support for infinite state spaces, unbounded loops, and recursion
    • +
  • Support for different proof rules, such as from martingale analysis or domain theory
    • +
  • Integration with SMT solvers and probabilistic model checkers
    • +
  • Program slicing for error localization and hints
    • +
  • Integration with Visual Studio Code
    • +
+ +

Key Components

+ +

The Quantitative Intermediate Verification Language HeyVL

+

+ The architecture of Caesar is inspired by modern program verifiers that use an intermediate verification language (IVL) to encode a program, its specification, and proof rules into a common representation. + Our quantitative IVL is called HeyVL. + HeyVL generalizes classical IVLs to the quantitative setting through HeyLo, our new quantitative logic developed for Caesar. + The names come from Heyting algebras, which underlie the logic. +

+

+ In Caesar, HeyVL also has high-level constructs such as loops or procedure calls, but these are all encoded into a smaller core language. + This core language and many encodings are described in our OOPSLA 2023 publication "A Deductive Verification Infrastructure for Probabilistic Programs". +

+ +

Backends: SMT Solving and Probabilistic Model Checking

+

+ Caesar uses the Z3 SMT solver to reason about HeyVL programs. + This allows Caesar to use symbolic reasoning to prove properties of probabilistic programs, enabling reasoning about infinite state spaces and unbounded loops. + It is also possible to use other SMT solvers (by emitting SMT-LIB). +

+

+ In addition, Caesar has a model checking backend that emits files in the JANI format, a JSON-based interchange format for probabilistic models. + This is possible for an "executable" subset of HeyVL programs that can be translated into JANI models. + The result can be fed into probabilistic model checkers such as Storm. +

+ +

Slicing for Error Localization and Hints

+

+ Caesar includes a program slicing engine called Brutus (get it?) that reduces HeyVL programs with respect to certain properties. + Slicing is Caesar's theoretical and practical foundation for error localization and hints. + For example, by removing assertions from the program, we can find out the remaining assertions which must cause a verification failure. +

+ +

Visual Studio Code Integration

+

+ We value usability and user-friendliness highly and want to make Caesar as easy to use as possible. + It is our belief that UX is a key factor in making formal verification succeed in practice. + This is why we put a lot of effort into integrating Caesar with Visual Studio Code with our Caesar for VSCode extension. +

+ +

Disclaimer: (Un)Related Work

+

+ Caesar should not be confused with the set of tools in the CADP toolbox by INRIA, which includes tools like the CAESAR or CAESAR.ADT compilers, or the OPEN/CAESAR software architecture. +

+
+ + ); +} \ No newline at end of file