Search results

Make run_tests print a warning when skip_proofs is set in .isabelle/etc

build systemrelated to building the proofs or kernelrelated to building the proofs or kernel

enhancement

Status: Open.

Feature

#905 In seL4/l4v;

· Xaphiosis opened on Jun 25, 2025



Improve formalisation of the reply objects and the reply stack

enhancement

MCSrelated to `rt` branch and mixed-criticality systemsrelated to `rt` branch and mixed-criticality systems

Status: Open.

#877 In seL4/l4v;

· michaelmcinerney opened on Mar 31, 2025

1 comment

Consolidate the various approaches we have to projecting from the kernel heap

cleanup

enhancement

MCSrelated to `rt` branch and mixed-criticality systemsrelated to `rt` branch and mixed-criticality systems

proof engineeringnicer, shorter, more maintainable etc proofsnicer, shorter, more maintainable etc proofs

Status: Open.

Task

#841 In seL4/l4v;

· michaelmcinerney opened on Dec 13, 2024

6 comments

Enhance C Parser to allow named array bounds

C-parseranything about the C/Simpl parseranything about the C/Simpl parser

enhancement

proof toolsconvenience, automation, productivity toolsconvenience, automation, productivity tools

Status: Open.

#754 In seL4/l4v;

· Xaphiosis opened on May 22, 2024

3 comments

Investigate further use of none_top/none_bot in the proofs

enhancement

proof engineeringnicer, shorter, more maintainable etc proofsnicer, shorter, more maintainable etc proofs

Status: Open.

#751 In seL4/l4v;

· michaelmcinerney opened on May 1, 2024

Safer vcg in CRefine

enhancement

proof engineeringnicer, shorter, more maintainable etc proofsnicer, shorter, more maintainable etc proofs

Status: Open.

#726 In seL4/l4v;

· Xaphiosis opened on Mar 1, 2024

Methods such as monadic_rewrite_symb_exec_r should warn that discharging side-conditions failed

enhancement

proof engineeringnicer, shorter, more maintainable etc proofsnicer, shorter, more maintainable etc proofs

Status: Open.

#715 In seL4/l4v;

· Xaphiosis opened on Feb 15, 2024

SIMPL: don't print _'proc

C-parseranything about the C/Simpl parseranything about the C/Simpl parser

enhancement

Status: Open.

#710 In seL4/l4v;

· lsf37 opened on Jan 23, 2024

missing error message for 0-length array

C-parseranything about the C/Simpl parseranything about the C/Simpl parser

enhancement

Status: Open.

#303 In seL4/l4v;

· lsf37 opened on Jul 5, 2021