Search results

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

make defs take attributes?

cleanup

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

Status: Open.

#872 In seL4/l4v;

· lsf37 opened on Mar 21, 2025

consolidate equations between ASpec/Haskell constants into one theory

Status: Open.

#858 In seL4/l4v;

· lsf37 opened on Feb 26, 2025

eliminate get_tcb

cleanup

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

Status: Open.

Task

#854 In seL4/l4v;

· lsf37 opened on Feb 17, 2025

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

Change lemmas to be state_ext where possible instead of det_ext

cleanup

Status: Open.

#839 In seL4/l4v;

· corlewis opened on Dec 12, 2024

Remove etcb_at

cleanup

Status: Open.

#838 In seL4/l4v;

· corlewis opened on Dec 12, 2024

consolidate definitions of tcbs_of'

cleanup

Status: Open.

#806 In seL4/l4v;

· lsf37 opened on Jul 30, 2024



Remove or alter use of stateAssert

cleanup

Status: Open.

#787 In seL4/l4v;

· michaelmcinerney opened on Jul 11, 2024

port haskell translator improvements from rt to master

cleanup

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

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

Status: Open.

#783 In seL4/l4v;

· lsf37 opened on Jul 9, 2024

Should we reduce DSpec to sys-init operations only?

Status: Open.

#767 In seL4/l4v;

· lsf37 opened on Jun 18, 2024

3 comments

support strongest-postcondition reasoning

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

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

Status: Open.

#763 In seL4/l4v;

· lsf37 opened on Jun 5, 2024

1 comment

take L4V_PLAT into account in rebuilds

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

Status: Open.

#762 In seL4/l4v;

· lsf37 opened on Jun 4, 2024



Can Isabelle's custom functions and data types be combined with the C-parser?

question

Status: Open.

#756 In seL4/l4v;

· riyuejiuzhao opened on May 24, 2024

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

Some way of blocking simp from unifying schematics

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

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

Status: Open.

#730 In seL4/l4v;

· Xaphiosis opened on Mar 7, 2024

1 comment

Have wp warn when resulting in a goal with a schematic assumption.

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

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

Status: Open.

#729 In seL4/l4v;

· Xaphiosis opened on Mar 7, 2024

15 comments

Sub-term to free variable lifting tactic

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

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

Status: Open.

#727 In seL4/l4v;

· Xaphiosis opened on Mar 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

Document mysterious useful comments for ctac and ceqv

cleanup

docsDocumentation, READMEs, etcDocumentation, READMEs, etc

Status: Open.

#692 In seL4/l4v;

· Xaphiosis opened on Oct 27, 2023



Cleanup post-x64 comments

cleanup

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

Status: Open.

#691 In seL4/l4v;

· Xaphiosis opened on Oct 27, 2023

Cleanup CRefine Wellformed_C

cleanup

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

Status: Open.

#690 In seL4/l4v;

· Xaphiosis opened on Oct 27, 2023