I am a first-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: email@example.com
Follow me on Twitter: @GeorgePirlea
Google Scholar: George Pîrlea
|Oct 22||I served on the POPL21 Artifact Evaluation Committee.|
|Aug 9||I joined Ilya Sergey's group at the NUS School of Computing. Very exciting!|
- 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.
- 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.
- 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).
© 2020 George Pîrlea ― last updated on 2020-11-05 at 01:59 UTC