Back to homeMore on GitHub


Industry โš™

Google @ 2020 summer: Implement hierarchical modelling in an industrial-grade NLP framework and use it for detecting bad mobile apps

AWS @ 2019 summer: Static analyzer for finding interesting dataflows in thousands of services' Java bytecode

Startup @ 2017-2018: Retail trading platform, cryptocurrency transaction processor and UI & devops infrastructure

Research ๐Ÿงช

Checking Android Apps against Behavioral GUI Specification GithubPolicy Dataset

Program AnalysisAndroid ApplicationGUIFormal Verification

Intro: UI Checker is a tool for statically checking whether an Android app violates a formal specification about its look and behaviors, e.g. whether clicking a button of certain style will trigger certain APIs

Contributions: Project lead

Checking Android Apps against Behavioral GUI Specification logo

SeGuard Github

Program AnalysisMachine LearningMalware ClassificationAndroid Application

Intro: SeGuard is a new automated malware detection system for Android applications that combines the advantages of semantic signatures and machine learning.

Contributions: Project lead

SeGuard logo

Iris-C GithubTechnical Report

VerificationC/C++Program LogicConcurrencyCoq

Intro: a library with examples built in Coq, based on Iris framework. This is the artifact of my Bachelor's thesis "An Extensible Verification Framework for Higher-Order Concurrent Imperative Programs".

Iris-C logo

Iris Homepage

VerificationFunctional ProgrammingProgram LogicConcurrencyCoq

Intro: Iris is a Higher-Order Concurrent Separation Logic Framework implemented and verified in the proof assistant Coq.

Contributions: Atomicity related verification, ticket lock etc.

Iris logo


WebProgram AnalysisSpecification

Intro: JavaScript API misuse checking based on the eXtended WebIDL specification, including (highly) experimental integration with TAJS and SAFE analyzers.

Open Source Contributions โค๏ธ

HaLVM Github

Operating SystemsUnikernelFunctional ProgrammingVirtual Machine

Intro: The Haskell Lightweight Virtual Machine (HaLVM): GHC running on Xen. It is one example of <i>Unikernel</i> and is created and maintained by Galois Inc.

Contributions: Porting HaLVM-GHC from v7.8 to v8.0; Integration of the HaLFS file system library

HaLVM logo

Servo Homepage

WebBrowser EngineRust

Intro: Servo is a modern, high-performance browser engine written in Rust language. It is created by Mozilla Research, and being built by a global community, from individual contributors to companies such as Mozilla and Samsung News: Servo code is shipped to millions of users as part of Firefox

Contributions: Implementation of File etc. DOM APIs and resource backends

Servo logo

Hadrian GithubICFP 17' HIWSoH 17'

Build SystemsFunctional ProgrammingCompiler

Intro: Hadrian is a new build system for the Glasgow Haskell Compiler. It is based on Shake and we hope that it will eventually replace the current make-based build system. News: Hadrian is merged into GHC master tree

Contributions: Dynamic linking, installation rules, cross compilation etc.

Hadrian logo

PureScript Homepage

Intro: PureScript is a small strongly typed programming language that compiles to JavaScript. The infrastructure is written in Haskell and it is in many ways like Haskell.

Contributions: PSCi REPL refactoring and libraries patches

Course Projects ๐Ÿซ

BitScope: Scaling Bitcoin Address De-anonymization using Multi-Resolution Clustering Homepage

NLP4SE: Evaluation of Natural Language Processing Techniques for Software Engineering Tasks Report

Finding ๐Ÿฅฃ and ๐Ÿ… in Near-photorealistic Environment using Reinforcement Learning Poster

Solver-aided Language SMT2 Benchmark Github

More on GitHub

Updated in: Sep 2021

Back to home