您的位置:首页 > 科学研究 > 学术科研

可信软件系统工程(国际)春季学校

发布时间:2017-04-13 来源:本站原创 作者:本站编辑   浏览次数:

 

可信软件系统工程(国际)春季学校

Spring School on Engineering Trustworthy Software Systems

 

可信软件系统工程(国际)春季学校由西南大学计算机与信息科学学院、软件学院举办。自2014年以来,我们已成功举办过两届,这是第三届。本届春季学校邀请了澳大利亚昆士兰大学Ian Hayes教授、微软研究院Rustan Leino首席研究员、美国中佛罗里达大学Gary T. Leavens教授、南京大学马晓星教授、德国弗莱堡大学Andreas Podelski教授、SRI国际计算机科学实验室Natarajan Shankar教授、荷兰阿姆斯特丹大学Maarten de Rijke教授、美国西密歇根大学Zijiang Yang教授和越南国立大学Dang Van Hung教授,共9名海内外著名的软件工程领域专家和学者,以专题讲座、学术沙龙、互动交流等形式,为学员展现计算机软件系统工程领域最前沿的软件工程方法、技术和实用性工具。可信软件系统工程(国际)春季学校的招生范围包括在读硕士研究生、博士研究生、高校相关专业青年教师和研究人员、以及计算机软件产业从业者。本届春节学校学员人数共计80余人,分别来自30多个高校和科研院所。通过春季学校,各位学员们不但能学习到最先进的软件工程方法与前沿技术,还能直接与多位国内外专家面对面互动和交流,从而建立起与业内专家合作进行软件工程领域的科学、教育研究的前期基础。

每届春季学校的讲义将汇集成册,由Springer出版社以LNCS Tutorial www.springer.com/lncs)的形式出版。

 

时间安排

主讲人/主持人

单位

题目

41708:00-08:30

Prof. Zili Zhang

Southwest University

Opening Session          

(1) Welcome Speech by Vice President of SWU, Prof. Yanqiang Cui

(2) SETSS Briefing by Prof. Zhiming Liu

(3) Ceremony of Guest Professorship of Prof. Zhou Chaochen

(4) School Photo Taking

41708:30-09:30

Prof. Ian Hayes

The University of Queensland, Australia

Rely/Guarantee Thinking (Part I)

41709:45-10:45

Prof. Gary T. Leavens

The University of Central Florida

Hoare-Style Specification and Verification of Object-Oriented Programs with JML (Part I)

41711:00-12:00

Prof. Ian Hayes

The University of Queensland, Australia

Rely/Guarantee Thinking (Part II)

41714:00-15:00

Prof. Gary T. Leavens

The University of Central Florida

Hoare-Style Specification and Verification of Object-Oriented Programs with JML (Part II)

41715:15-16:15

Prof. Natarajan Shankar

The SRI International Computer Science Laboratory

Logic, Specification, Verification, and Interactive and Proof (Part I)

41716:30-17:30

Prof. Natarajan Shankar

The SRI International Computer Science Laboratory

Logic, Specification, Verification, and Interactive and Proof (Part II)

41719:00-21:00

Prof. Maarten de Rijke

The University of Amsterdam

Agents that Get the Right Information to the Right People in the Right Way

41808:30-09:30

Prof. Ian Hayes

The University of Queensland, Australia

Rely/Guarantee Thinking (Part III)

41809:45-10:45

Prof. Gary T. Leavens

The University of Central Florida

Hoare-Style Specification and Verification of Object-Oriented Programs with JML (Part III)

41811:00-12:00

Prof. Natarajan Shankar

The SRI International Computer Science Laboratory

Logic, Specification, Verification, and Interactive and Proof (Part III)

41814:00-15:00

Prof. Ian Hayes

The University of Queensland, Australia

Rely/Guarantee Thinking (Part IV)

41815:15-16:15

Prof. Gary T. Leavens

The University of Central Florida

Hoare-Style Specification and Verification of Object-Oriented Programs with JML (Part IV)

41816:30-17:30

Prof. Natarajan Shankar 

The SRI International Computer Science Laboratory

Logic, Specification, Verification, and Interactive and Proof (Part IV)

41908:30-09:30

Prof. Gary T. Leavens

The University of Central Florida

Hoare-Style Specification and Verification of Object-Oriented Programs with JML (Part V)

41909:45-10:45

Prof. Ian Hayes

The University of Queensland, Australia

Rely/Guarantee Thinking (Part V)

41911:00-12:00

Prof. Natarajan Shankar

