len0rd/FreeRTOS-Kernel
1
0
Fork 0
mirror of https://github.com/FreeRTOS/FreeRTOS-Kernel.git synced 2025-12-11 14:15:12 -05:00
Code Issues Projects Releases Packages Wiki Activity
FreeRTOS-Kernel/Test/VeriFast/tasks/vTaskSwitchContext/proof
History
Tobias Reinhard 17004fbf1b Deleted the old explanation of reusing list proofs.
2022-12-29 14:30:13 -05:00
..
single_core_proofs Removed deprecated TODOs. 2022-12-28 12:33:02 -05:00
single_core_proofs_extended Handled minor TODOs in proof headers. 2022-12-28 10:40:32 -05:00
lock_predicates.h Removed comments. 2022-12-28 13:12:42 -05:00
port_contracts.h Handled minor TODOs in proof headers. 2022-12-28 10:40:32 -05:00
README.md Deleted the old explanation of reusing list proofs. 2022-12-29 14:30:13 -05:00
ready_list_predicates.h Handled minor TODOs in proof headers. 2022-12-28 10:40:32 -05:00
stack_predicates.h Renamed predicate stack_p_2 into stack_p 2022-12-13 10:57:41 -05:00
task_predicates.h Added documentation of the locking discipline and renamed some predicates. 2022-12-28 13:11:55 -05:00
task_running_states.h Renamed proof headers. Removed "verifast" prefix where unnecessary. 2022-12-28 10:12:08 -05:00
verifast_lists_extended.h Deleted unnecessary list axioms. 2022-12-28 10:47:33 -05:00

README.md

This directory contains the bulk of VeriFast formalizations and proofs.

Directory Structure

├── *.h files
│   Headers containing VeriFast formalizations and proofs.
│
├── README.md
│   Contains more details about the proof.
│
├── single_core_proofs
│   Contains the old list formalization and proofs written by
│   Aalok Thakkar and Nathan Chong in 2020 for the single-core
│   setup.
│   │
│   ├── scp_common.h
│   │   Contains auxiliary definitions and lemmas.
│   │
│   └── scp_list_predicates.h
│       Contains the formalizaton of doubly linked lists and list items.
│
└── single_core_proofs_extended
    Contains new proofs extending the single-core list
    formalization.