【会议通知】CONFESTA 2018
2018/7/13 7:01:21 中国科学院软件研究所
并发理论与形式化验证联合大会
CONCUR 2018
FORMATS 2018
QEST 2018
SETTA 2018
中国 北京
2018年8月24日—9月8日
摘要:最近三十年中在验证领域，显著的一个进步是验证有限状态模型的时序规范的算法式方法的发展。然而仍然有评论批评这种方法：验证是在已经将大量资源投入到设计开发中之后被完成的。由于设计总是包含错误，验证容易简单地编程调试过程的一部分。批评者认为，期望的目标是在设计开发过程中使用时序规范，以保证正确设计的开发。这称为temporal synthesis。在本次演讲中，我将回顾六十年来temporal synthesis问题的研究，描述为解决这一问题而开发的自动机理论方法，并描述该研究项目的成功与失败。
简历: Moshe Y. Vardi是莱斯大学的计算工程乔治杰出服务教授和 Ken Kennedy信息技术研究所所长。他获得三项IBM杰出创新奖， ACM SIGACT Goedel奖，ACM Kanellakis奖，ACM SIGMOD Codd奖，欧洲科学院布莱士·帕斯卡奖章，IEEE计算机学会Goode奖，EATCS杰出成就奖，SURA(东南高校研究协会)的杰出科学家奖和EATCS(欧洲理论计算机科学协会) 邱奇奖。他是500多篇论文的作者和共同作者，著有两本专著：《知识推理》和《有限模型理论及其应用》。他是ACM(计算机协会)、AAAI(美国人工智能协会)、AAAS(美国科学促进协会)、EATCS(欧洲理论计算机科学协会)、IEEE(电气电子工程师学会)以及SIAM(工业和应用数学会)的会士。他是NAE(美国国家工程院)和NAS(美国国家科学院)、美国文理科学院，EurASc(欧洲科学院)和AE(欧洲科学院)的院士。他拥有德国萨尔大学，法国奥尔良大学，巴西UFRGS大学和比利时列日大学的荣誉博士学位。在担任总编辑十年之后，他目前是ACM通讯的高级编辑。
CONCUR 2018
摘要: 互模拟是并发理论为了比较不确定性进程行为的基础概念。它在不同的理论中都有很好的刻画，例如不动点理论，模态逻辑，博弈论，余代数等。在这次演讲中，我们回顾在概率进程和量子进程的互模拟的合理概念的构造和刻画中使用的一些关键思想。在某种程度上，从概率并发理论到量子并发理论的转变是平滑和自然的。但是，还需要引入新的想法。我们尚未达到使用自动工具实现的互模拟形式化地验证量子通信协议和量子算法的阶段。我们将会讨论最近在这方向的一些努力。
简历: 邓玉欣本科 (1999) 和硕士 (2002) 毕业于上海交通大学并于2005年于巴黎高科矿业学院获得博士学位。他曾任澳大利亚新南威尔士大学(2005-2006)的副研究员，中国上海交通大学副教授(2006-2015)，美国卡内基梅隆大学访问学者(2011年)，联合国教科文组织法国总部的专家(2012-2014)。 2015年，他加入华东师范大学担任教授。邓博士的研究兴趣包括并发理论，特别是关于进程演算和编程语言的形式语义，以及安全协议和分布式算法的形式验证。著有一本概率进程语义专著。
摘要：如果互斥算法的正确性不依赖于组件的相对速度，则它被称为速度无关。着名的互斥协议，如Dekker算法，Peterson算法和Lamport的面包店算法，都是速度无关的。
在这次演讲中，我将论证速度无关的互斥可能无法在标准硬件上实现，这取决于我们如何相信对某个内存位置的读取和写入操作真正被执行。然而，它可以在电路上实现。
这建立在之前那些表明在标准进程代数中无法准确地建模互斥的工作基础上。
简历：Rob van Glabbeek,澳大利亚新南威尔士大学计算机科学与工程学院教授，同时隶属于斯坦福大学的计算机科学系。他的主要研究兴趣有表示分布式系统的并发语义、数学模型和形式语言以及对它们的性质的验证，尤其是关于这些模型和语言的多种可能性的基础工作。在这一领域的主要会议和期刊上共发表了百余篇论文。
Rob van Glabbeek在并行计算理论研究方面享有很高的国际声誉。通过将当前对分支时间观点和对因果关系的观点共同发展为并发当中正交但相互作用的维度，为交错语义社区和真并发社区的调和做出了特别的贡献。他众所周知的一些贡献是线性时间分支时间谱，分支互模拟(与PeterWeijland合作)和动作精化(与UrsulaGoltz合作)。最近，自2015年以来，他与Peter H?fner一起研究了公平性概念以及在标准进程代数中刻画公平调度程序或互斥协议的可能(或不可能)性。此外，他还组织了关于结合组合性和并发性、逻辑、语言和信息、 UML语言、工作流管理、Web服务和业务流程建模、自动和半自动系统验证、结构操作语义、以及嵌入式系统的形式化方法等方向的专题讨论会。他是EPTCS(理论计算机科学电子学报)的主编，IANDC(信息与计算)以及 TCS(理论计算机科学)编辑委员会成员，并曾在数十个程序委员会任职。
摘要：数学结构是基于代数结构的密码系统计算所必需的。它们通常使用汇编语言编写，并手动优化以提高效率。我们开发了一种混合技术来验证由OpenSSL和boringSSL中的汇编代码实现的数学结构。我们的技术将数学结构的代数规范转化为代数问题。代数问题反过来由计算机代数系统Singular解决。该技术还将溢出和范围检查转换为SMT求解器中的位向量理论。我们报告了关于在Curve25519和NIST P-256中的大有限域上验证算术计算的案例研究，以及X25519中的Montgomery Ladderstep。
简历：王柏尧，台湾中央研究院资讯科学研究所研究员。于2008年至2012年担任中央研究院副研究员，2009年至2011年担任INRIA特邀教授，2009年至2010年任清华大学副教授，2009年至2012年任台湾大学副教授，2003年至2008年担任中央研究院助理研究员，2004年至2009年任台湾大学助理教授。他的研究兴趣是逻辑及其在计算机科学中的应用。他主要在形式验证方向开展研究工作。过去他一直致力于组合推理，程序验证，基于学习的验证技术。最近，他的研究兴趣在验证安全库(如OpenSSL和boringSSL)加密原语的汇编实现。他还在中央研究院开展跨学科隐私研究项目。
FORMATS 2018
摘要：关于不确定性的推理是许多信息物理融合系统应用实际部署中的基本挑战之一。目前人们已经提出了几种能够抓住环境不确定性的模型，这些模型通常是参数模型，这些模型具有关于系统的时间演化的马尔可夫假设或者关于不确定性的高斯假设。在本次演讲中，我们提出了一个基于随机时序逻辑的创建数据驱动的环境抽象的框架。这种逻辑允许将基于时序逻辑的抽象的能力与强大的随机建模技术相结合。我们的框架允许使用广义主方程构建随机模型，这些模型可以被视为非参数模型，并且捉住了系统变量的概率随时间的动态演化。此外，我们展示了如何从这样的模型中自动推断基于时序逻辑的抽象。我们举例说明了这种框架的应用，并强调了这种方法中的一些开放性问题和挑战。
简历：Jyotirmoy V. Deshmukh(Jyo)是美国洛杉矶南加州大学维特比工程学院计算机科学系的助理教授。在加入南加州大学之前，他曾在丰田汽车北美研发部门担任首席研究工程师。他从德克萨斯大学奥斯汀分校获得了博士学位，并且曾是宾夕法尼亚大学的博士后研究员。 Jyo的研究兴趣包括信息物理融合系统的分析、设计、验证和合成等领域。他在嵌入式控制软件的认证和验证技术方面拥有丰富的经验，他目前的研究重点是信息物理融合系统的形式化方法与机器学习和AI算法的交叉领域。
摘要：本报告分析了实时系统模型的应用，特别是信息物理融合系统，它将物理子系统的实时行为与大部分非实时的软件行为混合在一起。它考察了模型在工程和科学中的使用方式，表明使用模型的两种互补方式可以得出关于如何处理实时系统建模问题的不同结论。本次报告主张更多地使用工程风格的建模，模型更像是想要的行为的规范，而不是对某些预先存在的系统的描述。最后，这主张在工程风格的建模中，确定性是一种极其有价值的特性。
简历：Edward A. Lee是加州大学伯克利分校EECS的Robert S. Pepper杰出教授。他是多本书籍和300多篇论文的作者，并在全球各地举办了170多场主题演讲和其他邀请演讲。 Lee的研究重点是信息物理融合系统，它将物理动力学与软件和网络相结合。他的专注于使用确定性模型作为此类系统的工程工具包的核心部分。他是iCyPhy(伯克利工业信息物理融合系统研究中心)的主任以及伯克利托勒密项目的负责人。从2005年至2008年，他担任电子工程系主任，然后担任加州大学伯克利分校电子工程和计算机科学学系主任。他领导了几个有影响力的开源软件包的开发，特别是Ptolemy及其衍生产品。从1979年到1982年，他是新泽西州霍尔姆德尔贝尔实验室的技术人员。他是BDTI公司的联合创始人，并为许多其他公司提供咨询。他是IEEE会士，曾获得科学基金委总统青年科学家奖，1997年获得Frederick Emmons Terman工程教育奖，并获得IEEE实时系统技术委员会(TCRTS)颁发的2016年杰出技术成就和领导奖。
QEST 2018
摘要：本报告概述了量化信息流分析(QIF)领域的最新进展。研究的主题是由秘密数据和可观察输出之间的相关性引起的允许对手对敏感信息做出推断的信息流。该研究特别具有挑战性，因为完美通常是难以达成的，因为出于功能或实践中的原因必须接受一些不想要的信息流。 QIF理论提供了系统的方法以操作上重要的方式量化这些信息“泄漏”，然后对攻击对手的利益和另一种实现之间的比较进行限制。该理论在许多案例研究中得到了证明，该案例研究显示了如何将量化信息流分析应用于实际场景。
简历：Kostas Chatzikokolakis是法国CNRS(法国国家科学研究中心)的副研究员。他从巴黎综合理工学院获得计算机科学博士学位。他的工作专注于是安全和隐私，特别是量化信息流、位置隐私和差分隐私，以及概率验证和并发。他发表了50多篇研究论文，并参与了40个国际会议和研讨会的程序委员会，其中领域中知名的会议，包括安全和隐私(PETS，CSF，POST)、数据库(ICDE)、Web技术(WWW)、编程语言(ESOP)和形式化方法(ICFEM)。他目前担任隐私增强技术研讨会(PETS)的程序委员会主席。
Mark Wallace
莫纳什大学信息技术学院副院长
Opturion公司创始人
报告题目：约束与第四次工业革命
摘要：许多公司通过减少蓝领人力和提高效率来寻求在车间中省钱。然而，数据分析的革命实际上可以大大节省白领管理的人力资源。本演讲着重于优化软件，除了讲述真实的危机，还将描述能够自我运行的新一代公司。我们讨论约束规规划技术、技术转移以及实现这一目标所需的行业接受度。
简历：Mark Wallace教授探索了约束规划在解决工业和社会重大问题方面的潜力和局限性。他对结合数学规划、人工智能和元启发式的规划和调度方法特别感兴趣，他的研究已经形成了一系列优化平台： ECLiPSe，G12和MiniZinc。它们能够准确地模拟复杂问题，并且能够快速解决大规模实例。 他创立了Opturion公司，该公司部署G12解决了澳大利亚皇家飞行医生服务组织和许多其他澳大利亚公司的问题。
SETTA 2018
摘要：利用或调整人工智能技术解决软件工程任务(尤其是工具自动化)的研究和实践已经存在了几十年。最近研究界的努力一直在解决一系列问题，例如，如何定义或确定软件工程工具中的智能水平，如何在软件工程工具中提供高水平的智能，如何协同整合机器智能和人类智能(例如，领域知识或洞察力)从而有效地解决具有挑战性的软件工程任务。另一方面，随着人工智能软件在社会中越来越重要和普及，研究界最近的努力也在探索软件工程解决方案来提高开发人工智能软件的效率和人工智能软件的可靠性。智能软件工程的新兴领域是专注于两个方向：(1)在软件工程任务的解决方案中注入智能; (2)为AI软件提供软件工程解决方案。本演讲将分享智能软件工程的观点以及智能软件工程两个方向的实例研究。
简历：Tao Xie是美国伊利诺伊大学厄巴纳-香槟分校计算机科学系的教授和Willett学者。他曾在Microsoft Research担任访问研究员。他的研究兴趣是在软件工程领域内，专注于软件测试、程序分析、软件分析、软件安全和教育软件工程。他获得了NSF(美国国家科学基金会) CAREER奖，微软研究杰出合作者奖，Google教师研究奖，IBM爵士创新奖以及三次IBM教师奖。他是ACM杰出演讲者，是IEEE计算机学会杰出访客。他是ACM杰出科学家和IEEE会士。
简历：Hongseok Yang是韩国KAIST(韩国科学技术院大学)计算机学院的教授。他的研究领域是编程语言，但他主要研究编程语言与其他领域之间的交叉领域，例如机器学习，统计学，概率论和分布式系统。他于2001年获得美国伊利诺伊大学厄巴纳-香槟分校计算机科学系的博士学位。然后，他从2001年到2003年首次在KAIST担任博士后研究员，2003年至2006年在首尔国立大学担任博士后研究员。在完成博士后训练后，他在英国伦敦大学玛丽皇后学院担任讲师(相当于助理教授职位)大约五年。在这之后他到牛津大学担任副教授(2011-2014)，然后担任全职教授(2014-2017)。在牛津大学期间，他还在最美丽的牛津大学之一伍斯特学院(WorcesterCollege)获得了教学奖学金。他于2017年加入KAIST。他是2016年CAV奖的共同获奖者，获得了2014年PLDI的杰出论文奖和2012年CONCUR的最佳论文奖，并于2007年至2012年期间获得了EPSRC(英國工程和自然科學研究委員會)高级研究资助。
SSFM暑期班
简历：Joost-Pieter Katoen是德国亚琛工业大学的杰出教授，并在荷兰恩斯赫德的屯特大学担任兼职教授。他是欧洲科学院院士，并获得丹麦奥尔堡大学的荣誉博士学位。他是牛津大学、奥地利科学技术研究所和悉尼麦考瑞大学的访问教授。他的研究兴趣包括形式方法，模型检测，并发理论和概率计算。 2018年，他获得了ERC高级研究基金。他与人合著了170多篇会议论文，70篇期刊论文和《模型检测原理》一书。 Katoen教授是ETAPS指导委员会主席，CONCUR，QEST和FORMATS会议指导委员会成员。
摘要：概率程序结合了概率论、统计学和从建模的角度来说最重要的编程语言。它们允许以相当简洁的方式对更大一类的模型进行建模。现代概率程序语言的全部潜力来自于根据观察到的数据自动推断模型中未观察到的变量的过程。正如一些研究人员所说：“概率程序的目标是使程序员能够接触概率建模和机器学习。”
概率程序引导自主机器人是安全机制的核心，其中包含随机算法，并用人工智能推断关于大量不确定数据的统计结论。
在本系列讲座中，我将介绍概率程序的主要概念，并讨论如何使用经典的程序验证来解决Dijkstra问题，例如：这些程序是否计算出人们期望他们做的事情？他们终止了吗？有什么概率？他们消耗了多少资源？贝叶斯网络的应用将显示如何通过使用程序验证以完全自动化的方式获得有关分析此类网络的深入信息。
简历：Holger Hermanns教授是德国萨尔布吕肯萨尔大学的教授，担任可靠系统和软件实验室主任。此前，他曾在德国埃尔兰根-纽伦堡大学、荷兰特屯特大学和法国格勒诺布尔罗纳-阿尔卑斯地区的法国国家信息与自动化研究所担任过职务，并曾担任萨尔大学数学与计算机科学学院院长。他的研究兴趣包括并发系统的建模和验证，资源感知嵌入式系统，组合性性能和可靠性评估，以及它们在能源信息学中的应用。 Holger Hermanns撰写或合著了200多篇同行评审的科学论文。他曾担任CAV，CONCUR，TACAS和QEST等主要国际会议的计划委员会主席，并在十几个国际会议和研讨会上发表了主题演讲。他是ETAPS和TACAS指导委员会的成员。他是“Friends of Dagstuhl e.V.”协会的主席，以及 “ETAPS e.V.” 协会的副主席。 Holger Hermanns获得荷兰“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进行交互。 策略提供了一种强大的方法，可以针对当前证明策略无法实现的案例自动执行通用或领域专用的证明搜索过程。
(图片来源：中国科学院大学新闻网《光影国科大》栏目、国际会议中心)
扫描大会网站二维码 关注大会讯息
文章来源：计算机科学国家重点实验室
http://weixin.100md.com
返回 中国科学院软件研究所 返回首页 返回百拇医药