“信息科学理论研究前沿论坛”

会议日程

时间：2016年11月26-27日

地点：北京国际数学研究中心，镜春园78号院（怀新园）77201室

 

2016年11月26日，星期六

Morning

8:00-8:40   Registration

8:40-10:00  Session One: Hybrid Systems(Chair: 张立军)

詹乃军(ISCAS): Formal Verification of SDEs

佘志坤(BUAA): Under Approximating Backward Reachable Sets by Polytopes

10:00-10:30 Coffee Break

10:30-12:30  Session Two: Verification(Chair: 孙军)

贺飞(THU): Learning based Assume Guarantee Regression Verification

陈振邦(NUDT): Symbolic Verification of MPI Programs

秦胜潮(Teeside): Reasoning about Fences and Relaxed Atomics

12:30-14:00   Lunch

Afternoon

14:00-15:20  Session One: Program Analysis and Verification(Chair: 蒲戈光)

熊英飞(PKU): 浮点误差的自动查找

田聪(XDU): Model Checking via Dynamic Program Execution

15:20-15:50   Coffee Break

15:50-17:10  Session Two: Testing and Debugging (Chair: 熊英飞)

蒲戈光(ECNU): 覆盖驱动的自动测试研究进展

卜磊(NJU): Systematically Debugging IoT Control System Correctness for Home Automation

17:30-20:00   Dinner

2016年11月27日，星期日

Morning

9:00-10:20   Session One: Probabilistic Systems (Chair: 秦胜潮)

张立军(ISCAS): Probabilistic Model Checking

孙军(SUTD): Verification of Complex Systems Probabilistically through Learning Abstraction and Refinement

10:20-10:50   Coffee Break

10:50-12:10   Session Two: Software Specification and Analysis (Chair: 詹乃军)

陈立前(NUDT): 面向中断驱动型嵌入式软件的数值静态分析

赵永望(BUAA): 符合工业标准的操作系统内核形式规约与安全分析

12:10-14:00   Lunch

Afternoon

14:00-16:00   Free Discussion

16:00        Closing

 

 报告人报告摘要及个人简介

1. 詹乃军(ISCAS): Formal Verification of SDEs

Abstract

Probabilistic and stochastic behaviors are omnipresent in computer controlled systems, in particular, so-called safety-critical cyber-physical systems, because of fundamental properties of nature, uncertain environments, or simplifications to overcome complexity. Tightly intertwining discrete, continuous and stochastic dynamics complicates modeling, analysis and verification of stochastic hybrid systems. In the literature, this issue has been extensively investigated, but unfortunately, still remains challenging due to the difficulty of stochastic differential equations (SDEs). Most existing approaches are either not scalable, or not efficient, or not reliable because of poor precision. In this talk, we propose a promising solution to this challenge by showing that the reachability problems of SDEs can be reduced to the initial-boundary value problems of  a family of partial differential equations (PDEs), called advection-diffusion equations (ADEs), which can be well solved by well-developed solvers for ADEs. Compared with existing approaches, the advantages of our method is threefold: the first is its scalability, as it can be applied to any SDE; the second is its reliability, as the user can predefine  the tolerance of error, and our approach can give a reliable answer to a verification problem w.r.t. the error; the third is its efficiency, e.g., SDEs with high dimension are still doable.  A prototypical implementation and some case studies are provided.

Bio

詹乃军，博士，中科院软件所研究员，中国科学院大学教授，中国科学院特聘研究员，国家杰出青年基金获得者，博士生导师。现任中国科学院软件研究所计算机科学国家重点实验室副主任，中国计算机学会形式化方法专业组秘书长，《Formal Aspects of Computing》、

《Journal of Logical and Algebraic Methods in Programming》、《软件学报》、《计算机研究与发展》等编委，及多个国际学术组织任职。主要研究兴趣包括:实时、混成和嵌入式系统，程序验证，模态和时序逻辑，并发计算模型,程序形式语义等。

 

2. 佘志坤(BUAA): Under Approximating Backward Reachable Sets by Polytopes

Abstract

Under-approximations are useful for falsification of safety properties for nonlinear (hybrid) systems by finding counter-examples. Polytopic under-approximations enable analysis of these properties using reasoning in the theory of linear arithmetic. Given a nonlinear system, a target region of the simply connected compact type and a time duration, we in this paper propose a method using boundary analysis to compute an under-approximation of the backward reachable set. The under-approximation is represented as a polytope.The polytope can be computed by solving linear program problems. We test our method on several examples and compare them with existing methods. The results show that our method is highly promising in under-approximating reachable sets. Furthermore, we explore some directions to improve the scalability of our method.

Bio

