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

Automatic security protocol analysis is currently feasible only for small protocols. Since larger protocols quite often are composed of many small protocols, compositional analysis is an attractive, but non-trivial approach. We have…

Assurance arguments provide a clear and structured way to explain why stakeholders should trust that a system satisfies certain properties, yet widely used notations, e.g.Goal Structuring Notation (GSN), typically lack an operational…

Cyber-physical systems (CPS) such as autonomous cars, aircraft, and robots are often also safety-critical; thus it is imperative that they operate as intended with a high degree of certainty. Formal verification has been employed to verify…

We propose a method for compositional verification to address the state space explosion problem inherent to model-checking timed systems with a large number of components. The main challenge is to obtain pertinent global timing constraints…

Formal methods have been employed for requirements verification for a long time. However, it is difficult to automatically derive properties from natural language requirements. SpecVerify addresses this challenge by integrating large…

Simulation and formal verification are important complementary techniques necessary in high assurance model-based systems development. In order to support coherent results, it is necessary to provide unifying semantics and automation for…

Lighthouse projects such as CompCert, seL4, IronFleet, and DeepSpec have demonstrated that full verification of entire systems is feasible by establishing a refinement relation between an abstract system specification and an executable…

We consider the stability and the input-output analysis problems of a class of large-scale hybrid systems composed of continuous dynamics coupled with discrete dynamics defined over finite alphabets, e.g., deterministic finite state…

Recent advances in deep learning have enabled the development of autonomous systems that use deep neural networks for perception. Formal verification of these systems is challenging due to the size and complexity of the perception DNNs as…

The sumcheck protocol, introduced in 1992, is an interactive proof which is a key component of many probabilistic proof systems in computational complexity theory and cryptography, some of which have been deployed. However, none of these…

We study induction on the program structure as a proof method for bisimulation-based compiler correctness. We consider a first-order language with mutually recursive function definitions, system calls, and an environment semantics. The…

Description Logics (DLs) are a family of languages used for the representation and reasoning on the knowledge of an application domain, in a structured and formal manner. In order to achieve this objective, several provers, such as RACER…

In order to handle the complexity and heterogeneity of mod- ern instruction set architectures, analysis platforms share a common design, the adoption of hardware-independent intermediate representa- tions. The usage of these platforms to…

We present an environment, benchmark, and deep learning driven automated theorem prover for higher-order logic. Higher-order interactive theorem provers enable the formalization of arbitrary mathematical theories and thereby present an…

Large language models (LLMs) have shown increasing competence in solving mathematical reasoning problems. However, many open-source LLMs still struggle with errors in calculation and semantic understanding during intermediate reasoning…

Fully automated verification of large-scale software and hardware systems is arguably the holy grail of formal methods. Large language models (LLMs) have recently demonstrated their potential for enhancing the degree of automation in formal…

Cell injection is an approach used for the delivery of small sample substances into a biological cell and is widely used in drug development, gene injection, intracytoplasmic sperm injection (ICSI) and in-virto fertilization (IVF). Robotic…

Classes on compiler technology are commonly found in Computer Science curricula, covering aspects of parsing, semantic analysis, intermediate transformations and target code generation. This paper reports on introducing certified…

Recent advances in large language models (LLMs) have shown promise in formal theorem proving, yet evaluating semantic correctness remains challenging. Existing evaluations rely on indirect proxies such as lexical overlap with…

We present an automated verification of the well-known modal logic cube in Isabelle/HOL, in which we prove the inclusion relations between the cube's logics using automated reasoning tools. Prior work addresses this problem but without…