Skip to content
View Hughshine's full-sized avatar
💠
💠
101 followers · 223 following

Achievements

Achievement: StarstruckAchievement: Pull Sharkx2Achievement: Arctic Code Vault Contributor

Achievements

Achievement: StarstruckAchievement: Pull Sharkx2Achievement: Arctic Code Vault Contributor

Block or report Hughshine

Block user

Prevent this user from interacting with your repositories and sending you notifications. Learn more about blocking users.

You must be logged in to block users.

Please don't include any personal information such as legal names or email addresses. Maximum 100 characters, markdown supported. This note will be visible to only you.
Report abuse

Contact GitHub support about this user’s behavior. Learn more about reporting abuse.

Report abuse
Hughshine/README.md

Hi there 👋 Blessing on your day.

I'm Xuyang Li, currently a 1st year PhD student working on formal methods at Elmore Family School of Electrical and Computer Engineering , Purdue. Feel free to chat with me at li5274 at purdue dot edu!

I research on formal methods and software engineering techiques.

For former projects, I worked on verified compilation (see CompCert) and polyhedral compilation (see Pluto). I also know something about relaxed concurrency (see compiler verification on Promising Semantics). I mechanize proofs with Coq proof assistant.

If you're interested, just drop by my homepage!

2024.9.15

Pinned Loading

  1. verif-scop/PolCert verif-scop/PolCert Public

    A verified polyhedral scheduling validator in Coq.

    Coq 19 1

  2. promising-comp promising-comp Public

    Mirror for compcert implementation in promising semantics

    Coq

  3. bondhugula/pluto bondhugula/pluto Public

    Pluto: An automatic polyhedral parallelizer and locality optimizer

    C 278 65

  4. AbsInt/CompCert AbsInt/CompCert Public

    The CompCert formally-verified C compiler

    Coq 1.9k 230