佘志坤，北京航空航天大学数学与系统科学学院教授、博士生导师、研究生教学副院长。2014年度国家优秀青年科学基金项目获得者。

 

3. 贺飞(THU): Learning based Assume Guarantee Regression Verification

Abstract

Due to enormous resource consumption, model checking each revision of evolving systems repeatedly is impractical. To reduce cost in checking every revision, contextual assumptions are reused from assume-guarantee reasoning. However, contextual assumptions are not always reusable. We propose a fine-grained learning technique to maximize the reuse of contextual assumptions. Based on fine-grained learning, we develop a regressional assume-guarantee verification approach for evolving systems. We have implemented a prototype of our approach and conducted extensive experiments (with 1018 verification tasks). The results suggest promising outlooks for our incremental technique.

Bio

贺飞，博士，清华大学副教授。2002年7月毕业于国防科技大学计算机学院，获工学学士学位；2008年1月毕业于清华大学计算机系，获工学博士学位。自2008年起于清华大学软件学院任教。主要研究方向为形式化验证理论及其在嵌入式系统、软件系统中的应用。

 

4. 陈振邦(NUDT): Symbolic Verification of MPI Programs

Abstract

Message Passing Interface (MPI) is the standard paradigm of programming in high performance computing. Due to their high parallelism, MPI programs are difficult to write and error-prone. Analyzing MPI programs is also challenging because of non-determinism caused by program inputs and non-deterministic operations. Existing approaches for analyzing MPI programs either do not handle inputs or fail to support non-determinism for the mixed blocking and non-blocking mechanism. We present MPISE, the first symbolic execution based technique for verifying MPI programs that have both blocking and non-blocking operations. To ensure its soundness, we propose a lazy matching algorithm to safely handle non-deterministic operations. To improve its scalability, we employ model checking to guide path exploration and prune redundant paths during symbolic execution. We have implemented MPISE based on Cloud9 and PAT, and evaluated it on the verification of deadlock freedom for real-world MPI programs. Our experimental results are promising and demonstrate MPISE's effectiveness and efficiency.

Bio

Zhenbang Chen is an associate professor of the College of Computer, National University of Defense Technology, Changsha, China. He received the Ph.D. degree from the National University of Defense Technology in 2009. His current research interests include program analysis (especially symbolic execution) and formal methods, and their applications.

 

5. 秦胜潮(Teeside): Reasoning about Fences and Relaxed Atomics

Abstract

For efficiency reasons, weak (or relaxed) memory is now the norm on modern architectures. To cater for this trend, modern programming languages are adapting their memory models. The new C11 memory model allows several levels of memory weakening, including non-atomics, relaxed atomics, release-acquire atomics, and sequentially consistent atomics. Under such weak memory models, multithreaded programs exhibit more behaviours, some of which would have been inconsistent under the traditional strong (i.e. sequentially consistent) memory model. This makes the task of reasoning about concurrent programs even more challenging. The GPS framework, recently developed by Turon et al., has made a step forward towards tackling this challenge. By integrating ghost states, per-location protocols and separation logic, GPS can successfully verify programs with release-acquire atomics. In this paper, we present a program logic, an enhancement of the GPS framework, that can support the verification of a bigger class of C11 programs, that is, programs with release-acquire atomics, relaxed atomics and release-acquire fences. Key elements of our proposed logic include two new types of assertions, a more expressive resource model and a set of newly-designed verification rules.

Bio

2002 年获北京大学博士学位，2002-2004 年在新加坡国立大学攻读博士后，2005 年起在英国高校任教。主要研究领域包括软件形式化方法、程序理论、程序分析与验证、分离逻辑、数字物理融合系统等。

 

6. 熊英飞(PKU): 浮点误差的自动查找

Abstract

浮点数误差常常会导致严重的事故，找出程序中的浮点数误差常常。本报告介绍一种测试技术自动查找程序中的浮点误差。给定一个程序，本报告中介绍的技术自动查找一个输入来触发程序中的大误差。同时，目前常用的程序误差估算方法会受到精度特定运算的影响，本报告也同时介绍如何查找程序中的精度特定运算并消除它们的影响。

该报告主要源自报告人的ICSE15和FSE16论文内容。

Bio

熊英飞2009年毕业于日本东京大学。2009年-2011年在加拿大滑铁卢大学从事博士后研究。2012年加入北京大学，任“百人计划”研究员。熊英飞博士着眼于软件系统的质量问题，从发现和消除软件中的缺陷入手，取得了基于变化的演化缺陷修复理论和方法、配置缺陷修复理论和方法、高精度程序缺陷修复技术等一系列研究成果，在软件工程顶级期刊会议（ICSE、FSE、ASE、TSE）上发表了11篇论文，1篇被选为顶级期刊《IEEE TSE》首页论文。成果受到国际同行的关注和认可，总共被引用952次。熊英飞博士作为项目负责人承担了青年973项目一项，是软件工程领域首个也是唯一一个青年973项目。

 

