日期

时间

报告人

报告题目

主持人

13日

8:00-8:50

注册

8:50-9:00

开幕式 领导致辞

Session 1: 模型检验 （1） 报告厅

陈意云

9:00-9:40

王捍贫

1. 模型检查理论与实践的差距
   

9:40-10:10

张立军

1. Probabilistic Model Checking -- How to Avoid Direct Product Construction?

10:10-10:40

孔维强

1. Facilitating Multicore Bounded Model Checking with Stateless Explicit-State Exploration
   

10:40-11:00

陈 哲

1. Model Checking Aircraft Controller Software
   

11:00-11:20

茶歇

Session 2: 程序分析与测试 报告厅

陈仪香

11:20-11:50

杨 珉

1. AppIntent: Analyzing Sensitive DataTransmission in Android for Privacy Leakage Detection

11:50-12:20

刘 攀

1. RFSM：A Test Modeling Tool Prototype for Regular Expressions

12:20-12:40

孙家泽

1. 基于群体智能的软件测试用例优化研究

12:40-13:40

工作午餐 奥运餐厅一层

Session 3: 程序建模与分析 报告厅

张立军

13:40-14:10

张文辉

1. Bounded Semantics and Bounded Correctness Checking

14:10-14:40

陈立前

1. CAI：一个面向嵌入式C程序的数值性质分析工具

14:40-15:10

孙 猛

1. A Hybrid Model of Connectors in Cyber-Physical Systems

15:10-15:30

茶歇

Session 4: 程序验证 报告厅

朱惠彪

15:30-16:00

陈一峯

1. 几个应用领域的潜在问题

16:00-16:30

陈振邦

1. Symbolic Execution of MPI Program

16:30-17:10

董云卫

1. 模型驱动的IMA嵌入式系统设计与验证方法

17:10-18:10

讨论会(报告厅)：软件分析和验证研究当前和未来的焦点

18:30-20:30

晚餐 (校内天天餐厅)

日期

时间

报告人

报告题目

主持人

14日

Session 5: 可信计算与度量 报告厅

张文辉

8:30-9:10

陈仪香

1. 软件可信度量与评估

9:10-9:40

熊英飞

1. 内存泄露的自动修复

9:40-10:10

赵世忠

1. 算术表达式的误差可控计算及其软件Isreal的一些进展

10:10-10:30

茶歇

Session 6: 程序分析与验证 报告厅

熊英飞

10:30-11:10

赵建华

1. Scope Logic进展：数据流分析、最弱前置条件计算的集成

11:10-11:40

蒲戈光

1. 基于时序公式收敛展开的运行时验证框架

11:40-12:10

徐立华

1. ProMiner:基于系统属性的双向一致性检验框架

12:10-13:10

工作午餐 奥运餐厅一层

Session 7: 程序开发与精化 报告厅

贾春福

13:10-13:40

王海峰

1. 轨道交通列控系统安全关键软件的开发实践

13:40-14:10

付 明

1. Refinement-Based Verification Framework for Lock-Based Software Transactional Memory

14:10-14:40

李 钦

1. A Refinement Framework for Autonomous Agents

14:40-15:10

茶歇

Session 8: 程序分析 报告厅

赵建军

15:10-15:40

林子熠

1. Java Concurrent Bug Benchmark

15:40-16:10

开金宇

1. 基于定量概率模型检验的Web服务系统主动式自适应调整

16:10-16:40

程 啸

1. Towards Synchronizing Programs via Bidirectional Transformation

16:40-17:00

刘海洋

1. 面向对象程序的所有权分析

Session 9: 程序验证 会议室

赵建华

15:10-15:40

时清凯

1. VerifyingSynchronization for Atomicity Violation Fixing: Tech. & Tools

15:40-16:10

张 扬

1. Program Logic for Local Reasoning in TSO

16:10-16:40

方徽星

1. Formal verification and simulation for platform screen doors and collision avoidance in subway control systems

16:40-17:00

张 可

1. OO程序验证系统的Coq实现

17:00-18:00

讨论会(报告厅)：软件分析和验证研究当前和未来的焦点

18:30-20:30

晚餐 (校内天天餐厅)

日期

时间

报告人

报告题目

主持人

15日

Session 10: 程序分析技术应用 报告厅

裘宗燕

8:30-9:00

刘建宾

1. 基于程序蓝图的软件可视自动化逆向工程技术

9:00-9:30

朱雪阳

1. 同步数据流图的优化与调度研究

9:30-10:00

杨红丽

1. WSN数据收集协议建模、分析与测试

10:00-10:30

Deepak Kapur

1. When is a formula invariant?

Session 11:程序设计与分析 会议室

贺 飞

8:30-9:00

陈明帅

1. Shift between Formal and Informal Design of Embedded Systems

9:00-9:30

祖 佺

1. Bounded model-checking of discrete duration calculus

9:30-10:00

王伟峰

1. 时间自动机迹抽象求精（Trace Abstraction Refinement for Timed Automata）

10:30-10:50

茶歇

Session 12: 模型检验（2）报告厅

缪淮扣

10:50-11:20

贺 飞

1. Leveraging Weighted Automata in Compositional Reasoning about Concurrent Probabilistic Systems

11:20-11:50

李国强

1. Time-Sensitive Pushdown Systems

11:50-12:20

宋 富

1. Model-checking for Android Malware Detection

12:20-12:50

张智慧

1. 安全关键软件在核电中的开发与应用

Session 13:程序分析与验证 会议室

焦 莉

10:50-11:20

吴添勇

1. Relda2：一个轻量级的Android程序资源泄露检查工具

11:20-11:50

李 新

1. pIML - An Interrupt Program Modelling Language for Real-Time and Embedded Systems

11:50-12:20

胡婷婷

1. OO程序的代数规范与验证

12:50-13:00

会议总结 张健

13:00-14:00

工作午餐 奥运餐厅一层