Stephan Merz

Latest

• A Rigorous Correctness Proof for Pastry
• Encoding TLA + + into Many-Sorted First-Order Logic
• Proving Determinacy of the PharOS Real-Time Operating System