Invited Talks

Keynote Talks:

• Speaker: Santiago Escobar, Universitat Politècnica de València, Spain.
• Title: Equational Unification and Narrowing in Maude
• Abstract Maude is a language and a system based on rewriting logic. It is a mathematical modeling language thanks to its logical basis and its initial model semantics. Maude can be used in three, mutually reinforcing ways: as a declarative programming language, as an executable formal specification language, and as a formal verification system. Logical reasoning capabilities have been added to Maude during the last years and, in this invited talk, we give an overview of the different unification and narrowing techniques available in Maude, focusing on some of the programming, modeling, and verification aspects of Maude.

• Speaker: Xiaowei Huang, University of Liverpool, United Kingdom.
• Title: Bridging Formal Methods and Machine Learning with Global Optimisation
• Abstract Formal methods and machine learning are two research fields with drastically different foundations and philosophies. Formal methods utilise mathematically rigorous techniques for the specification, development and verification of software and hardware systems. Machine learning focuses on pragmatic approaches to gradually improve a parameterised model by observing a training data set. While historically the two fields lack communication, this trend has been changed in the past few years with an outburst of research interest in the robustness verification of neural networks. This paper will briefly review these works, and focus on urgent need for broader, and more in-depth, communication between the two fields, with the ultimate goal of developing learning-enabled systems with not only excellent performance but also acceptable safety and security. We present a specification language, MLS², and show that it can express a set of known safety and security properties including generalisation, uncertainty, robustness, data poisoning, backdoor, model stealing, membership inference, model inversion, interpretability, and fairness. For the verification of MLS² properties, we promote the global optimisation based methods, which have provable guarantees on the convergence to the optimal solution. Many of them have theoretical bounds on the gap between current solutions and the optimal solution.

• Speaker: Yuan Feng, University of Technology Sydney, Australia.
• Title: Model checking quantum Markov chains
• Abstract Quantum software will play an important role in harnessing the superpower of quantum computing. However, it is extremely difficult to guarantee its correctness. Model checking has been shown to be effective in the verification of classical programs, but a fundamental difficulty arises when it is applied to quantum systems: the state space of a quantum system is always a continuum even if its dimension is finite. To overcome this difficulty, we introduce a novel concept of quantum Markov chains, in which quantum effects are encoded as super-operators labelling transitions, keeping the location information (nodes) classical. We define a quantum extension of Probabilistic Computation Tree Logic called QCTL for the new model and develop algorithms to verify properties expressed in this logic. It is worth noting that in this framework, model checking is performed symbolically at the super-operator level, without resorting to the underlying quantum states, thus avoiding the difficulties brought about by the continuity of the (quantum) state space. To verify omega-regular (e.g. Linear Temporal Logic) properties, we transform the product of the quantum Markov chain and the property automaton into a single super-operator and show that the BSCC subspace decomposition of the associated state space provides a solution to the model checking problem.