The 21st International Conference on Formal Engineering Methods

ICFEM 2019

November 5th-9th, 2019, Shenzhen, China

Keynote Speakers

  • Yang Liu, Nanyang Technological University, Singapore (detail) (slide)
  • Luke Ong, University of Oxford (detail) (slide)
  • Zhendong Su, ETH Zurich (detail) (slide)
  • Naijun Zhan, Institute of Software, Chinese Academy of Sciences (detail)

    Yang Liu


Title: Secure Deep Learning Engineering: A Road Towards Quality Assurance of Intelligent Systems

Abstract: In company with massive data explosion and powerful computational hardware enhancement, deep learning (DL) has recently achieved substantial strides in cutting edge intelligent applications, ranging from virtual assistant (e.g., Alex, Siri), art design, autonomous vehicles, to medical diagnoses-tasks that until a few years ago could be done only by humans. DL has become the innovation driving force of many next generation’s technologies. We have been witnessing on the increasing trend of industry stakeholders’ continuous investment on DL based intelligent system, penetrating almost every application domain, revolutionizing industry manufacturing as well as reshaping our daily life.
However, current DL system development still lacks systematic engineering guidance, quality assurance standards, as well as mature toolchain support. The magic box, such as DL training procedure and logic encoding (as high dimensional weight matrices and complex neural network structures), further poses challenges to interpret and understand behaviors of derived DL systems. The latent software quality and security issues of current DL systems, already started emerging out as the major vendors, rush in pushing products with higher intelligence (e.g., Google/Uber car accident, Alexa and Siri could be manipulated with hidden command.
To bridge the pressing industry demand and future research directions, we perform a large-scale study on the most-recent curated 223 relevant works on deep learning engineering from a software quality assurance perspective. Based on this, we further conduct a consecutive set of ongoing work towards addressing the current challanges in quality, reliability, and security assurance of general-purpose intelligent systems. This talk not only provides a high-level vision of secure deep learning engineering (SDLE), from the quality assurance perspective, accompanied by a state-of-the-art literature curation, as well as the state-of-the-art solutions. We hope this work facilitates drawing the attention of the software&system engineering community on necessity and demands of quality assurance for SDLE, which altogether lays down the foundations and conquers technical barriers towards constructing robust and high-quality DL applications.

Bio: Dr. Yang Liu obtained his bachelor and ph.d degree in the National University of Singapore in 2005 and 2010, respectively. In 2012, he joined Nanyang Technological University as a Nanyang Assistant Professor. He is currently a full professor, director of the cybersecurity lab, Program Director of HP-NTU Corporate Lab and Deputy Director of the National Satellite of Excellence of Singapore. In 2019, he received the University Leadership Forum Chair professorship at NTU.
Dr. Liu specializes in software verification, security and software engineering. His research has bridged the gap between the theory and practical usage of formal methods and program analysis to evaluate the design and implementation of software for high assurance and security. By now, he has more than 270 publications in top tier conferences and journals. He has received a number of prestigious awards including MSRA Fellowship, TRF Fellowship, Nanyang Assistant Professor, Tan Chin Tuan Fellowship, Nanyang Research Award 2019 and 10 best paper awards and one most influence system award in top software engineering conferences like ASE, FSE and ICSE.

    Luke Ong


Title: Probabilistic Programming for Bayesian Machine Learning

Abstract: Probabilistic programming is a general-purpose means of expressing probabilistic models as computer programs, and automatically performing Bayesian inference such as posterior probability and marginalisation. By providing implementations of these generic inference algorithms, probabilistic programming systems enable data scientists to focus on what they can do best, i.e., utilising their domain knowledge to design good models; the task of constructing efficient inference engines can be left to researchers with expertise in statistical machine learning and programming languages. By promoting the separation between model construction and inference procedures, probabilistic programming can democratise access to Bayesian machine learning, with potentially huge benefits to AI and scientific modelling. Because of their generality, probabilistic programming poses interesting and challenging research problems for (both pragmatic and semantic aspects of) programming languages, and Bayesian statistics, and machine learning. In this talk I will introduce probabilistic programming for Bayesian machine learning as a general concept, and explain a number of research directions unique to probabilistic programming.

Bio: Luke Ong is Professor of Computer Science and Head of Programming Languages Research, Department of Computer Science, University of Oxford; and Fellow of Merton College. He works in programming languages, verification, semantics of computation, and logic and algorithms. Ong has made pioneering contributions to game semantics; he has played a leading role in the development of higher-order model checking. His current research interests include statistical probabilistic programming for Bayesian machine learning and differentiable programming; specification and synthesis of programs; analysis of concurrent and distributed systems; and verification of cryptographic and consensus protocols. Ong was a joint winner of the 2017 ACM/EATCS Alonzo Church Award for Outstanding Contributions to Logic and Computation. He is a former General Chair of ACM/IEEE Symposium on Logic in Computer Science (LICS), and Vice Chair of the ACM Special Interest Group in Logic and Computation (SIGLOG). He has served on the steering committee of EATCS, EACSL, and ETAPS; and the judging panel of the EACSL Ackermann Award, EATCS Distinguished Dissertation Award, ETAPS / EATCS Best Paper Award, and ETAPS Test-of-Time Award. Ong has served on the editorial boards of Logical Methods in Computer Science, Mathematical Structures in Computer Science, and Acta Informatica.

    Zhendong Su


Title: Specification-less Semantic Bug Detection

Abstract: The lack of specifications has been the most difficult practical and technical obstacle to software reliability. Without detailed application-specific properties, one cannot utilize formal verification and is confined to detecting generic bugs such as program crashes and memory safety violations, rather than deeper semantic bugs. Breaking this paradoxical impasse is very difficult, and impossible in general. This talk shows how to mitigate it via effective techniques for constructing tests with expected results, thus tackling both test and oracle generation. It illustrates this view with recent successful attacks on difficult testing and analysis problems from diverse domains, ranging from compilers, database engines, to deep learning systems. The talk discusses (1) the high-level principles and core techniques, (2) their significant practical successes --- hundreds and thousands of confirmed/fixed bugs in the most widely-used software, and (3) future opportunities and challenges.

Bio: Zhendong Su is a Professor in Computer Science at the Swiss Federal Institute of Technology in Zurich (ETH Zurich). Previously, he was a Professor in Computer Science and a Chancellor's Fellow at the University of California, Davis (UC Davis). He received his PhD in Computer Science from the University of California, Berkeley (UC Berkeley). His research spans programming languages and compilers, software engineering, computer security, deep learning and education technologies. His work was recognized by an ACM SIGSOFT Impact Paper Award, a Google Scholar Classic Paper (2017) Award, multiple best/distinguished paper awards at top venues (e.g., PLDI, OOPSLA, EAPLS, TACAS, ISSTA, and ICSE), an ACM CACM Research Highlight, an NSF CAREER Award, a UC Davis Outstanding Faculty Award, and multiple industrial faculty awards (e.g., Cisco, Google, Huawei, IBM, Microsoft, and Mozilla). He serves on the steering committees of ISSTA and ESEC/FSE, served as an Associate Editor for ACM TOSEM, co-chaired SAS 2009, program chaired ISSTA 2012, and program co-chaired SIGSOFT FSE 2016.

    Naijun Zhan


Title: Taming Delays in Cyber-Physical Systems

Abstract: With the rapid development of feedback control, sensor techniques and computer control, time delay has become an essential feature  of cyber-physical system (CPS), underlying both the continuous evolution of physical plants and the discrete transition of computer programs, which may well annihilate the stability/safety certificate and control performance of CPSs. In the safety-critical context, automatic verification and synthesis methods addressing time-delay in CPSs should therefore abound. However, surprisingly,  they do not, although time-delay has been extensively studied in the literature of mathematics and control theory from a qualitative perspective.  In this talk, we will report our recent efforts to tackle these issues, including controller synthesis for time-delayed systems in the setting of discrete time, bounded and unbounded verification of delay differential equations, and discuss remaining challenges and future trends. 

Bio: Dr. Naijun Zhan is a research professor at the State Key Lab. of Computer Science, Institute of Software, Chinese Academy of Sciences, Beijing, China. He received the Ph.D. degree in computer science from the Institute of Software, Chinese Academy of Sciences in 2000, and M.Sc. in computer science and B.Sc in mathematics both from Nanjing University respectively in 1996 and 1993. Prior to joining the Institute of Software, he was a Research Fellow with the Faculty of Mathematics and Information, University of Mannheim, Mannheim, Germany, from 2001 to 2004. He is a distinguished research professor of Chinese Academy of Sciences (since 2015) and the winner of Outstanding Youth Fund of Natural Science Foundation of China (2016).​
His research interests include formal techniques for the design of real-time and hybrid systems, program verification, modal and temporal logics, concurrent computation models, semantic foundations of component and object systems. Currently, he serves in the editorial boards of Formal Aspects of Computing, Journal of Logical and Algebraic Methods in Programming, Journal of Software, Journal of Computer Research and Development.