Jinpeng Wang

Jinpeng Wang

王锦朋

he/his

Young, simple, and naive

Sitemap

A list of all the posts and pages found on the site. For you robots out there, there is an XML version available for digesting as well.

Pages

Posts

Jane Street 挂经

less than 1 minute read

Published:

记录 Jane Street 技术面试、onsite 面试题与未获录用的经历。

如何投稿一篇论文

less than 1 minute read

Published:

记录首次投稿论文前后的科研经历、幻灭与反思。

JVM exception handlers

less than 1 minute read

Published:

分析 JVM 异常处理器顺序及 Java 静态分析中的方法内异常传播。

我是如何成为TA的

less than 1 minute read

Published:

记录第一次担任助教的经历、工作、同事及对本科教育的思考。

DOM

less than 1 minute read

Published:

本文尚未展开 DOM 内容。

Futamura Projections

less than 1 minute read

Published:

介绍 Futamura 投影，以及特殊化器、编译器和元编译器的关系。

DB04 Storage

less than 1 minute read

Published:

介绍数据库的文件、页、块、元组存储及有序数据组织。

DB03 SQL

1 minute read

Published:

介绍 SQL 查询、视图、事务、约束及编程语言与数据库交互。

浅谈Verilog中的X

1 minute read

Published:

讨论 Verilog 中 X 的仿真、综合、验证语义及其精度问题。

DB02 Relational

1 minute read

Published:

介绍关系模型、主键与外键，以及基本关系代数操作。

DB01 Intro

less than 1 minute read

Published:

介绍数据库、数据模型、DBMS 分层及存储、查询和事务管理。

SA04 Abstract interpretation

less than 1 minute read

Published:

介绍 Galois connection、soundness 与抽象解释的最优性。

Tour de SAT

1 minute read

Published:

介绍 SAT、CNF、Resolution、DPLL 及 SAT 求解器搜索策略。

SA03 narrowing & widening

less than 1 minute read

Published:

介绍 Widening 加速格上分析，以及 Narrowing 提升分析精度。

Cpp Lambda Quirks

1 minute read

Published:

通过实例解释 C++ Lambda 捕获、静态变量与可变闭包的行为。

SA02 lattice

3 minute read

Published:

介绍格、偏序、单调函数与不动点在静态分析中的作用。

SA01 Type

1 minute read

Published:

介绍类型作为静态分析、递归类型和约束求解类型检查。

大三下荒唐实录

less than 1 minute read

Published:

记录大三下的课程、科研、生活及保研经历。

LLHD 踩坑记

less than 1 minute read

Published:

记录 Moore/LLHD 工具链构建中的 Rust、依赖与头文件问题。

Compiler04 语法制导翻译

less than 1 minute read

Published:

介绍语法制导定义、继承属性、综合属性与语义动作。

Network06 Wireless

less than 1 minute read

Published:

介绍无线局域网、隐藏终端、CDMA、802.11、CSMA/CA 与 RTS/CTS。

Network05 Link

2 minute read

Published:

介绍链路层、校验码、共享介质协议、ARP、交换机与 VLAN。

Automata07 TS

1 minute read

Published:

介绍 Transition System、等价关系、积系统及 LTL 时序逻辑。

cmm Compiler Design

3 minute read

Published:

记录 Cmm 编译器的解析、AST、类型检查、数据流分析与优化设计。

CMU-DB Lab

less than 1 minute read

Published:

记录 CMU 数据库 Lab0 Trie 的实现经验与 C++ 指针用法。

Network04 Network

1 minute read

Published:

介绍网络层、SDN、路由器、IP 编址、NAT 与路由算法。

大三上昏睡日志

less than 1 minute read

Published:

记录大三上学期的校园生活、课程体验、工程尝试与日常感想。

Automata06 Complexity

1 minute read

Published:

介绍可判定性、递归语言、P/NP/PSPACE/EXP 及复杂度规约。

Automata05 TM

1 minute read

Published:

介绍图灵机、递归可枚举语言、机器变体与语言闭包性质。

Automata04 PDA

1 minute read

Published:

介绍下推自动机、接受方式、确定性及其与 CFG 的等价性。

Automata03 CFL

1 minute read

Published:

介绍上下文无关文法、推导、二义性及 Chomsky 范式。

Automata02 RE