7. 田聪(XDU): Model Checking via Dynamic Program Execution

Abstract

This talk presents a unified model checking approach where the program to be verified is written in a Modeling, Simulation and Verification Language (MSVL) program M and the desired property is specified with a Propositional Projection Temporal Logic (PPTL) formula P. Different from the traditional model checking approach, the negation of the desired property,  is translated into an MSVL program  M' first. Then whether M violates P can be checked by evaluating whether there exists a feasible execution of the new MSVL program (M and M'). This problem can be efficiently conducted with the compiler of MSVL namely MSV. The proposed approach has been implemented in a tool called UMC4MSVL which is capable in verifying real-world programs. 

Bio

西安电子科技大学计算机学院教授，博士生导师。分别于2004年，2007年和2009年在西安电子科技大学获学士、硕士和博士学位。于2010年10月1日至2011年3月31日在日本Hosei大学访问。2013年获国家自然科学基金优秀青年基金和教育部新世纪优秀人才计划资助。2014年获陕西省青年科技新星称号。

 

8. 蒲戈光(ECNU): 覆盖驱动的自动测试研究进展

Abstract

报告介绍了软件开发阶段如何进行自动化的单元测试，借助符号执行技术与模型检查技术，我们开发了针对各种覆盖准则的测试用例自动生成技术，支持例如语句，分支，边界，MC/DC，数据流等覆盖标准。在工业实践方面，我们开发了SmartUnit工具，在航空/轨道交通等行业进行了大规模的自动化测试工具。

Bio

蒲戈光，1978年生，男, 华东师范大学计算机科学与软件工程学院 教授/博士生导师，上海市高可信计算重点实验室副主任。武汉大学学士，北京大学博士。主要的研究领域包括软件形式化方法，程序分析、验证与测试。已发表学术论文60余篇，包括国际学术期刊12篇，国际学术会议50余篇。多篇论文发表于本领域的国际顶级会议，如SIGIR,FSE,ICSE FM等。研究工作被国际上的学者广泛引用，论文总被引进千余次。20曾获上海市青年科技启明星，教育部自然科学一等奖。目前担任多个国际学术会议的程序委员会委员，同时担任软件学报，JCST, 计算机学报，基金委面上项目的评审专家，并承担了基金委重点，863等10余项科研项目。

 

9. 卜磊(NJU): Systematically Debugging IoT Control System Correctness for Home Automation

Abstract

Advances and standards in Internet of Things (IoT) have simplified the realization of home automation. However, non-expert IoT users still lack tools that can help them to ensure the underlying control system correctness: user- programmable logics match the user intention. In fact, non- expert IoT users lack the necessary know-how of domain experts. This talk presents our experience in running a building automation service based on the Salus framework. Complementing efforts that simply verify the IoT control system correctness, Salus takes novel steps to tackle practical challenges in automated debugging of identified policy violations, for non-expert IoT users. First, Salus leverages formal methods to localize faulty user-programmable logics. Second, to debug these identified faults, Salus selectively transforms the control system logics into a set of parameterized equations, which can then be solved by popular model checking tools.

Bio

Lei Bu is currently an associate professor at Department of Computer Science and Technology, Nanjing University, P.R. China. He received his bachelor and PH.D. degree in Computer Science from Nanjing University in 2004 and 2010. He has been visiting scholar/students in institutes like Carnegie Mellon University, Microsoft Research Asia, Fondazione Bruno Kessler, and University of Texas at Dallas. 

His main research interests include formal method, model checking, hybrid system, cyber-physical system, software testing and analysis. He has published around 40 papers in leading journals and conferences like RTSS, TC, CAV, TPDS, STTT, STVR, DATE, VMCAI, FMCAD, CAV, FORTE and so on.

 

10. 张立军(ISCAS): Probabilistic Model Checking

Abstract

In this talk I'll present background theories for probabilistic model checking algorithms, including the Markov chains, Markov decision processes with respect to temporal logic extensions PCTL*. In particular, I'll present some recent efficient algorithms for probabilistic linear time properties. Then, I'll survey probabilistic model checking tools, and introduce a new format for the modelling language, which can be useful to establish a platform for comparing the existing probabilistic model checkers.

Bio

