相关论文: Towards Verification of Constituent Systems throug…

We apply a compositional formal modeling and verification method to an autonomous aircraft taxi system. We provide insights into the modeling approach and we identify several research areas where further development is needed. Specifically,…

This paper presents the verification of control systems implemented in Simulink. The goal is to ensure that high-level requirements on control performance, like stability, are satisfied by the Simulink diagram. A two stage process is…

Formal verification of complex algorithms is challenging. Verifying their implementations goes beyond the state of the art of current automatic verification tools and usually involves intricate mathematical theorems. Certifying algorithms…

The present dissertation introduces the research project on HOLMS (\textbf{HOL} Light Library for \textbf{M}odal \textbf{S}ystems), a growing modular framework for modal reasoning within the HOL Light proof assistant. To provide an…

On the one hand, ordered completion is a fundamental technique in equational theorem proving that is employed by automated tools. On the other hand, their complexity makes such tools inherently error prone. As a remedy to this situation we…

Composition technologies improve reuse in the development of large-scale complex systems. Safety critical systems require intensive validation and verification activities. These activities should be compositional in order to reduce the…

The need for formal definition of the very basis of mathematics arose in the last century. The scale and complexity of mathematics, along with discovered paradoxes, revealed the danger of accumulating errors across theories. Although,…

In previous work, summarized in this paper, we proposed an operation of parallel composition for rewriting-logic theories, allowing compositional specification of systems and reusability of components. The present paper focuses on…

Scalable and automatic formal verification for concurrent systems is always demanding. In this paper, we propose a verification framework to support automated compositional reasoning for concurrent programs with shared variables. Our…

We consider the problem of automated reasoning about dynamically manipulated data structures. The state-of-the-art methods are limited to the unfold-and-match (U+M) paradigm, where predicates are transformed via (un)folding operations…

Using Isabelle/HOL, we verify the state-of-the-art decision procedure for multi-level syllogistic with singleton (MLSS for short), which is a quantifier-free fragment of set theory. We formalise its syntax and semantics as well as a sound…

The formal analysis of automated systems is an important and growing industry. This activity routinely requires new verification frameworks to be developed to tackle new programming features, or new considerations (bugs of interest). Often,…

Cyber-physical systems (CPS), such as automotive systems, are starting to include sophisticated machine learning (ML) components. Their correctness, therefore, depends on properties of the inner ML modules. While learning algorithms aim to…

In this paper we study possibilities of using hierarchical reasoning, symbol elimination and model generation for the verification of parametric systems, where the parameters can be constants or functions. Our goal is to automatically…

Concurrent separation logic with fractional permissions (CSLPerm) provides a promising reasoning system to verify most complex sequential and concurrent fine-grained programs. The logic with strong and weak separating conjunctions offers a…

This set of theories presents a formalisation in Isabelle/HOL+Isar of data dependencies between components. The approach allows to analyse system structure oriented towards efficient checking of system: it aims at elaborating for a concrete…

We consider the problem of verification modulo tested library contracts as a step towards automating the verification of client programs that use complex libraries. We formulate this problem as the synthesis of modular contracts for the…

Model checking and automated theorem proving are two pillars of formal methods. This paper investigates model checking from an automated theorem proving perspective, aiming at combining the expressiveness of automated theorem proving and…

We present a prototype of an integrated reasoning environment for educational purposes. The presented tool is a fragment of a proof assistant and automated theorem prover. We describe the existing and planned functionality of the theorem…

We propose a local model-checking proof system for a fragment of CTL. The rules of the proof system are motivated by the well-known fixed-point characterisation of CTL based on unfolding of the temporal operators. To guarantee termination…