1 minute read

Published:

介绍正则表达式、正则语言的性质及与有限自动机的等价性。

Concurrency04 Promising

less than 1 minute read

Published:

介绍 Promising Semantics 通过 promises 约束内存行为并避免 OOTA。

Linguistics02 Phonetics

less than 1 minute read

Published:

介绍 IPA、辅音和元音，以及发声部位和发声方式。

Linguistics01 Intro

less than 1 minute read

Published:

介绍语言学的研究对象及语音、音系、形态、句法等分支。

Network03 Transport

less than 1 minute read

Published:

介绍 UDP、TCP、Socket、可靠传输及 ARQ 协议的基本机制。

Automata01 FSM

1 minute read

Published:

介绍 DFA、NFA、ε-NFA 的定义、等价性与 DFA 最小化。

Concurrency03 Axiomatic

less than 1 minute read

Published:

本文尚未展开公理化并发语义内容。

Concurrency02 Operational

less than 1 minute read

Published:

用操作语义描述并发系统中的 CPU、内存及 CAS、FAA 等操作。

Concurrency01 HMM

less than 1 minute read

Published:

介绍弱内存模型、happens-before 关系与 Out-of-Thin-Air 行为。

Network02 Application

2 minute read

Published:

介绍网络应用、Socket、HTTP、DNS、P2P 与 CDN 等应用层主题。

Memory Models

1 minute read

Published:

介绍顺序一致性、TSO 及写缓冲导致的内存可见性问题。

TAOMP02 Mutex

2 minute read

Published:

形式化讨论互斥锁、活性、公平性以及 Peterson、Filter 和 Bakery 算法。

TAOMP01 Intro

less than 1 minute read

Published:

介绍多处理器并发、共享状态、互斥性、活性与 Amdahl 定律。

TAPL09 Recursive Types

1 minute read

Published:

介绍递归类型、等递归与同构递归，以及归纳和余归纳不动点。

TAPL08 Subtyping

1 minute read

Published:

介绍子类型关系、函数变型、引用类型及 coercion semantics。

TAPL07 Exceptions

less than 1 minute read

Published:

介绍异常传播、捕获、携带信息及异常处理的类型规则。

TAPL06 References

less than 1 minute read

Published:

介绍可变引用、副作用、别名、存储位置及引用类型检查。

Network01 Intro

less than 1 minute read

Published:

从分层、交换与接入方式介绍计算机网络和互联网基础。

TAPL05 Extensions

1 minute read

Published:

介绍为简单类型 Lambda 演算添加 Unit、Record、Variant、Exception 等语言构造。

TAPL04 Typed Lambda

1 minute read

Published:

介绍简单类型 Lambda 演算及类型唯一性、Progress 和 Preservation 定理。

操作系统05 调度

less than 1 minute read

Published:

介绍单核与多核任务调度策略、评价指标及公平性问题。

Haskell Parser Combinator

4 minute read

Published:

用 Haskell 实现 Parser Combinator，介绍 Functor、Monad 与解析组合子。

TAPL03 Untyped Lambda

2 minute read

Published:

介绍无类型 Lambda 演算、规约策略、代数数据类型与 De Bruijn 表示。

TAPL02 Basics

less than 1 minute read

Published:

介绍 TAPL 中的数学记号、语法、操作语义及基本语言性质。

TAPL01 Intro

less than 1 minute read

Published:

介绍类型系统、静态检查、语言安全与类型推导的基本概念。

操作系统04 进程与线程

less than 1 minute read

Published:

介绍进程、线程、用户态线程、内核线程与纤程的概念。

Algebra03 同态与同构

1 minute read

Published:

介绍群同态、核、同构、第一同构定理与对应定理。

Algebra01 群的定义

3 minute read

Published:

从代数系统出发介绍半群、幺半群、群及其等价定义。

操作系统03 内存管理

less than 1 minute read

Published:

介绍虚拟内存、换页、Buddy System、freelist 与 SLAB 分配。

操作系统02 并发

1 minute read

Published:

介绍并发 bug、互斥锁、条件变量、信号量及 RCU 等同步机制。

操作系统01 导引

less than 1 minute read

Published:

从程序、抽象、资源管理与系统调用角度介绍操作系统。

ANTLR4 笔记

less than 1 minute read

