10月31日:张苗苗:Bounded Model-checking of Discrete Duration Calculus
题 目:Bounded Model-checking of Discrete Duration Calculus
报告人:Prof. Zhang Miaomiao
主持人:刘静 教授
时 间:10月31日 13:30—15:00
地 点:中北校区数学馆201
报告摘要:
Fränzle and Hansen investigated the model-checking problem of the subset of Duration Calculus without individual variables and quantifications w.r.t. some approximation semantics by reduction to the decision problem of Presburger Arithmetic, thus obtained a model-checking algorithm with 4-fold exponential complexity [6, 7]. As an alternative, inspired by their work, we consider the bounded model-checking problem of the subset in the context of the standard discrete-time semantics in this paper. Based on our previous work , we reduce this problem to the reachability problem of timed automata. The complexity of our approach is singly exponential in the size of formulas and quadratic in the number of states of models. We implement our approach using UPPAAL and demonstrate its efficiency by some examples.
报告人简介:
张苗苗教授于2001年从上海交通大学自动化系取得博士学位,先后在荷兰内梅亨大学计算机科学系、联合国大学国际软件技术研究所进行软件理论研究工作,作为主要研究者参加了HAAST和AMETIST等欧盟科研项目。归国后,任教于同济大学软件学院,先后主持多项国家自然基金、教育部回国留学基金以及航天领域等项目。 目前从事嵌入式系统的建模和验证以及故障容错方面等的系统研究。
11月1日:田丰:云端融合的自然交互设备和工具
报告题目:云端融合的自然交互设备和工具
报告人:田丰 研究员
主持人:王长波
报告时间:2016年11月1日 16:00-17:00
报告地点:中北校区数学馆201
报告人简介:
田丰,中国科学院软件研究所研究员, 副总工程师,人机交互北京市重点实验室副主任,国家优秀青年基金获得者。现担任 ACM SIGCHI 中国分会主席、中国计算机学会人机交互专委会秘书长。担任 ACM TiiS、JVLC 等人机交互领域国际刊物编委。作为负责人承担国家重点研发计划等国家重点项目。在CHI, IJHCS, TPAMI, CSCW等国内外重要期刊会议上录用/发表学术论文近百余篇,合作出版专著1部,申请专利12 项(授权7项)。技术成果已覆盖到国内30 多个省市以及北美、欧洲、亚洲、非洲等多个国家, 并在协和、湘雅等大型三甲医院,国家跳水队、羽毛球队等多个国家队成功应用。作为第一完成人获得了2015 年度北京市科学技术一等奖。
报告摘要:
自然人机交互作为影响人类生活和推动经济发展的颠覆性信息技术具有重要的研究和应用价值,其中面临着交互场景复杂性,交互通道多样性,交互信息海量性等一些共性挑战。如何在医疗、教育等大范围、复杂场景中捕获多样化目标的自然行为和生理状态?如何融合用户的手势、体态、触控、语音、表情、眼动、生理等非精确交互信息并一致呈现?如何利用海量交互信息实现用户意图的准确理解?这些难题的破解都有赖于自然人机交互中共性关键技术的突破。本报告将从自然人机交互出发,所承担的国家重点研发计划“云端融合的自然交互设备和工具”中的相关工作和思路。
11月2日:Julian Dolby:Analysis of Android hybrid applications and other fun with WALA
讲座题目:Analysis of Android hybrid applications and other fun with WALA
主讲人: Julian Dolby (Research Staff Member, IBM Thomas J. Watson Research Center)
开始时间:2016年11月2日 13:30—15:00
报告地点:中北校区理科大楼B1002
Julian Dolby is a Research Staff Member at the IBM Thomas J. Watson Research Center, where he works on a range of topics, including static program analysis, software testing, concurrent programming models and the semantic Web. He is one of the primary authors of the publicly-available Watson Libraries for Analysis (WALA) program analysis infrastructure, and his recent WALA work has focused on creating the WALA Mobile infrastructure.
His program analysis work has recently focused on scripting languages like JavaScript and on security analysis of Web applications; this work has been included in IBM products, most notably Rational AppScan, Standard Edition and Source Edition. He was educated at the University of Illinois at Urbana-Champaign as a graduate student where he worked with Professor Andrew Chien on programming systems for massively-parallel machines.
报告摘要:
The bulk of my talk will focus on ASE 2016 work on analysis of hybrid apps (1), a blend of per-platform native code and portable JavaScript. Providing platform-specific functionality via native code and user interactions via JavaScript code, hybrid apps help developers build multiple apps for different platforms with less duplicated effort. However, most hybrid apps are developed in multiple programming languages with different semantics, complicating programming. Moreover, untrusted JavaScript code may access device-specific features via native code, exposing hybrid apps to attacks. Unfortunately, there are no existing tools to detect such vulnerabilities. In this paper, we present HybriDroid, the first static analysis framework for Android hybrid apps. First, we investigate the semantics of interoperation of Android Java and JavaScript. Then, we design and implement a static analysis framework that analyzes inter-communication between Android Java and JavaScript. We demonstrate HybriDroid with a bug detector that identifies programmer errors due to the hybrid semantics, and a taint analyzer that finds information leaks cross language boundaries. Our empirical evaluation shows that the tools are practically usable in that they found previously uncovered bugs in real-world Android hybrid apps and possible information leaks via a widely-used advertising platform.
I will also briefly discuss two other recent projects involving WALA: ASE 2015 work on a practically tunable static analysis framework for large-scale JavaScript applications (2), and ISSTA 2015 work on scalable and precise taint analysis for Android (3).
References:
1: Sungho Lee, Julian Dolby, Sukyoung Ryu: HybriDroid: static analysis framework for Android hybrid applications. ASE 2016: 250-261;
2: Yoonseok Ko, Hongki Lee, Julian Dolby, Sukyoung Ryu: Practically Tunable Static Analysis Framework for Large-Scale JavaScript Applications (T). ASE 2015: 541-551;
3: Wei Huang, Yao Dong, Ana Milanova, Julian Dolby: Scalable and precise taint analysis for Android. ISSTA 2015: 106-117。
11月2日:Yiyu Shi :Efficient Location Identification of Multiple Line Outages with Limited PMUs in Smart Grids
报告题目:Efficient Location Identification of Multiple Line Outages with Limited PMUs in Smart Grids
报告人:Yiyu Shi 教授
主持人:陈铭松 教授
报告地点:中北校区数学馆201
报告时间:11月2日13:30--14:30
报告摘要:
The efficient location identification of multiple line outages is critical to not only cascading failure elimination but also repair cost reduction. Most of existing methods, however, fail to handle location identification well. This failure typically occurs because the methods cannot overcome two challenges: the very limited number of phasor measurement units (PMUs) and the high computational complexity. This talk presents an efficient algorithm inspired by the ambiguity group theory to identify the locations of line outages with limited PMUs. Using 14-, 57-, 118-, 300-, and 2383-bus systems, our experimental study demonstrates that the proposed technique successfully identifies the most likely multiple line outages while attaining a 500 × speedup when compared to the method of exhaustive search.
报告人简介:
Dr. Yiyu Shi is currently an associate professor in the Department of Computer Science and Engineering and Electrical Engineering (concurrent appointment) at the University of Notre Dame . He received his B.S. degree (with honor) in Electronic Engineering from Tsinghua University, Beijing, China in 2005, the M.S and Ph.D. degree in Electrical Engineering from the University of California, Los Angeles in 2007 and 2009 respectively. He was an assistant professor in the Electrical and Computer Engineering Department at Missouri University of Science and Technology from 2010 to 2015, where he was the site founding co-director of the NSF I/UCRC Net-Centric Software and Systems Center. His current research interests include low-power design, three-dimensional integration, hardware security and renewable energy applications. In recognition of his research, eight of his papers have been nominated for the Best Paper Award and one paper have received the Best Paper in Track, all in top conferences (DAC'05, ICCAD'07, ICCD'08, ASPDAC'09, DAC'09, ISPD'13, ICCAD'14, ISPD'15, DAC'16). He was also the recipient of IBM Invention Achievement Award in 2009, Japan Society for the Promotion of Science (JSPS) Faculty Invitation Fellowship, Humboldt Research Fellowship, IEEE St. Louis Section Outstanding Educator Award, Academy of Science (St. Louis) Innovation Award, Missouri S&T Faculty Excellence Award, NSF CAREER Award, IEEE Region 5 Outstanding Individual Achievement Award, all in 2014, and the Air Force Summer Faculty Fellowship in 2015 and 2016. He has served on the technical program committee of many international conferences including DAC, ICCAD, DATE, ISPD, ASPDAC and ICCD. He is also a member of IEEE CEDA Publicity Committee and IEEE Smart Grid R&D Committee, and an associate editor of IEEE TCAD, ACM JETC, VLSI Integration, IEEE VLSI CAS Newsletter, IEEE TCCCPS Newsletter and ACM SIGDA Newsletter. He is a senior member of IEEE.
11月3日:Patrick S P Wang:New Biometrics and Forensics Using IPR Techniques in Fuzzy Learning Environment and Big Data
讲座题目:New Biometrics and Forensics Using IPR Techniques in Fuzzy Learning Environment and Big Data
主讲人:Patrick S P Wang教授 (美国东北大学)
主持人:吕岳
开始时间:2016-11-3 10:00am
讲座地址:中北校区理科大楼B1002
主办单位:计算机科学与以诚为本赢在信誉9001cc
报告摘要:
This talk deals with fundamental aspects of Similarity, Semantics, Ambiguity, Intelligent Pattern Recognition (IPR) and applications. It basically includes the following: Overview of 3D Biometric Technology and Applications, Importance of Security: A Scenario of Terrorists Attack, What are Biometric Technologies? Biometrics: Analysis vs Synthesis, Analysis: Concept of Syntax. Semantics, Ambiguity and Interactive Pattern Recognition, Importance of Measurement, How it works: FingerprintExtraction and Matching, Iris, and Facial Analysis, Authentication Applications, Thermal Imaging: Emotion Recognition. Synthesis in Biometrics, Modeling and Simulation, and more Examples and Applications of 3D Biomedical Imaging in Interactive Web/Video Networking Fuzzy Learning Environment. Finally, some future research directions are discussed.
报告人简介:
Prof. Patrick S.P. Wang, PhD. Fellow, IAPR, ISIBM, WASE and IEEE and ISIBM Outstanding Achievement Awardee, and is Tenured Full Professor, Northeastern University, USA, iCORE (Informatics Circle of Research Excellence) Visiting Professor, University of Calgary, Canada, OttoVonuericke Distinguished Guest Professor, Magdeburg University, Germany, Zijiang Visiting Chair, ECNU, Shanghai, China, as well as honorary advisory professor of several key universities in China, including Sichuan University, Xiamen University, East China Normal University, Shanghai, and Guangxi Normal University, Guilin. Prof. Wang received his BSEE from National Chiao Tung University (Jiaotong University), MSEE from National Taiwan University, MSICS from Georgia Institute of Technology, and PhD, Computer Science from Oregon State University. Dr. Wang has published over 26 books, 200 technical papers, 3 USA/European Patents, in PR/AI/TV/Cybernetics/Imaging, and is currently founding Editor-in-Chief of IJPRAI.