Puss in Boots: Formalizing Arm's Virtual Memory System Architecture.
IEEE Micro, 2024
RTL2MμPATH: Multi-μPATH Synthesis with Applications to Hardware Security Verification.
Proceedings of the 57th IEEE/ACM International Symposium on Microarchitecture, 2024
Abstraction for Crash-Resilient Objects.
Proceedings of the Programming Languages and Systems, 2022
Elastic Indexes: Dynamic Space vs. Query Efficiency Tuning for In-Memory Database Indexing.
Proceedings of the 25th International Conference on Extending Database Technology, 2022
Taming x86-TSO persistency.
Proc. ACM Program. Lang., 2021
Abstraction for Crash-Resilient Objects (Extended Version).
CoRR, 2021
Speculative taint tracking (STT): a comprehensive protection for speculatively accessed data.
Commun. ACM, 2021
Proving highly-concurrent traversals correct.
Proc. ACM Program. Lang., 2020
Taming x86-TSO Persistency (Extended Version).
CoRR, 2020
Privatization-Safe Transactional Memories (Extended Version).
CoRR, 2019
Privatization-Safe Transactional Memories.
Proceedings of the 33rd International Symposium on Distributed Computing, 2019
Proving consistency of concurrent data structures and transactional memory systems.
PhD thesis, 2018
Safe privatization in transactional memory.
Proceedings of the 23rd ACM SIGPLAN Symposium on Principles and Practice of Parallel Programming, 2018
Proving Linearizability Using Partial Orders (Extended Version).
CoRR, 2017
Proving Linearizability Using Partial Orders.
Proceedings of the Programming Languages and Systems, 2017
A Generic Logic for Proving Linearizability (Extended Version).
CoRR, 2016
A Generic Logic for Proving Linearizability.
Proceedings of the FM 2016: Formal Methods, 2016
ACM SIGSOFT Softw. Eng. Notes, 2012