Expand description
Formally Verified IPC
Model-checking and proof harnesses for IPC channel correctness, including FIFO ordering, message conservation, channel isolation, buffer bounds, capability enforcement, and deadlock freedom via wait-for graph analysis.
Structs§
- Async
Ring Buffer - Async ring buffer model for verification
- IpcChannel
Model - Model of an IPC channel for verification
- IpcInvariant
Checker - IPC invariant checker that validates channel properties
- IpcMessage
- A message in the IPC channel model
- Notification
- Notification model for delivery verification
- Shared
Region - Model for shared memory regions (zero-copy verification)
- Wait
Graph - Wait-for graph for deadlock detection
Enums§
- IpcModel
Error - Errors in the IPC model
- Message
Type - Message type tags for type safety verification