PSSV-2020 Invited speakers, talks and abstracts
-
Natasha Alechina (Intelligent Software Systems, Information and computing sciences department, Utrecht University, The Netherlands): State of the Art in Logics for Verification of Resource-Bounded Multi-Agent System
- Abstract: Approaches to the verification of multi-agent systems are typically based on games or transition systems defined in terms of states and actions. However such approaches often ignore a key aspect of multi-agent systems, namely that the agents' actions require (and sometimes produce) resources. I will survey previous work on the verification of multi-agent systems that takes resources into account.
-
Ekaterina Komendantskaya (School of Mathematical and Computer Sciences, Heriot-Watt University Edinburgh, UK): Refinement types for Verification of Neural Networks
- Abstract: Neural networks is an umbrella term for a range of machine learning algorithms that, given numeric data instances as an
input, construct a non-linear function or classifier that separates these data instances into classes. There are numerous applications of neural networks: in computer vision,
natural language processing, data mining, to name but a few. As neural networks move into domains where safety and security are important—e.g., autonomous
cars, conversational agents, governance—the problem of their verification comes to the forefront.
Neural network verification is a notoriously difficult problem. The very features that we value in neural networks (adaptivity and the ability
to generalise from noisy data) becomes a source of safety and security threats. For example, neural networks are known to be vulnerable to adversarial attacks (specially crafted inputs that can create an unexpected and possibly danger-ous output) and suffer from catastrophic forgetting.
Several approaches to neural network verification exist, two most prominent are the Reluplex system by Guy Katz et al, and abstract interpretation-inspired approaches
by the team of Martin Vechev. In both cases, the main emphasis of work is on algorithms employed in verifying neural network properties.
In this talk, I will raise a complementary question: given that we have several powerful algorithms on the market, what will be the right programming language infrastructure to
deploy these algorithms directly into implementation of systems based on neural networks? The solution I will be arguing for is to use refinement types to impose
verification conditions on neural networks. On the one hand, types will embed verification guarantees directly into the code that implements neural networks.
On the other hand, refinement type infrastructure will allow to annotate types of neural networks with refinements (e.g. robustness conditions), truth or falsity of which will be determined automatically by SMT solvers or any other similar tools.
In this talk, I will describe recent experiments conducted in F* (a functional language with refinement types)
on finding the right level of abstraction for expressing verification conditions for neural networks as refinement types.
This is a collaborative work with Wen Kokke and Daniel Kienitz.
-
Samvel K. Shoukourian (IT Educational and Research Center, Yerevan State University, Armenia): Polynomial algorithm for equivalence problem of deterministic multitape finite automata
- Abstract: An efficient algorithm for determining the equivalence of two deterministic multitape
finite automata is suggested. It is based on an already published proof of solvability for
this problem. It is shown that the suggested algorithm has polynomial complexity. The
asymptotic running time of the algorithm is bounded by k × s(n+1), where k is some constant,
n is the number of tapes and s is the sum of the number of states for the considered
automata.
This is a joint work with Hayk A. Grigoryan.
-
Ilya Sergey (Yale-NUS College and National University of Singapore): Deductive Synthesis of Heap-Manipulating Programs: Sound, Expressive, Fast
- Abstract: In my talk, I will describe a deductive approach for synthesising imperative programs with pointers from declarative specifications expressed in Separation Logic. The approach treats logical program specifications, given in the form or pre- and postconditions with a pure and a spatial part, as proof goals, and provides an algorithm for rule-directed program construction based on the shape of the symbolic heap footprint a desired program manipulates.
The program synthesis algorithm rests on the novel framework of Synthetic Separation Logic (SSL). The produced executable programs are correct by construction, in the sense that they satisfy the ascribed specifications, and are accompanied by complete proof derivations (i.e., certificates), which can be checked independently by a third-party verifier. The approach has been implemented as a proof search engine for SSL in a form a program synthesiser. For efficiency, the engine exploits properties of SSL specifications, aggressively relying on a version of the Frame Rule and commutativity of separating conjunction to prune the search space.
I will explain and showcase the use of SSL on characteristic examples, describe the design of out tool, and report on the experience of using it to synthesise a series of benchmark programs manipulating with heap-based linked data structures. I will also tell about some recent advances of using SSL-based synthesis, enhanced with immutability annotations, as well as its applications for program repair.
|