张立军，中国科学院软件研究所研究员，2013年入选“百人计划”。研究领域主要是基于马尔科夫模型及其扩展的概率并发系统的模型检验。作为模型检验的重要扩展,概率模型检验是热门前沿基础研究领域之一。学术成果在著名会议和杂志上发表,例如 CAV、CONCUR、LICS、POPL、ETAPS/TACAS、LMCS、 AAAI、Inf. & Comp.等。论文请参考:http://iscasmc.ios.ac.cn/?page_id=819。关注系统的形式验证的理论研究工作，同时也注重验证工具的开发及应用。

 

11. 孙军(SUTD): Verification of Complex Systems Probabilistically through Learning Abstraction and Refinement

Abstract

Precisely modeling complex systems like cyber-physical systems is often challenging, which may render model-based system verification techniques like model checking infeasible. To overcome this challenge, we propose a method called LAR to ‘verify’ such complex systems through a combination of learning, abstraction and refinement. Instead of starting with system modeling, our method takes a set of concrete system traces as input. The output is either a counterexample with a bounded probability of being a spurious counterexample, or a probabilistic model based on which the given property is ‘verified’. The model could be viewed as a proof obligation, i.e., the property is verified if the model is correct. It can also be used for subsequent system analysis activities like runtime monitoring. Our method has been implemented as a self-contained software toolkit. The evaluation results on multiple benchmark systems as well as a real-world water purification system show promising results.

 

Bio

Sun, Jun received Bachelor and PhD degrees in computing science from National University of Singapore (NUS) in 2002 and 2006. In 2007, he received the prestigious LEE KUAN YEW postdoctoral fellowship in School of Computing of NUS. Since 2010, he joined Singapore University of Technology and Design (SUTD) as an Assistant Professor. He was a visiting scholar at MIT from 2011-2012. Jun's research interests include software engineering, formal methods, software engineering, program analysis and cyber-security. He is the co-founder of the PAT model checker. 
 

12. 陈立前(NUDT): 面向中断驱动型嵌入式软件的数值静态分析

Abstract

Interrupts are a commonly used facility that introduces concurrency in embedded software. Meanwhile, embedded software often involves intensive numerical computations that have the potential to cause numerical run-time errors, and thus the technique of numerical static analysis holds a prominent position in checking the correctness of embedded software. However, few existing numerical static analysis methods consider interrupts. In this talk, we will present a numerical static analysis approach specifically for Interrupt-Driven Programs (IDPs). The main idea is to first sequentialize IDPs by a semantic sound program transformation and then to analyze the resulted sequential programs by numerical abstract interpretation enriched with newly designed abstract domains specific to the features of IDPs. Finally, we will show our experimental results conducted on a selection of benchmarks and real-world programs.

Bio

陈立前，国防科技大学计算机学院助理研究员。主要从事软件分析与验证、形式化方法领域研究工作。在ACM Transactions on Embedded Computing Systems、Science of Computer Programming、ESOP、SAS、VMCAI等期刊会议上发表学术论文40余篇，其中一篇获得 EMSOFT 2015 最佳论文提名。曾获军队科技进步二等奖1项。

 

13. 赵永望(BUAA): 符合工业标准的操作系统内核形式规约与安全分析

Abstract

操作系统隔离内核（Separation Kernel）在航空航天飞行器、国防装备、工业设备等得到了广泛应用。随着物联网、智能设备以及工业互联网等新型网络环境的快速发展，有效支撑两类安全（Security和Safety）是操作系统隔离内核的发展趋势。本报告介绍基于ARINC653标准的隔离内核形式规约、安全保持的逐步求精方法、基于定理证明的安全分析等。在规约开发和证明过程中，我们发现了ARINC 653标准中的11个安全缺陷。同时，我们对符合ARINC 653的一个工业级内核（VxWorks 653）和两个开源内核（XtratuM、POK）的源代码进行了验证，发现了其中7个安全缺陷。相关成果已经得到了美国波音公司等的认可，并被纳入ARINC 653标准的新版本。

Bio

赵永望，博士，副教授，CCF高级会员、 CCF YOCSEF 委员、国家信息技术标准化技术委员会 SOA 分委员会专家。主要研究方向包括形式逻辑与验证、操作系统内核及安全、安全攸关系统与模型驱动方法等。主持和参与了国家自然基金课题、国家核高基重大专项、新加坡国家研究署（NRF）重大项目等十余项。主持开发的国产Web 服务中间件平台在国内中间件厂商、航空/航天企业得到应用，获得中国电子学会电子信息科技一等奖。近年来，与新加坡南洋理工大学、欧盟EURO-MILS重大项目、法国科学院IRIT研究所等合作开展操作系统内核及安全验证、形式化方法等研究工作。

 

北京大学地图

  

 

20161115161924952325.png