Specification and Automated Verification for Some Concurrency Mechanisms (Chin Wei Ngan, National University of Singapore)
This talk outlines the reasoning of waitgroups-like mechanisms of concurrent programs, where the synchronization among threads is mainly achieved via the WaitGroup of Golang or CountDownLatch (CDL) protocol of Java. Both of these two mechanisms allow one or more threads to exchange resources and synchronize by waiting until some tasks being performed in other threads complete. We unify WaitGroup and CountDownLatch and propose specifications to support a unified synchronization mechanism. As a practical proof of concept, this new specification and automated verification mechanism for both WaitGroup and CountDownLatch, is implemented and evaluated under the HIP/SLEEK verification system. We utilize existing concepts of Concurrent Abstract Predicates that have been enhanced to support thread local abstractions, with updateable local states that are fictionally shared. This is joint work with Yin-Fang Chen (Department of Computer Science,National University of Singapore).
Next Generation Lagrangian Reachtubes (Radu Grosu, Vienna University of Technology , Austria )
We introduce LRT-NG, a set of techniques and an associated toolset that computes a reachtube (an over-approximation of the set of reachable states over a given time horizon) of a nonlinear dynamical system. LRT-NG significantly advances the state-of-the-art Langrangian Reachability and its associated tool LRT. From a theoretical perspective, LRT-NG is superior to LRT in three ways. First, it uses for the first time an analytically computed metric for the propagated ball which is proven to minimize the ball’s volume. We emphasize that the metric computation is the centerpiece of all bloating-based techniques. Secondly, it computes the next reachset as the intersection of two balls: one based on the Cartesian metric and the other on the new metric. While the two metrics were previously considered opposing approaches, their joint use considerably tightens the reachtubes. Thirdly, it avoids the “wrapping effect” associated with the validated integration of the center of the reachset, by optimally absorbing the interval approximation in the radius of the next ball. From a tool-development perspective, LRT-NG is superior to LRT in two ways. First, it is a standalone tool that no longer relies on CAPD. This required the implementation of the Lohner method and a Runge-Kutta time-propagation method. Secondly, it has an improved interface, allowing the input model and initial conditions to be provided as external input files. Our experiments on a comprehensive set of benchmarks, including two Neural ODEs, demonstrates LRT-NG’s superior performance compared to LRT, CAPD, and Flow*. This is joint work with S. Gruenbacher, J. Cyranka, M. Lechner, A. Islam, and S.A. Smolka.
Deductive Synthesis of Heap-Manipulating Programs: Sound, Expressive, Fast (Ilya Serghei, Yale-NUS College, Singapore )
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.
Financial Derivatives as Smart Contracts: challenges, adoption and trust (Andrei Arusoaie, Alexandru Ioan Cuza University of Iasi, Romania )
Financial derivatives are a special type of financial contracts that are mostly used to hedge risks or to speculate on the market fluctuations. The recent development of the blockchain technologies enables the automatic processing of financial derivatives. Financial derivatives can be encoded as programs (smart contracts) in the blockchain. In spite of all the guarantees offered by this technology, world’s top investors are skeptical. In 2019, the market value of OTC derivatives was estimated at $640.4 trillion. Only a small percentage was traded on the blockchain, and that was mostly due to trading cryptocurrency. So, large scale adoption of the blockchain for derivatives seems to be a difficult deal. In this talk we review several issues that need to be addressed in this area. The first issue is usability: people in finance find it hard to interact directly with smart contracts as they are now. Another big issue is trust, which can be tackled using state of the art formal methods and tools. A very convincing argument for using the blockchain is the cost and automation, as long as the expenses do not exceed the existing fees for processing derivatives. Finally, the main challenge is to benefit from the full power of the blockchain features in the financial derivatives market (e.g., tokenization, anonimity, decentralization, cross-border processing).
Non-linear interpolant synthesis and its application to program verification (Naijun Zhan, Institute of Software, Chinese Academy of Sciences, China)
The bottleneck of most of existing program verification techniques is the scalability. Compositional way has been thought as an effective solution to the problem. Interpolation-based techniques are inherently local and modular, which can be used to scale up these techniques, like BMC, CEGAR, theorem-proving, etc. Synthesizing Craig interpolants is the cornerstone of interpolation based techniques. In the literature, there has been numerous work on how to synthesize interpolants of different decidable fragments of first-order logic, linear arithmetic, array logic, multi-sets, etc. and their combinations, but little work related to non-linear arithmetic. In this talk, I will report our recent solutions to this issue by using real algebraic geometry and semi-definite programming, and by machine learning. In addition, I will also show how to apply the result to program verification such as invariant generation and so on.
Modelling for Software Defined Human-Cyber-Physical Systems (Zhiming Liu, Southwest University, China)
We recall the evolution of from Cyber-Physical-Systems (CPS) to Human-Cyber-Physical Systems (HCPS) in past two decades. We shall clarify some concepts and discuss some challenges from system engineering perspectives in this new and pervasive form of ICT systems. We propose a research agenda arena for model-based software defined technology of HCPS. We discuss about the need of new abstractions for system software design and the importance of architecture modelling. Based on the system architecture perspective, we argue for the controllable, composable and reusable (i.e. trustworthy) AI systems to advance the system engineering of HCPS. Acknowledgment: The work is supported in part by Capacity Building Grant of Southwest University (SWU116007) and China National Nature Foundation (NNSF) projects (61802318, 61732019, 61672435, 61811530327).
Decidability Problems in Logic-based Knowledge Representation (Sebastian Rudolph, TU Dresden, Germany)
The availability of large repositories of knowledge in structured, machine-processable form – like knowledge graphs or linked open data – poses new challenges regarding the intelligent handling of these resources via complex query answering, information integration, and diverse further knowledge management tasks. To this end, contemporary knowledge representation languages such as the Web Ontology Language (OWL) or rule-based formalisms play an important role in theory and practice; they enable a unified view on heterogeneous data sources and a better exploitation of information that is incomplete or given only implicitly. Yet, in particular for very expressive formalisms, the question of the algorithmically possible arises. In my talk, I introduce the topic of decidability problems in knowledge representation and exemplify the typical approach by presenting a central non-trivial decidability result for conjunctive query answering over OWL ontologies.
Towards Safety in Learning-enabled Systems: Verification and Design (Chao Huang, Northwestern University, US )
Learning-enabled systems have been receiving numerous attractions from both academia and industry due to promising applications. They often leverage machine learning techniques in their perception of the environment, and increasingly also in the consequent decision making process for planning, navigation, control, etc. With no doubt, safety is one of the key issues before such systems are applied in practice. In this talk, I will introduce the state-of-the-arts, as well as our recent works, on safety verification and design of learning-enabled systems with respect to perception, adaptation and control. This talk aims to bring the audiences in the formal method community an overview of the current works on this important topic, and provide some insights on machine learning from the perspective of formal methods.
Local Reasoning about Parametric and Reconfigurable Component-based systems (Marius Bogza, VERIMAG, CNRS, France)
We introduce a logical framework for the specification and verification of component-based systems, in which finitely many component instances are active, but the bound on their number is not known. Besides specifying and verifying parametric systems, we consider the aspect of dynamic reconfiguration, in which components and connectors can be created and removed at runtime. We describe such parametric and reconfigurable architectures using resource logics, close in spirit to Separation Logic, used to reason about dynamic pointer structures. These logics support the principle of local reasoning, which is the key for writing modular specifications and building scalable verification algorithms.
Dependable View Update Strategies on Relations (Zhenjiang Hu, Peking University, China)
“View update” is an important mechanism that allows updates on a view by translating them to the corresponding updates on the base relations. Existing literature has shown the ambiguity of the view update translation and the lack of dependability. To address this problem, we propose a robust language-based approach for making view update strategies programmable and valid so that the corresponding view definition is automatically derived without ambiguity. Particularly, we design a fragment of Datalog language for specifying update strategies and a validation algorithm for these strategies. We have implemented our proposed approach together with a debugging system to support development of correct view strategies. The experimental results show our system is feasible and efficient.
Towards Verified Stochastic Variational Inference for Probabilistic Programs (Hongseok Yang, KAIST, South Korea)
Probabilistic programming is the idea of writing models from statistics and machine learning using program notations and reasoning about these models using generic inference engines. Recently its combination with deep learning has been explored intensely, which led to the development of so called deep probabilistic programming languages, such as Pyro, Edward and ProbTorch. At the core of this development lie inference engines based on stochastic variational inference algorithms. When asked to find information about the posterior distribution of a model written in such a language, these algorithms convert this posterior-inference query into an optimisation problem and solve it approximately by a form of gradient ascent or descent. In this paper, we analyse one of the most fundamental and versatile variational inference algorithms, called score estimator or REINFORCE, using tools from denotational semantics and program analysis. We formally express what this algorithm does on models denoted by programs, and expose implicit assumptions made by the algorithm on the models. The violation of these assumptions may lead to an undefined optimisation objective or the loss of convergence guarantee of the optimisation process. We then describe rules for proving these assumptions, which can be automated by static program analyses. Some of our rules use nontrivial facts from continuous mathematics, and let us replace requirements about integrals in the assumptions, such as integrability of functions defined in terms of programs’ denotations, by conditions involving differentiation or boundedness, which are much easier to prove automatically (and manually). Following our general methodology, we have developed a static program analysis for the Pyro programming language that aims at discharging the assumption about what we call model-guide support match. Our analysis is applied to the eight representative model-guide pairs from the Pyro webpage, which include sophisticated neural network models such as AIR. It finds a bug in two of these cases, and shows that the assumptions are met in the others. This is joint work with Wonyeol Lee and Hangyeol Yu (KAIST, South Korea) and Xavier Rival (INRIA Paris/CNRS/ENS/PSL Research University, France).
Towards Verifying Neural Network Fairness (Sun Jun, Singapore Management University, Singapore)
In this work, I will present our recent work on analysing neural networks in terms of fairness, i.e., solving the problem of checking whether a neural network inherits discrimination from real-world discriminative data. We start with a testing approach (i.e., falsification) and subsequently work towards an approach for fairness verification. We show that discrimination often exists in neural network models and humbly seek your contribution to jointly address the problem.
Security of Internet-of-Things Systems: A Perspective of Integration (Guangdong Bai, University of Queensland, Australia)
Internet of Things (IoT) is rapidly evolving and applied extensively in various areas such as smart home, smart healthcare, and smart city. A key feature of IoT systems is the integration of a wide assortment of technologies, including multiple standards, customized or proprietary communication protocols, and heterogeneous platforms. During the integration, critical security vulnerabilities are likely to be introduced, due to customization, unsatisfied assumptions, incompatibility, and conflicts in security policies. Hence, our work aims to address the security problems in IoT systems from an integration perspective, as a complement to numerous studies that focus on the analysis of individual techniques. In this presentation, we will introduce and discuss our ongoing work.
Secure Deep Learning Engineering: A Road Towards Quality Assurance of Intelligent Systems (abstract)
Yang Liu, Nanyang Technological University, Singapore
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 and 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.
Scalable Analysis and Control of Boolean Networks (Jun Pang, University of Luxembourg, Luxembourg)
Computational modelling plays a prominent role in providing a system-level understanding of processes that take place in a living cell. However, it faces significant challenges when modelling realistic biological systems due to the size of the state-space that needs to be considered. Hence, profound understanding of biological processes asks for the development of new methods that would provide means for formal analysis and reasoning about large systems. In this talk, I will present (1) a scalable method for attractor detection in Boolean networks (BNs), which is the first efficient approach that can deal with large asynchronous BNs with hundreds of nodes; and (2) several efficient reprogramming methods to derive optimal control strategies for driving large BNs from a source attractor to a target attractor, which can have important applications in the study of systemic diseases.
Modeling and Verification of Concurrent and Distributed Systems in Mediator (Meng Sun, Peking University, China)
In this talk I will introduce the Mediator modeling language and show how to formalize component-based concurrent and distributed system models in Mediator. Mediator supports a two-step hierarchical modeling approach: Automata, which provide an interface of ports, are the basic behavior units; Systems declare components or connectors through automata, and glue them together. With the help of Mediator, components and systems can be modeled separately and precisely. The distributed Mediator and its semantics can be used to capture the inherent real-time and asynchronous behavior in distributed systems. Properties of Mediator models can be specified through CTL* formulae that support various families of properties such as safety and liveness, which can be verified using the nuXmv model checker.
Cyclic Satisfiability Proofs in Separation Logic (Quang Loc Le, University College London, UK)
Separation logic is a well-established assertion language designed for reasoning about heap-manipulating programs. Combined with inductive predicates, separation logic has been shown to capture semantics of loops and recursive procedures naturally and succinctly. The main challenge of the reasoning over this fragment of separation logic is that it often requires reasoning about infinite heaps as well as infinite integer domain. In this talk, we introduce inductive reasoning for the satisfiability problem in separation logic. We present a cyclic proof system in which inductive inference relies on circular reasoning and the soundness is guaranteed by Fermat’s method of infinite descent. Beside some basic concepts and foundations, the talk also discusses experimental evaluation on satisfiability problems over complex data structures.
Software validation: Challenges and opportunities raised by the AI effervescence (Ileana Ober, Université Paul Sabatier, Toulouse, France)
During the last years we witnessed an impressive rate of progress in the field of artificial intelligence, both on theoretical results and, mostly, on using these results in various application fields. While few connections exist traditionally between the research field of software validation and artificial intelligence, some interesting research results emerge. In this talk we will discuss on the impact of the new trends in artificial intelligence on the field of software validation.
TBA (Grigore Rosu, University of Illinois at Urbana-Champaign, US )
available soon