5 papers
NoC-Out: A Formally-verified Network-on-Chip Library for Rule-based Hardware Designs
Max Kurze, František Farka, Sebastian Ertel
The Network-on-Chip (NoC) is the communication backbone of any multiprocessor chip. A failure of the NoC has severe consequences for the whole system. Yet, no approach exists that…
Harnessing Code Agents for Automatic Software Verification
Shuangxiang Kan, Shuanglong Kan, Sebastian Ertel
Formal verification offers the strongest guarantee of software correctness, but it does not scale: the proofs demanded by interactive theorem provers such as Coq require enormous e…
Interaction Tree Semantics for RISC-V: Bridging Compiler and Hardware Verification
Shuanglong Kan, Sebastian Ertel
The Instruction Set Architecture (ISA) is the contract between compilers and processors; proving this contract formally demands cross-level connection to existing mechanized compil…
Formally-verified Security against Forgery of Remote Attestation using SSProve
Sara Zain, Jannik Mähn, Stefan Köpsell +1
Remote attestation (RA) is the foundation for trusted execution environments in the cloud and trusted device driver onboarding in operating systems. However, RA misses a rigorous m…
On the mean field theory of Ensemble Kalman filters for SPDEs
Sebastian Ertel
This paper is concerned with the mathematical analysis of continuous time Ensemble Kalman Filters (EnKBFs) and their mean field limit in an infinite dimensional setting. The signal…