|
I am an Assistant Professor of Computer Science at National University of Singapore's
School of Computing.
I do research in verification, semantic models,
machine-checked proof, and computer security. Particular areas of
recent interest are verifying graph-manipulating programs, certified decision procedures, parallel programming, and
cryptocurrencies.
News
I am on the program committee for
APLAS 2022!
Publication (CAV 2021)
Functional Correctness of C
Implementations of
Dijkstra's, Kruskal's, and
Prim's Algorithms
with Anshuman Mohan and Wei Xiang Leow
I am on the program committee for
BSCT 2021!
Paper (January 2021)
A Partition Resilient
Overlay Network via Blockchain
with Vijeth Aradhya and Seth Gilbert
I am on the program committee for
ESOP 2022!
I was a moderator for
ICFP 2020!
I am on the program committee for
BSCT 2020!
Publication (CAV 2020)
Reasoning over
Permissions Regions in Concurrent
Separation Logic
with James Brotherston, Diana Costa, and
John Wickerson
Student (January 2020)
Shengyi Wang has defended his thesis!
Paper (January 2020)
A Machine-Checked C
Implementation of Dijkstra's
Shortest Path Algorithm
with Anshuman Mohan and Shengyi Wang
Publication (USENIX Security 2020)
BesFS: A POSIX Filesystem for
Enclaves with a
Mechanized Safety Proof
with Shweta Shinde, Shengyi Wang, Pinghai Yuan,
Abhik Roychoudhury, and Prateek Saxena
Publication (CPP 2020)
A Functional Proof Pearl:
Inverting the Ackermann
Hierarchy
with Linh Tran and Anshuman Mohan
Publication (APLAS 2019)
Pumping, With or Without
Choice
with Elaine Li and Frank Stephan
Poster (APLAS 2019)
A Certified Version of
Dijkstra's Shortest-Path
with Anshuman Mohan
Presentation (NIER 2019)
A Verified Garbage Collector
for Gallina
with Shengyi Wang, Anshuman Mohan,
and Qinxiang Cao
Publication (OOPSLA 2019)
Certifying Graph-Manipulating C Programs via
Localizations within Data Structures
with Shengyi Wang, Qinxiang Cao,
and Anshuman Mohan
Poster (OOPSLA 2019)
Certifying Graph-Manipulating C Programs
with Shengyi Wang, Qinxiang Cao,
and Anshuman Mohan
Publication (ISSTA 2019)
Exploiting the Laws of Order
in Smart Contracts
with Ivica Nikolic, Aashish Kolluri, Ilya Sergey,
and Prateek Saxena
I am on the program committee for
BSCT 2019!
I am on the program committee for
APLAS 2019!
Presentation (NIER 2018)
Temporal Properties of Smart Contracts
with Ilya Sergey and Amrit Kumar
Publication (ACSAC 2018)
Finding the
Greedy, Prodigal, and Suicidal Contracts
at Scale
with Ivica Nikolic, Aashish Kolluri, Ilya Sergey,
and Prateek Saxena
Publication (APLAS 2018)
Complexity Analysis of Tree Share Structure
with Xuan Bach Le and Anthony W. Lin
Publication (ISoLA 2018)
Temporal Properties of Smart Contracts
with Ilya Sergey and Amrit Kumar
I am on the program committee for
CPP 2019!
I am on the program committee for
BSCT 2018!
I am on the program committee for
APLAS 2018!
Publication (ESOP 2018):
Logical Reasoning over Disjoint Permissions
with Xuan Bach Le
Paper (January 2018)
SCILLA: a Smart Contract
Intermediate-Level
LAnguage
with Ilya Sergey and Amrit Kumar
Student (December 2017)
Xuan Bach Le has defended his thesis!
Poster (APLAS 2017)
Mechanized Verification of Graph-Manipulating
Programs
with Shengyi Wang and Qinxiang Cao
Grant (June 2017)
Verification of a Garbage Collector, Graph-
Manipulating Programs and Cryptocurrency
I am on the program committee for
BTA18!
I am on the program committee for
the BITCOIN
18!
Publication (ICFEM 2017):
A Certified Decision Procedure for Tree Shares
with Xuan Bach Le, Thanh Toan Nguyen, and
Wei Ngan Chin
Keynote (RTST 2017):
Formal Methods in Software Development
Publication (WTSC 2017):
A Concurrent Perspective on Smart Contracts
with Ilya Sergey
Publication (FSTTCS 2016):
Decidability and Complexity of Tree Share Formulas
with Xuan Bach Le and Anthony W. Lin
Publication (APLAS 2016):
Verifying Concurrent Graph Algorithms
with Azalea Raad, Jules Villard, and
Philippa Gardner
Publication (CCS 2016):
Making Smart Contracts Smarter
with Loi Luu, Duc-Hiep Chu, Hrishi Olickel, and
Prateek Saxena
I am on the program committee for
the BITCOIN
16!
Publication (ICFEM 2015)
Specifying Compatible Sharing in Data Structures
with Asankhaya Sharma and Wei-Ngan Chin
Publication (CSF 2015):
On Power Splitting Games in Distributed
Computation: The Case of Bitcoin Pooled Mining
with Loi Luu, Ratul Saha, Inian Parameshwaran,
and Prateek Saxena
Publication (FM 2015):
Certified Reasoning with Infinity
with Asankhaya Sharma, Shengyi Wang,
Andreea Costea, and Wei-Ngan Chin
I am on the program committee for
APLAS 2015!
Publication (ICFEM 2014):
A Resource-Based Logic for Termination and
Non-Termination Proofs
with Ton Chanh Le, Cristian Gherghina, and
Wei-Ngan Chin
Book (Cambridge University Press 2014):
Program Logics for Certified Compilers
(hardcover)
(e-book)
with Andrew W. Appel, Robert Dockins,
Lennart Beringer, Josiah Dodds, Gordon Stewart,
Sandrine Blazy, and Xavier Leroy
I am on the program committee for
CPP 2013!
I am on the program committee for
HOPE 2013!
New paper (June 2013):
Constructing Hereditary Worlds
Within Worlds
with Robert Dockins
Abstract (OBT 2013):
VisualizeSLE: A
Visual Editor for Separation Logic
Entailments (video
demo)
with Soe Lin Myat and Bimlesh Wadhwa
Poster (APLAS 2012):
VisualizeSLE: A
Visual Editor for Separation Logic
Entailments (abstract)
with Soe Lin Myat and Bimlesh Wadhwa
Publication (POPL 2013):
The Ramifications of Sharing
in Data Structures
with Jules Villard
See also this associated technical
report.
Publication (APLAS 2012):
Decision
Procedures over Sophisticated Fractional
Permissions
with Le Xuan Bach, Cristian Gherghina
Publication (MFPS 2012):
Verifying Time Bounds for
General Function Pointers
with Robert Dockins
I am on the program committee for
APLAS 2012!
Publication (LMCS):
Barriers in Concurrent Separation
Logic: Now with
Tool Support!
with Cristian Gherghina
I am the Co-Chair (with
Chin Wei Ngan) for
FTfJP
2012.
Submit a
paper!
Paper (July 2011):
Improving the Compositionality of
Separation
Algebras
Publication (CPP 2011):
Introducing Logic and Formal
Methods with Coq
with Martin Henz
Software release (12/8/2010):
MSL v0.3
with Robert Dockins and Andrew W. Appel
Publication (ESOP 2011):
Barriers in Concurrent Separation
Logic
with Cristian Gherghina
Tutorial presentation (APLAS 2010, 11/28/10):
Developing and
Mechanizing Semantic Models for
Program Logics
with Robert Dockins
(associated with A Logical Mix of Approximation and
Separation)
Publication (Dagstuhl Seminar 10351):
A Theory of Termination via
Indirection
with Robert Dockins
Publication (APLAS 2010, 11/28/10):
A Logical Mix of Approximation and
Separation
with Robert Dockins and Andrew W. Appel
(associated with
Developing and Mechanizing
Semantic Models for
Program Logics)
Publication (POPL 2010, 1/21/10):
A Theory of Indirection via
Approximation
with Robert Dockins and Andrew W. Appel
Publication (APLAS 2009, 12/15/09):
A Fresh Look at Separation Algebras
and Share
Accounting
with Robert Dockins and Andrew W. Appel
|