The SRI International Computer Science Laboratory

Logic, Specification, Verification, and Interactive and Proof (Part V)

41914:00-15:00

Prof. Gary T. Leavens

The University of Central Florida

Hoare-Style Specification and Verification of Object-Oriented Programs with JML (Part VI)

41915:15-16:15

Prof. Ian Hayes

The University of Queensland, Australia

Rely/Guarantee Thinking (Part VI)

41916:30-17:30

Prof. Natarajan Shankar

The SRI International Computer Science Laboratory

Logic, Specification, Verification, and Interactive and Proof (Part VI)

42008:30-09:30

Prof. Andreas Podelski

The University of Freiburg

Software Model Checking with Automizer (Part I)

42009:45-10:45

Prof. K. Rustan M. Leino

Microsoft Research

Writing programs and proofs (Part I)

42011:00-12:00

Prof. Xiaoxing Ma

Nanjing University

Engineering Self-Adaptive Software-Intensive Systems (Part I)

42014:00-15:00

Prof. Andreas Podelski

The University of Freiburg

Software Model Checking with Automizer (Part II)

42015:15-16:15

Prof. K. Rustan M. Leino

Microsoft Research

Writing programs and proofs (Part II)

42016:30-17:30

Prof. Xiaoxing Ma

Nanjing University

Engineering Self-Adaptive Software-Intensive Systems (Part II)

42019:00-21:00

Dr. Dang Van Hung

Vietnam National University, Hanoi

A Model for Real-time Concurrent Interaction Protocols in Component Interfaces

42108:30-09:30

Prof. K. Rustan M. Leino

Microsoft Research

Writing programs and proofs (Part III)

42109:45-10:45

Prof. Xiaoxing Ma

Nanjing University

Engineering Self-Adaptive Software-Intensive Systems (Part III)

42111:00-12:00

Prof. Andreas Podelski

The University of Freiburg

Software Model Checking with Automizer (Part III)

42114:00-15:00

Prof. K. Rustan M. Leino

Microsoft Research

Writing programs and proofs (Part IV)

42115:15-16:15

Prof. Xiaoxing Ma

Nanjing University

Engineering Self-Adaptive Software-Intensive Systems (Part IV)

42116:30-17:30

Prof. Andreas Podelski

The University of Freiburg

Software Model Checking with Automizer (Part IV)

42119:00-21:00

Prof. Zijiang Yang

Western Michigan University

Optimizing Symbolic Execution for Software Testing

42208:30-09:30

Prof. Xiaoxing Ma

Nanjing University

Engineering Self-Adaptive Software-Intensive Systems (Part V)

42209:45-10:45

Prof. Andreas Podelski

The University of Freiburg

Software Model Checking with Automizer (Part V)

42211:00-12:00

Prof. K. Rustan M. Leino

Microsoft Research

Writing programs and proofs (Part V)

42214:00-15:00

Prof. Xiaoxing Ma

Nanjing University

Engineering Self-Adaptive Software-Intensive Systems (Part VI)

42215:15-16:15

Prof. Andreas Podelski

The University of Freiburg

Software Model Checking with Automizer (Part VI)

42216:30-17:30

Prof. K. Rustan M. Leino

Microsoft Research

Writing programs and proofs (Part VI)

42219:00-21:00

Prof. Zhiming Liu

Southwest University

CCF FM Education Working Group Meeting

 

讲座题目:Rely/Guarantee Thinking

