From 2973b6c0ba70bfc109303517a25e7626d4eb27be Mon Sep 17 00:00:00 2001 From: Christopher Pulte Date: Wed, 5 Jun 2024 10:59:44 +0100 Subject: [PATCH] Update tutorial.adoc --- src/tutorial.adoc | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/tutorial.adoc b/src/tutorial.adoc index bb973cc7..409da17b 100644 --- a/src/tutorial.adoc +++ b/src/tutorial.adoc @@ -44,7 +44,7 @@ body > .sourceCode { // __________________________________________________________________________ -= CN tutorial += CN tutorial (work in progress) CN is a type system for verifying C code, focusing especially on low-level systems code. Compared to the normal C type system, CN checks not only that expressions and statements follow the correct typing discipline for C-types, but also that the C code executes _safely_ — does not raise C undefined behaviour — and _correctly_ — according to strong user-defined specifications. To accurately handle the complex semantics of C, CN builds on the https://github.com/rems-project/cerberus/[Cerberus semantics for C].