Tobias Reiher

### Motivation - Enable creation of automatically provable SPARK code (e.g., prevent access to uninitialized variables, statically false conditions, length-mismatches in message instantiations) ### Description - Enhance type system (e.g.,...

Ensure existence of message fields in checksum specification

1

The parameters of a checksum specification should be verified. A checksum specification referring to non-existing message fields should be rejected. ### Example The following specification should be rejected, as `Foo`,...

Constant values in a checksum specification could indicate errors in the specification and should lead to a warning. ### Example ```ada package Checksum_Message is type A is mod 2 **...

The verification of complex specifications is time-consuming. The model verification should be parallelized to reduce the required time.

A built-in syntax for defining padding fields could simplify message specifications. Due to the semantics of reserved/padding fields (cf. #601), opaque fields are not the optimal solution. In the SPDM...

Ensure that session state is not changed by user-defined function

2

The private part of the session context contains the current state of the state machine and the state of the memory allocator. The context is a tagged type. ```Ada type...

Nested expressions are rarely supported in state actions. A workaround for this limitation is the use of separate assignments for the nested expressions (e.g., `T := M.F; F (T);` instead...