George Pîrlea
I am a fifth-year PhD student at the National University of Singapore, supervised by Ilya Sergey.
My interests include formal methods, programming languages, distributed systems, and cryptography.
Get in touch via email: george@pirlea.net
Follow me on Twitter: @GeorgePirlea
Google Scholar: George Pîrlea
What's new
7 Aug 2024 | I have been awarded the Dean's Graduate Research Excellence Award. |
5 July 2024 | Our paper on compositional verification of Byzantine protocols is accepted at CCS'24. |
13 Dec 2023 | Our work on verifying tree clocks in Coq will be presented at CPP'24 in London. |
Publications
- Qiyuan Zhao, Compositional Verification of Composite Byzantine Protocols. In Proceedings of the 31st ACM Conference on Computer and Communications Security (CCS 2024). October 2024. ACM. , Karolina Grzeszkiewicz, Seth Gilbert, Ilya Sergey.
- Qiyuan Zhao, Rooting for Efficiency: Mechanised Reasoning about Array-Based Trees in Separation Logic. In Proceedings of the 13th ACM SIGPLAN International Conference on Certified Programs and Proofs (CPP 2024). January 2024. ACM. (Distinguished Paper Award) , Zhendong Ang, Umang Mathur, and Ilya Sergey.
- Ruijie Meng*, Greybox Fuzzing of Distributed Systems. In Proceedings of the 2023 ACM SIGSAC Conference on Computer and Communications Security (CCS 2023). November 2023. ACM. , Abhik Roychoudhury, and Ilya Sergey.
- Yasunari Watanabe, Kiran Gopinathan, Certifying the Synthesis of Heap-Manipulating Programs. In Proc. ACM Program. Lang. 5 (ICFP 2021). August 2021. ACM. , Nadia Polikarpova, and Ilya Sergey.
- Practical Smart Contract Sharding with Ownership and Commutativity Analysis. In 42nd ACM SIGPLAN International Conference on Programming Language Design and Implementation (PLDI 2021). Virtual, Canada. June 2021. ACM. , Amrit Kumar, and Ilya Sergey.
- Mechanising Blockchain Consensus. In 7th ACM SIGPLAN International Conference on Certified Programs and Proofs (CPP 2018). Los Angeles, CA, USA, January 2018. ACM. and Ilya Sergey.
Drafts
- Vladimir Gladshtein, Small Scale Reflection for the Working Lean User. Unpublished draft. arXiv:2403.12733. , Ilya Sergey.
Teaching
- CS3243 Introduction to Artificial Intelligence (AY 2020/21 Sem 2)
- YSC3208 Programming Language Design and Implementation (AY 2020/21 Sem 1)
Theses
- Toychain: Formally Verified Blockchain Consensus
MEng Thesis. Advised by Earl Barr and Ilya Sergey.
Abstract: We present Toychain, the first proven-correct implementation of a Nakamoto-style blockchain consensus protocol. We improve our original model by removing several overly-strong assumptions, notably the assumption that hashing is injective. Then, we instantiate the model with a SHA256-based proof-of-work scheme and extract our proven-correct OCaml implementation of Nakamoto consensus. Finally, we execute our implementation on a local area network to test its effectiveness.
Selected talks
- Practical Smart Contract Sharding with Ownership and Commutativity Analysis
Given at PLDI (June 2021) and Formal Reasoning about Financial Systems Workshop (September 2022). - A Formal Model of Rust's Pinning
Given at Max Planck Institute for Software Systems (September 2019). - Formally Verified Blockchain Consensus
Given at National University of Singapore (March 2019), Zilliqa Research (March 2019), and Max Planck Institute for Software Systems (June 2019). - Formally Verifying Coco
Given at Microsoft Research Cambridge (August 2018). - Mechanising Blockchain Consensus
Given at CPP (January 2018) and Microsoft Research Cambridge (June 2018).
© 2024 George Pîrlea ― last updated on 2024-08-28 at 08:12 UTC