主讲人:Prof. Ian Hayes

    间:2017417日上午8:3011:00418日上午8:30、下午14:00419日上午9:45、下午15:15

    点:西南大学计信院学术报告厅(25教一楼0114

主办单位:西南大学计算机与信息科学学院 软件学院

 

主讲人简介:Ian Hayes is a Professor of Computer Science at the University of Queensland, Australia. His research interests focus on formal methods for the specification and development of software and systems. He has worked on the Z specification notation, and specification and refinement of real-time systems. His most recent research has focused on the specification and refinement of concurrent systems, along with an algebraic approach to defining its semantics with the aim of providing tool support.

 

内容摘要:The rely/guarantee approach to reasoning about a concurrent process makes the use of a rely condition to abstractly represent the assumptions the process makes about interference from its environment and a guarantee condition to represent the interference it imposes on its environment. The general view of rely/guarantee thinking appears to apply to a very wide range of applications: it facilitates the development and formal proof of intricate code — at the other extreme, it provides a framework for deriving the specification of control systems that respond to –and actuate– physical systems that interact with the physical world. In the last couple of years, the way of recording rely assumptions and guarantee commitments has been recast into a style similar to the refinement calculus. This results in a much more algebraic feel to reasoning about rely/guarantee thinking and the laws of this calculus will be explained and demonstrated on examples.

 

讲座题目:Hoare-Style Specification and Verification of Object-Oriented Programs with JML

主讲人:Prof. Gary T. Leavens

    间:2017417日上午9:45、下午14:00418日上午9:45、下午15:15419日上午8:30、下午14:00

    点:西南大学计信院学术报告厅(25教一楼0114

主办单位:西南大学计算机与信息科学学院 软件学院

 

主讲人简介:Gary T. Leavens is a professor and chair of the department of Computer Science at the University of Central Florida. Previously he was a professor at Iowa State University, where he started in 1989, after receiving his Ph.D. from MIT. Before his graduate studies at MIT, he worked at Bell Telephone Laboratories in Denver, Colorado. Professor Leavens was general chair for the SPLASH 2012 conference, and research program committee chair for the 2009 OOPSLA conference. He was the research results program committee chair for the Modularity 2015 conference. See http://www.cs.ucf.edu/~leavens for more information on his research.

 

内容摘要:These lectures will address the problem of specification and verification of sequential object-oriented (OO) programs, which use subtyping and dynamic dispatch. First we will describe the semantics of class-based object-oriented languages with mutable objects, such as Java. Then we will describe the problems of applying Hoare-style reasoning to OO programs in a modular way. We look in detail at the key notions of refinement, modular verification, and modular correctness. This leads to a detailed discussion of behavioral subtyping and supertype abstraction. Finally we discuss specification inheritance, its relationship to behavioral subtyping, and how these concepts are embodied in JML.

 

讲座题目:Logic, Specification, Verification, and Interactive and Proof

主讲人:Prof. Natarajan Shankar

    间:2017417日下午15:1516:30418日上午11:00、下午16:30419日上午11:00、下午16:30

    点:西南大学计信院学术报告厅(25教一楼0114

主办单位:西南大学计算机与信息科学学院 软件学院

 

主讲人简介:Prof. Natarajan Shankar is a Principal Scientist at the SRI International Computer Science Laboratory. He is the co-developer of a number of cutting-edge tools (http:github.com/SRI-CSL) for automated reasoning and formal verification spanning interactive proof (PVS), model checking (SAL), SMT solving (Yices), and probabilistic inference (PCE). Dr. Shankar is an SRI Fellow and a co-recipient of the 2012 CAV Award.

 

内容摘要:Formalization plays a key role in computing in disciplines ranging from hardware and distributed computing to programming languages and hybrid systems. In this course, we explore the use of SRI's Prototype Verification System (PVS)[http://pvs.csl.sri.com] in formal specification and interactive proof construction. PVS and other proof assistants like ACL2, Coq, HOL, HOL Light, Isabelle, and Nuprl, have been used to formalize significant tracts of mathematics and verify complex hardware and software systems. In the lectures, we will explore the formalization of both introductory and advanced concepts from mathematics and computing. We use PVS to interactively construct proofs and to define new proof strategies.

 

讲座题目:Software Model Checking with Automizer

主讲人:Prof. Andreas Podelski

    间:2017420日上午8:30、下午14:00421日上午11:00、下午16:30422日上午9:45、下午15:15

    点:西南大学计信院学术报告厅(25教一楼0114

主办单位:西南大学计算机与信息科学学院 软件学院

 

主讲人简介:Prof. Andreas Podelski works in the area of programming languages, specifically on program analysis and verification. He is an Associate Editor of the journals ToPLaS, FMSD, JAR, and STTT. He has served as the chair or as a member of the program committee of over 50 conferences and he has been the invited speaker at over 20 conferences. He did his Master studies in Münster, Germany, his PhD in Paris, France, and a PostDoc in Berkeley, CA. He holds the Chair of Software Engineering at the University of Freiburg since 2006. He has spent sabbaticals for research at MSR Redmond, ENS Paris, MSR Cambridge, and Stanford Research Institute.

 

内容摘要:We present a new approach to the verification of programs. The approach is embodied in the tool Automizer. Automizer has won this year's gold medal at SV-Comp (the second time in a row). We can decompose the set of behaviors of the given program (whose correctness we want to prove) according to sets of behaviors for which we already have a proof. We can construct a program from the correctness proof of a sequence of statements. A sequence of statements is a simple case of a program (a straight-line program). At the same time, a sequence of statements is a word over a finite alphabet (a word that can be accepted by an automaton). Just as we ask whether a word has an accepting run, we can ask whether a sequence of statements has a correctness proof (of a certain form). The automaton accepts exactly the sequences that do. We construct programs from proofs, repeatedly, until the constructed programs together cover all possible behaviors of the given program (whose correctness we want to prove). A crucial step here is the covering check. This step is based on algorithms for automata (inclusion test, minimization, ...). We explain the approach for a wide range of verification problems: safety, termination, liveness; with (possibly recursive) procedures, multi-threaded, with possibly unboundedly many threads).

 

讲座题目:Writing programs and proofs

主讲人:Prof. K. Rustan M. Leino

    间:2017420日上午9:45、下午15:15421日上午8:30、下午14:00422日上午11:00、下午16:30

    点:西南大学计信院学术报告厅(25教一楼0114

主办单位:西南大学计算机与信息科学学院 软件学院

 

主讲人简介:Rustan Leino is Principal Researcher in the Research in Software Engineering (RiSE) group at Microsoft Research, Redmond and Visiting Professor in the Department of Computing at Imperial College London. He is known for his work on programming methods and program verification tools, and is a world leader in building automated program verification tools. One of these tools is the language and verifier Dafny. Leino is an ACM Fellow. Prior to Microsoft Research, Leino worked at DEC/Compaq SRC. He received his PhD from Caltech (1995), before which he designed and wrote object-oriented software as a technical lead in the Windows NT group at Microsoft. Leino collects thinking puzzles on a popular web page and hosts the Verification Corner channel on youtube.

 

内容摘要:Reasoning about programs and understanding how to write proofs are important skills for software engineers. In this course, you will learn techniques of how to reason about programs, both imperative programs and functional programs. For imperative programs, this includes the concepts of assertions, pre- and postconditions, and loop invariants. For functional programs, this additionally includes lemmas, proof calculations, and mathematical induction. Throughout the course, the Dafny language and verifier will be used.

 

讲座题目:Engineering Self-Adaptive Software-Intensive Systems

主讲人:Prof. Xiaoxing Ma

    间:2017420日上午11:00、下午16:30421日上午9:45、下午15:15422日上午8:30、下午14:00

    点:西南大学计信院学术报告厅(25教一楼0114

主办单位:西南大学计算机与信息科学学院 软件学院

 

主讲人简介:Xiaoxing Ma is a professor and the deputy director of the Institute of Computer Software at Nanjing University. His research interests include self-adaptive software systems, software architectures, and middleware systems. Xiaoxing co-authored more than 60 peer-reviewed papers, some of which were published in major software engineering conferences and journals such as FSE/ICSE/ASE and IEEE TSE/TC/TPDS. He has directed and participated over a dozen research projects funded by the National Natural Science Foundation and the Ministry of Science and Technology of China. He has also served actively in technical program committees of various international conferences and workshops.

 

内容摘要:Modern software-intensive systems often need to dynamically adapt to the changes in the environment in which they are embedded and in the requirements they must satisfy. Engineering self-adaptation in software is challenging due to the lack of systematic engineering methods and proper enabling techniques. In this tutorial, we are going to discuss some recent advances in software engineering for self-adaptive systems, with topics covering the sensing and understanding of systems' environmental context, the model-based and control theory-based approaches to adaptation decision making, and the actuation of adaptation decisions through dynamic software updating.

 

 

沙龙主题:Agents that Get the Right Information to the Right People in the Right Way

主讲人:Prof. Maarten de Rijke

    间:2016417日晚上7:00

    点:西南大学计信院学术报告厅(25教一楼0114

主办单位:西南大学计算机与信息科学学院 软件学院

 

主讲人简介:Maarten de Rijke, professor at the University of Amsterdam, Netherlands, leads the prestigious Information Language Processing and System (ILPS) laboratory in the field of information retrieval. He has published more than 670 articles in the top conferences and journals of information retrieval, machine learning, natural language processing and data mining, including SIGIR (CCF A), WWW (CCF A), KDD (CCF A), ICML (CCF) CCF A), NIPS (CCF A), ACL (CCF A), WSDM (CCF B), CIKM (CCF B), ACM Transactions on Information Systems (TOIS, CCF A) and IEEE Transactions on Knowledge and Data Engineering (TKDE, CCF A). Especially in the field of expert finding, online learning, modal logic, and community-based answering. According to the latest Google academic statistics, his current paper cited the amount of 18205, h-index of 62, in all information retrieval scholars ranked third. Professor Maarten de Rijke has served as Chairman of the Conference or Program Committee for various meetings in the field of information retrieval, including SIGIR, WWW, WSDM and CIKM. He is currently the director of the Amsterdam Data Science Center and the director of the Ad de Jonge Intelligence and Safety Center in the Netherlands, as well as the director of the Master of Artificial Intelligence program at the University of Amsterdam. Professor Maarten de Rijke is also the editor-in-chief of several top journals in the field of information retrieval and information systems, including ACM Transactions on Information Systems (TOIS CCF A).

 

内容摘要:Interaction with information is a fundamental activity of the human condition. Interactions with search systems play an important role in the daily activities of many people, so as to inform their decisions and guide their actions. For many years, the field of IR has accepted ``the provision of relevant documents'' as the goal of its most fundamental algorithms. The focus of the field is shifting towards algorithms that are able to get the right information to the right people in the right way. Artificial intelligence (AI) is entering a new golden age. How can these advances help information retrieval? That is, how can AI help to develop agents that get the right information to the people in the right way? Making search results as useful as possible may be easy for some search tasks, but in many cases it depends on context, such as a user's background knowledge, age, or location, or their specific search goals. Addressing each optimal combination of search result preferences individually is not feasible. Instead, we need to look for scalable methods that can learn good search results without expensive tuning. In recent years, there has been significant work on developing methods for a range of IR problems that learn directly from natural interactions with their users. In the talk I will sample from these advances and hint at future directions.

 

 

沙龙主题:A Model for Real-time Concurrent Interaction Protocols in Component Interfaces

主讲人:Dr. Dang Van Hung

    间:2016420日晚上7:00

    点:西南大学计信院学术报告厅(25教一楼0114

主办单位:西南大学计算机与信息科学学院 软件学院

 

主讲人简介:Interaction Protocol specification is an important part for component interface specification. To use a component, the environment must conform to the interaction protocol specified in the interface of the component. We give a powerful technique to specify protocols which can capture the constraints on temporal order, concurrency, and timing. We also show that the problem of checking if Dang Van Hung graduated in Mathematics in 1977 at the Department of Mathematics, Hanoi University, Hanoi, Vietnam, and obtained PhD degree in Computer Science in 1988 at the Computer and Automation Research Institute, Hungarian Academy of Sciences, Budapest, Hungary. He began his career as a research fellow at the Institute of Information Technology, Hanoi, Vietnam. He was a research fellow at the United Nations University, International Institute for Software Technology located in Macao for more than 12 years. Since 2008, he is a senior lecturer of the University of Engineering and Technology of Vietnam National University in Hanoi.

He has been actively involved in many scientific activities such as organising international conferences, editting books and journals. His research interests include formal methods, real-time, parallel and distributed systems, component-based software development.

 

内容摘要:Interaction Protocol specification is an important part for component interface specification. To use a component, the environment must conform to the interaction protocol specified in the interface of the component. We give a powerful technique to specify protocols which can capture the constraints on temporal order, concurrency, and timing. We also show that the problem of checking if a timed automaton conforms to a given real-time protocol is decidable and develop a decision procedure for solving the problem.

 

 

沙龙主题:Optimizing Symbolic Execution for Software Testing

主讲人:Prof. Zijiang Yang

    间:2016421日晚上7:00

    点:西南大学计信院学术报告厅(25教一楼0114

主办单位:西南大学计算机与信息科学学院 软件学院

 

主讲人简介:Zijiang Yang is a professor of Computer Science at Western Michigan University. His research is in the broad areas of software engineering and formal methods. The primary focus is to develop formal method based tools to support the debugging, analysis and verification of complex systems. He has published over seventy papers, many of which were published in major software engineering conferences and journals such as FSE, ICSE, ASE, ICST, CAV and TSE. He is also an inventor of ten United States patents. Yang received his Ph.D. from the University of Pennsylvania. See https://www.cs.wmich.edu/~zijiang/ for more information on his research.

 

内容摘要:Symbolic execution is a powerful technique for systematically exploring the paths of a program and generating the corresponding test inputs. However, its practical usage is often limited by the path explosion problem, that is, the number of explored paths usually grows exponentially with the increase of program size. We propose new symbolic execution approaches to mitigate the path explosion problem by predicting and eliminating the redundant paths based on symbolic values in the context of software testing.

 

 

CCF FM Education Working Group Meeting

主持人:Prof. Zhiming Liu

    间:2016422日晚上7:00

    点:西南大学计信院学术报告厅(25教一楼0114

主办单位:西南大学计算机与信息科学学院 软件学院