9 citations · 10 across the 4 of their papers we have counts for
6 papers
Domain Reasoning in TopKAT
Cheng Zhang, Arthur Azevedo de Amorim, Marco Gaboardi
TopKAT is the algebraic theory of Kleene algebra with tests (KAT) extended with a top element. Compared to KAT, one pleasant feature of TopKAT is that, in relational models, the to…
Finite-memory Strategies for Almost-sure Energy-MeanPayoff Objectives in MDPs
Mohan Dantam, Richard Mayr
We consider finite-state Markov decision processes with the combined Energy-MeanPayoff objective. The controller tries to avoid running out of energy while simultaneously attaining…
On Pitts' Relational Properties of Domains
Arthur Azevedo de Amorim
Andrew Pitts' framework of relational properties of domains is a powerful method for defining predicates or relations on domains, with applications ranging from reasoning principle…
The Meaning of Memory Safety
Arthur Azevedo de Amorim, Catalin Hritcu, Benjamin C. Pierce
We give a rigorous characterization of what it means for a programming language to be memory safe, capturing the intuition that memory safety supports local reasoning about state.…
Beyond Good and Evil: Formalizing the Security Guarantees of Compartmentalizing Compilation
Yannis Juglaret, Catalin Hritcu, Arthur Azevedo de Amorim +2
Compartmentalization is good security-engineering practice. By breaking a large software system into mutually distrustful components that run with minimal privileges, restricting t…
Towards a Fully Abstract Compiler Using Micro-Policies: Secure Compilation for Mutually Distrustful Components
Yannis Juglaret, Catalin Hritcu, Arthur Azevedo de Amorim +3
Secure compilation prevents all low-level attacks on compiled code and allows for sound reasoning about security in the source language. In this work we propose a new attacker mode…