Published:

记录 ANTLR4 中 Lexer、Parser、Visitor 与语法规则设计的实用技巧。

操作系统 Lab3 uproc

less than 1 minute read

Published:

记录用户进程实验中的地址空间、fork、进程管理与内核栈问题。

大二下摸鱼记录

less than 1 minute read

Published:

记录大二下的校园生活、课程体验及对多门课程的评价。

计算方法07 电阻网络

1 minute read

Published:

用拉普拉斯矩阵分析电阻网络、电势分布、等效电阻与能量。

计算方法06 FFT

less than 1 minute read

Published:

据助教说不考这么麻烦的计算，我就摸了

博弈论02 零和游戏

less than 1 minute read

Published:

介绍零和博弈的 min-max 定理、混合策略均衡与线性规划求解。

操作系统 Lab2 kmt

less than 1 minute read

Published:

记录多核任务、信号量与上下文切换实现中的栈竞争和调试问题。

操作系统 Lab1 pmm

less than 1 minute read

Published:

记录多核物理内存分配器的设计、链表与线段树实现及调试经历。

博弈论01 策略游戏

1 minute read

Published:

介绍纯策略与混合策略博弈、纳什均衡及其求解方法。

计算方法01 函数求根

less than 1 minute read

Published:

严格写就太累了，这个就当是随手的笔记得了。大概看看原理，不求甚解。

数理逻辑03 一阶逻辑

1 minute read

Published:

从命题逻辑扩展到一阶逻辑，介绍项、公式、量词、解释与赋值。

数理逻辑02 推演系统

9 minute read

Published:

介绍 Gentzen 与 Hilbert 推演系统，以及正确性、完备性和一致性。

数理逻辑01 命题逻辑

4 minute read

Published:

介绍命题逻辑的语法、语义、可满足性及 Semantic Tableaux 判定方法。

大二上躺平经验

less than 1 minute read

Published:

记录大二上课程体验、密码学与系统实验，以及留校生活。

PA4 附加关卡

less than 1 minute read

Published:

记录 PA4 中虚拟内存、进程、中断与加载器 bug 的实现思考。

密码学07 OWF&HC

less than 1 minute read

Published:

介绍单向函数、硬核谓词及其构造伪随机生成器的关系。

密码学06 HASH

less than 1 minute read

Published:

介绍密码学哈希的抗碰撞性质、Merkle-Damgård 构造及 MAC 应用。

密码学05 MAC

less than 1 minute read

Published:

介绍消息认证码、不可伪造性定义及定长和任意长 MAC 构造。

PA3 附加关卡

less than 1 minute read

Published:

记录 PA3 中栈、异常、ELF 加载、文件系统与库函数实现中的问题。

PA2 附加关卡

less than 1 minute read

Published:

记录 PA2 中声卡、调试追踪、差分测试与 NEMU 实现经验。

PA1 附加关卡

1 minute read

Published:

记录 PA1 中表达式求值、断点和程序测试等基础实验思考。

形式语义05 Semantics

less than 1 minute read

Published:

介绍操作语义及大小步、小步语义，用规则描述程序执行。

密码学04 PRG&PRF

1 minute read

Published:

介绍伪随机生成器和伪随机函数，以及它们在多次加密中的应用。

形式语义04 Types

1 minute read

Published:

介绍类型系统、类型安全及 STLC 的 Progress 与 Preservation 定理。

密码学03 Computational

1 minute read

Published:

介绍计算安全、可忽略函数、PPT 对手与私钥加密安全游戏。

形式语义03 Lambda

3 minute read

Published:

系统介绍 Lambda 演算的替换、规约、合流性与递归编码。

密码学02 Perfect

1 minute read

Published:

介绍完美保密、一次一密及其概率定义、证明与局限。

形式语义02 Math

1 minute read

Published:

用集合、函数与积和类型的形式化定义说明程序状态和类型构造。

形式语义01 Intro

less than 1 minute read

Published:

介绍形式语义课程动机、程序性质证明及 Coq 形式化验证。

密码学01 Intro

1 minute read

Published:

介绍密码学的安全目标、攻击模型、经典密码与可证明安全。

Compiler03 语法分析

4 minute read

Published:

介绍上下文无关文法、语法树、LL/LR 分析与错误恢复。

Compiler02 词法分析

