Algebraic effects and handlers are a powerful abstraction to build non-local control-flow mechanisms such as resumable exceptions, lightweight threads, co-routines, generators, and asynchronous I/O. All of such features have very evolved semantics, hence they pose very interesting challenges to deductive verification techniques. In fact, there are very few proposed techniques to deductively verify programs featuring these constructs, even fewer when it comes to automated proofs. In this paper, we present an extension to Cameleer, a deductive verification tool for OCaml code, that allows one to reason about algebraic effects and handlers. Our proposal embeds the behavior of effects and handlers using exceptions and employs defunctionalization to deal with continuations exposed by effect handlers.
We present symQV, a symbolic execution framework for writing and verifying quantum computations in the quantum circuit model. symQV can automatically verify that a quantum program complies with a first-order specification. We formally introduce a symbolic quantum program model. This allows to encode the verification problem in an SMT formula, which can then be checked with a delta-complete decision procedure. We also propose an abstraction technique to speed up the verification process. Experimental results show that the abstraction improves symQV's scalability by an order of magnitude to quan…
Reactive programs combine traditional sequential programming constructs with primitives to allow communication with other concurrent agents. They are ubiquitous in modern applications, ranging from components systems and web services, to cyber-physical systems and autonomous robots. In this paper, we present an algebraic verification strategy for concurrent reactive programs, with a large or infinite state space. We define novel operators to characterise interactions and state updates, and an associated equational theory. With this we can calculate a reactive program's denotational semantics, …
The growing complexity and diversity of models used in the engineering of dependable systems implies that a variety of formal methods, across differing abstractions, paradigms, and presentations, must be integrated. Such an integration relies on unified semantic foundations for the various notations, and co-ordination of a variety of automated verification tools. The contribution of this paper is Isabelle/UTP, an implementation of Hoare and He's Unifying Theories of Programming, a framework for unification of formal semantics. Isabelle/UTP permits the mechanisation of computational theories fo…
Formal Verification of Safety Architectures for Automated Driving
National Institute of Informatics（国立信息学研究所）；National Institute of Advanced Industrial Science and Technology (AIST)（国立先进工业科学技术研究院（AIST））；Japanese-French Laboratory for Informatics（日法信息学实验室）；The Graduate University for Advanced Studies (SOKENDAI)（综合研究大学院大学（SOKENDAI））
In this report, we present the preliminary work developed for our research project for the APDC (Área Prática de Desenvolvimento Curricular) course. The main goal of this project is to develop a framework, on top of the Why3 tool, for the verification of effectful higher-order programs. We use defunctionalization as an intermediate transformation from higher-order OCaml implementations into first order ones. The target for our translation is WhyML, the Why3's programming language. We believe defunctionalization can be an interesting route for the automated verification of higher-order programs…
Stochastic hybrid systems have received significant attentions as a relevant modelling framework describing many systems, from engineering to the life sciences: they enable the study of numerous applications, including transportation networks, biological systems and chemical reaction networks, smart energy and power grids, and beyond. Automated verification and policy synthesis for stochastic hybrid systems can be inherently challenging: this is due to the heterogeneity of their dynamics (presence of continuous and discrete components), the presence of uncertainty, and in some applications the…
Automated Experiment Design for Data-Efficient Verification of Parametric Markov Decision Processes
Department of Computer Science, University of Oxford（牛津大学计算机科学系）；Department of Electrical Engineering, Eindhoven University of Technology（埃因霍温理工大学电气工程系）
In this paper, we propose a tool, called DataProVe, for specifying high-level data protection policies and system architectures, as well as verifying the conformance between them in a fully automated way. The syntax of the policies and the architectures is based on semi-formal languages, and the automated verification engine relies on logic and resolution based proofs. The functionality and operation of the tool are presented using different examples.
Monash University（莫纳什大学）；University of Kaiserslautern（凯泽斯劳滕大学）；Sapienza University of Rome（罗马大学）；University of Oxford（牛津大学）
In the context of multi-agent systems, the rational verification problem is concerned with checking which temporal logic properties will hold in a system when its constituent agents are assumed to behave rationally and strategically in pursuit of individual objectives. Typically, those objectives are expressed as temporal logic formulae which the relevant agent desires to see satisfied. Unfortunately, rational verification is computationally complex, and requires specialised techniques in order to obtain practically useable implementations. In this paper, we present such a technique. This tech…
