Related papers: ALICE: An Advanced Logic for Interactive Component…
We present a process for the development of safety and security critical components in transportation systems targeting a high-level certification (CENELEC 50126/50128, DO 178, CC ISO/IEC 15408). The process adheres to the objectives of an…
Modern search techniques either cannot efficiently incorporate human feedback to refine search results or to express structural or semantic properties of desired code. The key insight of our interactive code search technique ALICE is that…
We present a trustworthy connection between the Leon verification system and the Isabelle proof assistant. Leon is a system for verifying functional Scala programs. It uses a variety of automated theorem provers (ATPs) to check verification…
We present a semantic framework for the deductive verification of hybrid systems with Isabelle/HOL. It supports reasoning about the temporal evolutions of hybrid programs in the style of differential dynamic logic modelled by flows or…
ALICE is the dedicated heavy ion experiment at the LHC at CERN and records lead-lead collisions at a rate of up to 50 kHz. The detector with the highest data rate of up to 3.4 TB/s is the TPC. ALICE performs the full online TPC processing…
In open systems, i.e. systems operating in an environment that they cannot control and with components that may join or leave, behaviors can arise as side effects of intensive components interaction. Finding ways to understand and design…
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…
A principled approach to the design of program verification and con- struction tools is applied to separation logic. The control flow is modelled by power series with convolution as separating conjunction. A generic construction lifts…
In a blockchain system, nodes regularly distribute data to other nodes. The ideal perspective taken in the scientific literature is that data is broadcast to all nodes directly, while in practice data is distributed by repeated multicast.…
This paper explores verification of constituent systems within the context of the Symphony tool platform for Systems of Systems (SoS). Our SoS modelling language, CML, supports various contractual specification elements, such as state…
ALICE (A Large Ion Collider Experiment) is the CERN LHC experiment optimized for the study of the strongly interacting matter produced in heavy-ion collisions and devoted to the characterization of the Quark-Gluon Plasma. To achieve the…
The Isabelle/HOL proof assistant has a powerful library for continuous analysis, which provides the foundation for verification of hybrid systems. However, Isabelle lacks automated proof support for continuous artifacts, which means that…
Interactive theorem provers are complex systems that require sophisticated platform efforts - and hence systems programming environments - to manage effectively. The Isabelle platform exemplifies this with its Isabelle/Scala systems…
We extend a semantic verification framework for hybrid systems with the Isabelle/HOL proof assistant by an algebraic model for hybrid program stores, a shallow expression model for hybrid programs and their correctness specifications, and…
A calculus is presented for the stepwise refinement of abstract information flow architectures. We give a mathematical model for information flow components based on relations between input and output communication histories, and describe…
Blind quantum computing [A. Broadbent, J. Fitzsimons, and E. Kashefi, Proceedings of the 50th Annual IEEE Symposium on Foundations of Computer Science 517 (2009)] is a secure cloud quantum computing protocol which enables a client (who does…
Assurance cases are often required to certify critical systems. The use of formal methods in assurance can improve automation, increase confidence, and overcome errant reasoning. However, assurance cases can never be fully formalised, as…
This paper summarizes our experience in communicating the elements of reasoning about correctness, and the central role of formal specifications in reasoning about modular, component-based software using a language and an integrated Web IDE…
Formally verifying properties of software code has been a highly desirable task, especially with the emergence of LLM-generated code. In the same vein, they provide an interesting avenue for the exploration of formal verification and…
ALICE is the CERN LHC experiment optimised for the study of the strongly interacting matter produced in heavy-ion collisions and devoted to the characterisation of the quark-gluon plasma. To achieve the physics program for LHC Run 3, a…