HOL4P4: semantics for a verified data plane .
A Case Study in Information Flow Refinement for Low Level Systems .
Formally Verified Isolation of DMA .
Foundations and Tools in HOL4 for Analysis of Microarchitectural Out-of-Order Execution .
Secure Partitioning of Composite Cloud Applications .
Validation of Side-Channel Models via Observation Refinement .
Refinement-Based Verification of Device-to-Device Information Flow .
ROOSTERIZE: Suggesting Lemma Names for Coq Verification Projects Using Deep Learning.
P Nie, K Palmskog, JJ Li, M Gligoric.
2021 IEEE/ACM 43RD INTERNATIONAL CONFERENCE ON SOFTWARE ENGINEERING: COMPANION PROCEEDINGS (ICSE-COMPANION 2021), Institute of Electrical and Electronics Engineers (IEEE).
2021.
On compositional information flow aware refinement .
PomCho: A tool chain for choreographic design.
R Guanciale, E Tuosto.
Science of Computer Programming.
2021.
Inspectre: Breaking and fixing microarchitectural vulnerabilities by formal analysis .
On testing message-passing components.
A Coto, R Guanciale, E Tuosto.
International Symposium on Leveraging Applications of Formal Methods.
2020.
An abstract framework for choreographic testing.
A Coto, R Guanciale, E Tuosto.
arXiv preprint arXiv:2009.07990.
2020.
Hoare-style logic for unstructured programs .
Validation of abstract side-channel models for computer architectures .
Speculative Leakage in ARM Cortex-A53 .
Trustworthy isolation of DMA devices .
Towards a Verified Model of the Algorand Consensus Protocol in Coq .
Trustworthy Isolation of DMA Enabled Devices .
On the verification of system-level information flow properties for virtualized execution platforms .
TrABin: Trustworthy Analyses of Binaries .
Trustworthy Memory Isolation of Linux on Embedded Devices .
Master's Thesis
