viperproject / VerifiedSCION

Verifying the SCION architecture using Gobra
Apache License 2.0
10 stars 2 forks source link

Enable `conditionalizePermissions` for the `router` #340

Closed jcp19 closed 4 months ago

jcp19 commented 4 months ago

Marco observed that a long time is spent on (sequential) pure function verification in the router package. He also suggested that using conditionalizePermissions might reduce the number of branches in these functions (moreJoins 1 does not have any effect on pure functions), which might speed up verification.