国家自然科学基金NSFC-RS（中英）
合作交流项目学术研讨会
国家自然科学基金NSFC-RS（中英）合作交流项目“演化信息物理系统的建模、验证与精化”于2018年10月19日举行2018年度学术研讨会。本次研讨会邀请到了英国约克大学、中科院软件所和国防科技大学等单位的老师做学术报告，详情如下。本次研讨会不收取注册费，食宿自理，欢迎各位同仁参加！
时 间：2018年10月19日8:30-18:00
地 点：西南大学桂园宾馆丹桂楼四楼会议室
联 系 人：赵恒军，18302301799
报 告 一：混成计算的UTP理论
报 告 人：Simon Foster博士, 英国约克大学
摘 要：
本报告将描述混成关系的UTP理论。混成关系是对关系演算的扩展，增加了连续变量和微分方程。混成关系的UTP理论利用Isabelle/UTP提供的机制支持对混成系统的建模和验证。此外，本报告还将介绍我们给出的Modelica语言的指称语义。
报告人简介：
Simon Foster博士是英国约克大学计算机科学系博士后研究员，欧盟Horizon 2020项目INTO-CPS的研究人员。于2005年获得英国谢菲尔德大学计算机科学硕士学位，2009年获得英国谢菲尔德大学计算机科学博士学位。Simon Foster博士的研究兴趣包括定理证明、形式语义、信息物理系统、混成系统、进程代数、指称语义、代数方法、函数式编程。Simon Foster博士是定理证明器Isabelle/HOL的专家，曾将Tony Hoare和何积丰院士的程序统一理论（Unifying Theories of Programming－UTP）实现为Isabelle/UTP。至今已参与多个欧盟研究项目，在知名期刊和会议发表近30篇论文。
报 告 二：概率模型检验
报 告 人：张立军
摘 要：
模型检验是验证系统性质的自动化技术。和测试相比，模型检验能够验证系统没有缺陷，但是存在状态爆炸问题。本报告将介绍概率模型检验的最新进展。
包括基于马尔科夫链的方法、概率时态逻辑和相关的模型检验算法。此外，还将介绍抽象和学习的方法。
报告人简介：
张立军，中科院软件研究所研究员。2000.10至2008.12, 德国萨尔大学本科、研究生、博士。研究领域主要是基于马尔科夫模型及其扩展的概率并发系统的模型检验。作为模型检验的重要扩展，概率模型检验是热门前沿基础研究领域之一。学术成果在著名会议和杂志上发表，例如 CAV、CONCUR、LICS、POPL、ETAPS/TACAS、LMCS、 AAAI、Inf. & Comp.等。
报 告 三：一个混成系统的交互式定理证明器
报 告 人：王淑灵
摘 要：
本报告将会介绍用于验证HCSP混成系统形式化模型的HHL交互式定理证明器。该定理证明器基于Isabelle/HOL实现，以shallow和deep两种方式实现了HHL推理的自动化。我们通过一个月球着陆器安全性验证的实际案例对比了HHL证明器的两种实现方式。
报告人简介：
王淑灵，中科院软件研究所副研究员，主要研究方向为形式化方法、混成系统验证、定理证明等
报 告 四：模态Mu-演算的简单概率扩展
报 告 人：刘万伟
摘 要：
在本报告中，我们提出了模态Mu-演算的一个自然而简洁的扩展。我们研究了扩展的模态Mu-演算和PCTL之间的关系。所提逻辑刻画了一些不能用PCTL表述的有用性质。我们研究了模型检测和可满足性问题，证明模型检测问题是UP和co-UP的，可满足性问题可通过归约到parity博弈问题而得到解决。
报告人简介：
刘万伟，国防科技大学副教授，主要研究方向为形式化方法、概率模型检验等
报 告 五：多项式约束求解问题
报 告 人：代立云
摘 要：
许多程序验证问题可以归结为多项式约束求解问题。在本报告中，我们解释了多项式约束求解的两个思路，一是基于柱形代数分解（CAD），一是基于半定规划（SDP）。同时介绍了我们在多项式约束求解方面的一系列工作。
报告人简介：
代立云，西南大学计算机与信息科学学院讲师，主要研究方向为约束求解、程序分析与验证、软件定义网络。
报 告 六：基于障碍函数生成的混成系统安全验证研究
报 告 人：曾霞
摘 要：
本报告介绍了混成系统验证中障碍函数生成的一种新方法，即Darboux多项式形式的障碍函数。我们给出了计算Darboux形式多项式障碍函数的新方法，
该方法将基于采样的松弛方法和交叉投影方法相结合。实例研究表明所提方法同现有工作相比在障碍函数生成和混成系统验证中的优越性。
报告人简介：
曾霞，西南大学计算机与信息科学学院讲师，主要研究方向为最优化算法、数值计算、混成系统验证。