【暑期班预告】SSFM 2018欢迎你！
2018/8/16 17:15:38 中国科学院软件研究所
SSFM 2018
形式化方式暑期班(SSFM 2018)将于2018年8月24日至9月1日在中国科学院软件研究所举办。 SSFM 2018是 CONFESTA 2018大会的一部分，由中国科学院软件研究所、北京大学和中国科学院大学联合举办。
CONFESTA 2018是并发理论和形式化验证领域的联合大会，由中科院软件所计算机科学国家重点实验室承办。大会包括4个国际会议、4个研讨会、2个讲习班和1个暑期班，将汇聚全球顶尖计算机及软件领域专家，深入交流并发理论与形式化验证领域的最新研究成果。
暑期班主席
詹乃军研究员, 中国科学院软件研究所
张立军研究员, 中国科学院软件研究所
组织主席
孙猛教授, 北京大学
薛白副研究员, 中国科学院软件研究所
课程安排
简历：Joost-Pieter Katoen是德国亚琛工业大学的杰出教授，并在荷兰恩斯赫德的屯特大学担任兼职教授。 他是欧洲科学院院士，并获得丹麦奥尔堡大学的荣誉博士学位。 他是牛津大学、奥地利科学技术研究所和悉尼麦考瑞大学的访问教授。他的研究兴趣包括形式方法，模型检测，并发理论和概率计算。 2018年，他获得了ERC高级研究基金。 他与人合著了170多篇会议论文，70篇期刊论文和“模型检测原理”一书。 Katoen教授是ETAPS指导委员会主席，CONCUR，QEST和FORMATS会议指导委员会成员。
摘要：概率程序结合了概率论、统计学和从建模的角度来说最重要的编程语言。它们允许以相当简洁的方式对更大一类的模型进行建模。现代概率程序语言的全部潜力来自于根据观察 到的数据自动推断模型中未观察到的变量的过程。正如一些研究人员所说：“概率程序的目标是使程序员能够接触概率建模和机器学习。”
概率程序引导自主机器人是安全机制的核心，其中包含随机算法，并用人工智能推断关于大量不确定数据的统计结论。
在本系列讲座中，我将介绍概率程序的主要概念，并讨论如何使用经典的程序验证来解决Dijkstra问题，例如：这些程序是否计算出人们期望他们做的事情？他们终止了吗？有什么概率？他们消耗了多少资源？贝叶斯网络的应用将显示如何通过使用程序验证以完全自动化的方式获得有关分析此类网络的深入信息。
ETAPS和TACAS指导委员会的成员
课程题目:并发程序
简历：Holger Hermanns教授是德国萨尔布吕肯萨尔大学的教授，担任可靠系统和软件实验室主任。此前，他曾在德国埃尔兰根-纽伦堡大学、荷兰特屯特大学和法国格勒诺布尔罗纳-阿尔卑斯地区的法国国家信息与自动化研究所担任过职务，并曾担任萨尔大学数学与计算机科学学院院长。他的研究兴趣包括并发系统的建模和验证，资源感知嵌入式系统，组合性性能和可靠性评估，以及它们在能源信息学中的应用。 Holger Hermanns撰写或合著了200多篇同行评审的科学论文。他曾担任CAV，CONCUR，TACAS和QEST等主要国际会议的计划委员会主席，并在十几个国际会议和研讨会上发表了主题演讲。他是ETAPS和TACAS指导委员会的成员。他是“Friends of Dagstuhl e.V.”协会的主席，以及 “ETAPS e.V.” 协会的副主席。 曾获荷兰“Vernieuwingsimpuls”和德国“Preis des Fakult?tentages Informatik”奖。他是ERC高级研究基金受资助人，也是 AE(欧洲科学院)的当选成员，并持有其他几项国家和欧洲研究资助。
摘要：现在几乎所有计算机、笔记本电脑和智能手机都可以找到同时执行并发任务的多核、显卡和其他并行架构。 编写这样的系统以使它们有效地工作是一个真正的挑战。 如果一个人相信硬件制造商的预测，这将很快成为普通软件工程师的日常任务。
不幸的是，编程这样的并发系统非常困难并且容易出错。 这具有理论和实践上的原因。 本讲座的目的是让学生熟悉并发编程的理论和实践。毫无疑问这是一项艰巨的任务。
这是Hermanns教授首次在德国以外的地方展示他的曾获奖的并发编程系列课程。
简历：王柏尧，台湾中央研究院资讯科学研究所研究员。 于2008年至2012年担任中央研究院副研究员，2009年至2011年担任INRIA特邀教授，2009年至2010年任清华大学副教授，2009年至2012年任台湾大学副教授，2003年至2008年担任中央研究院助理研究员，2004年至2009年任台湾大学助理教授。他的研究兴趣是逻辑及其在计算机科学中的应用。他主要在形式验证方向开展研究工作。过去他一直致力于组合推理，程序验证，基于学习的验证技术。 最近，他的研究兴趣在验证安全库(如OpenSSL和boringSSL)加密原语的汇编实现。 他还在中央研究院开展跨学科隐私研究项目。
摘要：密码程序广泛用于计算机系统。 从在线银行到身份证，敏感信息被来自计算机密码学的各种密码系统加密。 密码程序是当今世界中最关键的软件之一。 在本讲座中，我将鼓励在实践密码学中验证汇编实现的加密程序的研究。 我们将看到现有验证技术的局限性。 最后，我将介绍我们的混合技术CryptoLine，用于汇编加密程序的功能验证。 我们将看到如何应用CryptoLine来验证OpenSSL中的汇编程序。
简历：Martin Fr?nzle教授在德国奥尔登堡大学计算机科学系教授，主要从事离散连续混成系统的研究。他的研究兴趣包括对嵌入式和信息物理融合系统中交互、实时和混成行为的建模、验证和合成。他曾研究高层建模和规范语言的语义，以及决策问题及其在验证和合成实时离散连续混成系统(包括受随机干扰影响)中的应用。通过将有界模型检查扩展到非常富有表达力的时序逻辑、分支时间抽象以及通过开发可满足性模理论技术来解决算术约束并将它们处理为不同验证和合成领域的规范公式结构，复杂度边界被这样的自动验证和合成过程突然打破。此外，用于算术约束求解的可满足性模理论技术已经扩展到涉及超越函数和常微分方程的算术约束这样不可判定论域以及促进概率混成系统的全符号分析的随机变量。另一个主要研究领域涉及系统正确性的鲁棒概念，即具有正确性证书的结构，该正确性证书在诸如制造公差或不完整信息之类的普遍存在的干扰下仍然有效。关于这些主题的基础研究主要在大型合作研究项目中进行，如跨区域协作研究中心SFB-TR 14 AVACS(复杂系统的自动验证和分析)或最近研究培训组DFG GRK 1765 SCARE(不利条件下的系统正确性)。
摘要：四分之一世纪以来，混成自动机和与其密切相关的模型已经成为捕获和形式化分析信息物理融合系统(CPS)中离散和连续组件联合作用的主力。尽管在连续和离散状态空间可扩展性方面不断取得进展，但基础计算模型越来越多地显示出其局限性。虽然混成自动机对概率或随机的扩展是可用的，并且能够看到第一个实验工具支持，但仍有其他限制到目前为止还没有真正解决。特别重要的是反馈回路的延迟、与网络化CPS或CPS系统相关的问题以及所有当前混成自动机变体和几乎所有工程控制系统中发现的计量概念之间的基本差距，即不确定状态下的状态估计。
在本讲座中，我们将解释基于算术约束求解的各种风格(确定性，非确定性，概率性，随机性)和相关自动验证方法的混成自动机模型。然后我们将介绍涉及延迟反馈的信息物理融合系统模型以及通过优化状态估计(即过滤)来抵消测量误差的信息物理融合系统模型。我们将证明即使是最先进的传统混成自动机模型也无法充分编码CPS这些无所不在的特征的影响，并将建议相应的模型，从而也介绍相应自动验证程序。
简历：Stefan Mitsch教授是卡内基梅隆大学计算机科学系逻辑系统实验室的系统科学家。 他于2012年获得Johannes Kepler大学计算机科学博士学位，并获得了Promio Sub Auspiciis Praesidentis Rei Publicae和ERC Marie Curie研究奖学金。 他的研究专注于是信息物理融合系统的建模、形式验证和经过验证的运行时安全方法。 他对应用软件工程方法来支持系统设计和验证特别感兴趣。
摘要：信息物理融合(CPS)如今已普遍融入我们的生活中，并且越来越紧密地发挥作用，并对人类产生直接影响。 例如，汽车中的驾驶员辅助系统负责基于距离传感器控制加速和制动。 在生命受到威胁的许多安全攸关领域，例如工厂自动化，医疗设备，航空，汽车，铁路工业和机器人技术，都可以找到更为突出的例子。 形式化验证技术特别适合在必要的信任级别下提供必要的正确性保证。 可靠的CPS安全需要技术和工具来分析控制软件及其真实的物理效应，以保证 CPS的所有无限可能状态中的正确性。
在这一系列讲座中，我们将介绍定理证器者KeYmaera X的建模语言，KeYmaera X 是一个为混成系统设计的定理证明器。混成系统CPS 的数学模型，它将离散计算与其连续物理效应结合在一起。我们将学习用于分析混成系统的基础知识和证明技术，例如离散计算上的归纳法及其连续域上的对应，例如微分方程的微分不变量。一旦混成系统被证明是正确的，剩下的问题是用于验证的模型是否足以代表真实系统及其环境。我们将讨论ModelPlex方法，以合成可证明正确的监视器表达式，该表达式测试运行系统是否存在与验证模型的偏差。当监视器作为看门狗与真实系统上一起运行时，这些监视器会在偏差发生时启动紧急操作，以便以可证明的正确方式保持系统安全。
在整个讲座中，我们将研究地面机器人的模型作为运行示例。 这些示例将从KeYmaera X可以完全自动证明的简单任务开始(例如，将机器人直线驱动到充电站并停在那里)并进入更复杂的模型，在这些模型中需要手动交互或高级证明技巧(例如， 证明与转向和弯曲路径相关的性质)。
参与者将学习如何使用混成程序对混成系统进行建模，如何避免建模陷阱，以及如何证明安全性质(例如，机器人永远不会碰撞墙壁或永远不会错过充电站)。 为了探索安全验证概念，我们将通过其点击式Web界面和其策略编程语言与KeYmaera X进行交互。 策略提供了一种强大的方法，可以针对当前证明策略无法实现的案例自动执行通用或领域专用的证明搜索过程。
注册费用
前期注册：1000 RMB
后期注册：1200 RMB
SSFM 2018 日程
CAP项目研讨会
CAP 项目研讨会旨在促进来自不同领域的参与者齐聚北京，共同讨论项目成果以及未来的合作。会议邀请台湾中央研究院陈郁芳和的里雅斯特大学的Luca Bortolussi分别作基于高级自动机的程序终止检测算法和使用贝叶斯机器学习的参数化验证和合成问题的报告。
CONFESTA 大会网址
http://confesta2018.csp.escience.cn/
SSFM 2018 /CAP项目研讨会地点
北京市海淀区中关村南四街4号
中国科学院软件研究所
欢迎国内外学者及相关领域人士参与!
http://weixin.100md.com
返回 中国科学院软件研究所 返回首页 返回百拇医药