George Pîrlea

I am second-year PhD student at the National University of Singapore, supervised by Ilya Sergey, currently on leave from work for health reasons.
Expect long delays for responses when emailing.
Get in touch via email: george@pirlea.net
Follow me on Twitter: @GeorgePirlea
Google Scholar: George Pîrlea
What's new
Feb 4 | I am away from office for health reasons. |
Publications
- 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.
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
- 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).
© 2022 George Pîrlea ― last updated on 2022-02-04 at 05:38 UTC