1 minute read

Published:

介绍词法分析、正则表达式、DFA/NFA 及词法分析器构造。

软件分析08 Datalog

1 minute read

Published:

Datalog = Data + Logic，是声明式编程语言(Declarative Programming Language) Prolog的一个子集

软件分析07 Security

less than 1 minute read

Published:

本文尚未展开软件分析安全性内容。

软件分析06 CSA

less than 1 minute read

Published:

CSA=Context Sensitive Analysis 上下文敏感分析

软件分析05 PA

less than 1 minute read

Published:

本文尚未展开软件分析 PA 内容。

软件分析04 CGC

less than 1 minute read

Published:

CGC=Call Graph Construction

大一下存活纪实

less than 1 minute read

Published:

记录大一下的校园生活、课程体验与学习摸鱼经验。

集训补题合集

less than 1 minute read

Published:

汇总多场训练赛题解，涉及树上 DP、卷积、图论与数论。

软件分析03 DFA

less than 1 minute read

Published:

这里的DFA可不是有限状态自动机哦

软件分析02 IR

less than 1 minute read

Published:

本文尚未展开软件分析 IR 内容。

软件分析01 Intro

1 minute read

Published:

决定要好好开干了，于是有了这个系列的笔记

图论03 染色

4 minute read

Published:

讨论点染色、边染色、色多项式、Brooks 定理与平面图染色。

图论01 基本概念&定义

1 minute read

Published:

介绍图的基本类型、邻接、同构、子图、度数和距离等概念。

ICPC 2021 银川划水记

less than 1 minute read

Published:

记录银川 ICPC 线下赛的旅途、比赛过程与赛后感想。

图论02 匹配

less than 1 minute read

Published:

本文尚未展开图论匹配内容。

CSAPP实验06 : shlab

less than 1 minute read

Published:

本文尚未展开 shlab 实验内容。

大一上存活经验

less than 1 minute read

Published:

记录大一上校园生活、课程体验与期末复习经验。

CSAPP实验04: archlab

less than 1 minute read

Published:

本文尚未展开 archlab 实验内容。

CSAPP实验01 : datalab

8 minute read

Published:

记录 CSAPP Data Lab 中整数与浮点位级运算题的解法。

信息与计算科学导论03

less than 1 minute read

Published:

介绍集合势、康托定理、不可数性与 Cantor-Bernstein 定理。

信息与计算科学导论02

less than 1 minute read

Published:

讲解递归方程的特征方程、生成函数、算子与主定理。

信息与计算科学导论01

less than 1 minute read

Published:

介绍集合论基础、关系、传递闭包、等价类与函数。

Compiler01 Introduction

1 minute read

Published:

介绍编译器流程、前后端结构及词法分析到代码生成的主要阶段。

有关集合大小的比较

1 minute read

Published:

用双射证明无限集合等势，讨论实数、平面与幂集的大小。

Hello World!

less than 1 minute read

Published:

记录进入大学后的新博客，以及通过写作记录成长的愿望。

portfolio

publications

The Essence of Verilog: A Tractable and Tested Operational Semantics for Verilog

Published in OOPSLA, 2023

This paper is about the formal operational semantics of Verilog.

Recommended citation: Qinlin Chen, Nairen Zhang, Jinpeng Wang, Tian Tan, Chang Xu, Xiaoxing Ma, and Yue Li. (2023). The Essence of Verilog: A Tractable and Tested Operational Semantics for Verilog. Proceedings of the ACM on Programming Languages, 7(OOPSLA2), 234-263. https://doi.org/10.1145/3622805
Download Paper | Download Bibtex

Heap Abstraction via Early-Confluent Object Merging for Pointer Analysis

Published in OOPSLA, 2026

This paper is about efficient heap abstraction for pointer analysis.

Recommended citation: Jinpeng Wang, Yufei Liang, Zhongsheng Zhan, Tian Tan, and Yue Li. (2026). Heap Abstraction via Early-Confluent Object Merging for Pointer Analysis. Proceedings of the ACM on Programming Languages, 10(OOPSLA2). To appear.

talks

Verilator: The Fast Free Hardware Simulator

Published:

This is a course presentation talk about a widely-used tool, Verilator, which is a fast free hardware simulator that serves as the foundation of hardware design and verification.

teaching