The 2nd International Workshop on Artificial Intelligence and Formal Methods (AI & FM 2020)

>>> Registration Entrance
Please note all participants (including workshop co-chairs) need to register.

>>> Previous edition AI & FM 2019

Location

AI & FM 2020 will be held at Institute of Intelligent Software, Guangzhou. To get more information, please refer Offline Participants Guide for details.

Total Program Overview

November 26th   Reception
November 27th   Workshop I: Dependable Deep Learning   + Friendly Basketball Competition (evening)
November 28th   Workshop II: Program Analysis and Verification
November 29th   Collaboration and Discussion Groups

Workshop I: Dependable Deep Learning (November 27th, 2020)

Background and Objectives
Artificial Intelligence (AI) has achieved significant progress in the past few years, and is being deployed broadly in many areas such as robotics, healthcare, self-driving, finance, etc. Formal method (FM) is a collection of techniques for the specification, development, and verification of systems in mathematically rigorous ways. FM has been successfully applied to provide assurance to the safety and correctness of critical systems, spanning from avionic systems, insulin pump, to microchips. Up to now, the development of learning-enabled AI systems is often referred as “magic” due to its lack of mathematical rigor. In a more general sense, both quantitative and qualitative tools are in great demand to understand the problems like robustness, security, ethics and privacy raised by AI systems, and to assess the benefits of deploying AI to the whole society. On the other hand, the FM methods often suffer from state-explosion problem and thus high-performance implementations of the methods are needed. This workshop aims to nurture a community with experts of both AI and FM, from both the academia and the industry, to discuss important questions such as how to develop novel FM methods to support the development, use and governance of AI, how to apply AI to improve the performance of FM methods, etc.

Co-Chairs

• Weipeng Cao, Shenzhen University
• Qiang Wang, Southern University of Science and Technology
• Cheng-Chao Huang, Chinese Academy of Sciences

Session 1
09:30 - 09:40   Opening
09:40 - 10:30   Jun Sun, Verification-based Neural Network Repair
10:30 - 11:00   Qiang Wang, A Hybrid Approach to Safe and Efficient Control of Autonomous Vehicles
11:00 - 11:30   Liqian Chen, Detecting Numerical Bugs in Programs Developed Using Machine Learning Frameworks
11:30 - 14:00   Lunch
Session 2
14:30 - 14:50   Pengfei Yang, Improving Neural Network Verification through Spurious Region Guided Refinement
14:50 - 15:10   Renjue Li, PRODeep: A Platform for Robustness Verification of Deep Neural Networks
15:10 - 15:30   Tea Break
15:30 - 16:00   Cao Weipeng, A Biologically Inspired Feature Enhancement Framework for Zero Shot Learning
16:00 - 16:50   Xiaowei Huang, Safety and Reliability of Deep Learning
16:50 - 17:15   Hanwei Zhang, Deep Learning in Adversarial Context
17:15 - 18:00   Collaboration and Discussion Groups
18:00 - 20:00   Banquet

Workshop II: Program Analysis and Verification (November 28th, 2020)

Background and Objectives
Formal analysis and verification methods including model checking, theorem proving, program verifying, etc., have been intensively studied and many software tools have been developed and shown to be useful through case studies. Furthermore, quantum computing is an emerging discipline. The last four years witnessed a great amount of progress in the design of both hardware and software. Since quantum mechanics is counter-intuitive to our classical world, the design of quantum algorithms is challenging and error-prone. Formal verification of quantum algorithms and systems is thus of great importance. This workshop mainly focuses on programming models, probabilistic and quantum systems, aim to discuss the frontier theories and technologies of formal analysis and verification methods.

Co-Chairs

• Yuxin Deng, East China Normal University
• Xiaomu Shi, Shenzhen University

Session 1
09:00 - 09:10   Opening
09:10 - 09:50   Fei He, Incremental Termination Analysis of Evolving Programs
09:50 - 10:30   Yuxin Deng, Verifying Quantum Communication Protocols with Ground Bisimulation
10:30 - 11:00   Tea Break
11:00 - 11:30   Shenggen Zheng, State Complexity Advantage of Quantum Finite Automata
11:30 - 12:00   Jianling Fu, An Algebraic Method to Fidelity-based Model Checking over Quantum Markov Chains
12:00 - 12:30   Lunch
Session 2
13:00 - 13:30   Ganzhao Yuan, A Block Coordinate Decomposition Algorithm for Nonconvex Sparse Optimization
13:30 - 14:00   Yong Li, Hybrid Compositional Reasoning for Reactive Synthesis from Finite-Horizon Specifications
14:00 - 14:30   Hanru Jiang, Towards Certified Separate Compilation for Concurrent Programs
14:30 - 17:00   Collaboration and Discussion Groups
17:00 - 18:00   Dinner

Collaboration and Discussion Groups (November 29th, 2020)

09:00 - 11:30   Collaboration and Discussion Groups
11:30 - 12:30   Lunch
13:00 - 16:00   Collaboration and Discussion Groups