软件安全实验室
研究领域：
- 指针程序逻辑和推理工具
- 出具证明的编译器
- 软件事务内存的语义模型和程序推理工具
- 领域专用语言和逻辑
- 操作系统内核验证
实验室以往研究内容
- 代数规范
- constructional proof of software and chemical reaction-based computation model
- Gamma 语义和其它并发语言
- properties of non-terminated rewriting system and its category theoretical semantics
- 类型化低级语言的设计与实现
- vectorial FORTRAN 77 编译器与 concurrent C编译器
- 从C到Java语言翻译的编译器（由perl编写）
指导老师：
- 陈意云
- 张昱