RM/AVM

Information flow properties This category is for discussing information flow properties based on totally ordered sequences of messages (refining the partial order of messages in a message sequence chart). The relation to information flow control is as follows.[1] Information flow control An information flow control mechanism is an enforcement mechanism that ensures the behaviour of a system satisfies an information flow property. Execution proof This category is dedicated to discussing the succinct proof that verifies out-of-circuit checks required by the resource machine. Proof aggregation