4th Program Analysis and Verification on Trusted Platforms (PAVeTrust) Workshop

The workshop provides a venue where academics and practitioners promote: (A) the application of formal methods, and more specifically of program analysis and verification, to the specification and/or analysis of the trusted stack executing these TEE-hardened applications - this stack might include CPU microcode, firmware code, Operating System (OS) code, protocols for provisioning and attestation, and the application itself - and (B) innovative applications of TEEs to execute formal methods technologies (such as program analysers/verifiers).

The workshop will be held at FM 2024 this year.