Hoblovski

CS PhD (struggling) at Tsinghua. Interested in compilers & FP stuff & OS kernels. Currently doing static analysis work i.e. automated bug detection.

Tsinghua Univ.Beijing

Pinned Repositories

algorithms-park
My implementation of various algorithms.
Language:C++1 2 00
course-notes
Personal course notes (in Chinese) for THU CST.
Language:TeX13 3 00
decaf-backend
NEO backend for Decaf. (WIP) SSA IR; DAG covering for InstrSel; better RegAlloc.
Language:Scala20
dt-comp
Prototype auto test-case generation for Minidecaf. (Not for general C. Use CSmith for that.)
Language:Python1 1 00
MiniML
Self-made functional compiler for fun. Uses SECD as intermediate language.
Language:Python4 2 00
miniml-rs
MiniML reimplemented in Rust. Self-made functional compiler for fun.
Language:Rust0 1 00
OS2018spring-projects-g02
清华大学操作系统大作业: 针对一个极简 ISA 实现 cpu 和编译器, 并且适配一个极简 kernel
Language:C++8 3 02
screenshot-pin
Select a region on the screen and pin it on top of all other windows. For windows.
Language:C++20
stupid-see
A Rust symbolic execution engine. Mainly targeted at the verification course in THU.
Language:Rust2 2 00
xv6-public
xv6 OS + various experiments
Language:C10

Hoblovski's Repositories

Hoblovski/MiniML
Self-made functional compiler for fun. Uses SECD as intermediate language.
Language:Python4 2 00
Hoblovski/decaf-backend
NEO backend for Decaf. (WIP) SSA IR; DAG covering for InstrSel; better RegAlloc.
Language:Scala20
Hoblovski/dt-comp
Prototype auto test-case generation for Minidecaf. (Not for general C. Use CSmith for that.)
Language:Python1 1 00
Hoblovski/perwindow-search.vim
Allows different vim windows to have their own search patterns.
Language:Vim Script1 1 0
Hoblovski/rs-raft-interactive
Interactive TLA+ style reasoning of Raft in Rust
Language:Rust1 1 0
Hoblovski/miniml-rs
MiniML reimplemented in Rust. Self-made functional compiler for fun.
Language:Rust0 1 00
Hoblovski/arceos
An experimental modular OS written in Rust.
Language:Rust0 0
Hoblovski/brython
Brython (Browser Python) is an implementation of Python 3 running in the browser
Language:Python1 0
Hoblovski/checkers_sosp23
The source code of static checkers for refcounting bugs.
Language:Python0 0
Hoblovski/cmdgrp
Easily create command groups like `apt` or `git`
Language:Python1 0
Hoblovski/compilerverif
(partial) proofs for https://xavierleroy.org/courses/EUTypes-2019/
Language:Coq2 0
Hoblovski/dcore
Mini-microkernel in rust
Language:Rust1 0
Hoblovski/ExImp
Various PLV experiments
Language:Coq1 0
Hoblovski/IncorLogic
Formalization of O'Hearn's Incorrectness Logic in Coq.
Language:HTML
Hoblovski/kern-stack-stat
Language:Assembly
Hoblovski/mdverif_testcases
MiniDecaf 验证大作业的测例
Language:C2 0
Hoblovski/minidecaf-web
Language:JavaScript
Hoblovski/mircallgraph
Language:Rust1 0
Hoblovski/multiboot-example-os
Example OS code for multiboot, built and run.
Language:C
Hoblovski/nom
Rust parser combinator framework
Language:Rust1 0
Hoblovski/pysh
Painfree shell programming in Python
Language:Python1 0
Hoblovski/rc-files
Migrated from bitbucket
Language:Vim Script2 0
Hoblovski/rCore-Tutorial-v3
Let's write an OS which can run on RISC-V in Rust from scratch!
Language:Rust0 0
Hoblovski/RSECD-interp
Interactive interpreter, for the recursive SECD machine.
Language:Python2 0
Hoblovski/rt64
Real time OS on x64
Language:C2 0
Hoblovski/rustc-dev-guide
A guide to how rustc works and how to contribute to it.
Language:HTML0 0
Hoblovski/sf
Language:HTML0 0
Hoblovski/stupid-decaf
A stupid implementation of minidecaf (in fact smolsee)
Language:Python2 0
Hoblovski/xv6-riscv
Xv6 for RISC-V
Language:C1 0
Hoblovski/xx6
RISC-V OS inspired by (frankly largely reusing code from) xv6, with a lot of hacks (XXX)
Language:C2 0