Related papers: An Automatically Verified Prototype of the Android…
CoqQ is a framework for reasoning about quantum programs in the Coq proof assistant. Its main components are: a deeply embedded quantum programming language, in which classic quantum algorithms are easily expressed, and an expressive…
We present Leapfrog, a Coq-based framework for verifying equivalence of network protocol parsers. Our approach is based on an automata model of P4 parsers, and an algorithm for symbolically computing a compact representation of a…
We report on the development of an optimized and verified decision procedure for orthologic equalities and inequalities. This decision procedure is quadratic-time and is used as a sound, efficient and predictable approximation to classical…
Ensuring correctness is crucial for code generation. Formal verification offers a definitive assurance of correctness, but demands substantial human effort in proof construction and hence raises a pressing need for automation. The primary…
Current approaches for formal verification of algorithms face important limitations. For specification, they cannot express algorithms naturally and concisely, especially for algorithms with states and flexible control flow. For…
Formal verification using proof assistants, such as Coq, enables the creation of high-quality software. However, the verification process requires significant expertise and manual effort to write proofs. Recent work has explored automating…
Matching logic is a formalism for specifying, and reasoning about, mathematical structures, using patterns and pattern matching. Growing in popularity, it has been used to define many logical systems such as separation logic with recursive…
Most existing implementations of multiple precision arithmetic demand that the user sets the precision {\em a priori}. Some libraries are said adaptable in the sense that they dynamically change the precision of each intermediate operation…
Previous works on formally studying mobile robotic swarms consider necessary and sufficient system hypotheses enabling to solve theoretical benchmark problems (geometric pattern formation, gathering, scattering, etc.). We argue that formal…
Large language models (LLMs) can potentially help with verification using proof assistants by automating proofs. However, it is unclear how effective LLMs are in this task. In this paper, we perform a case study based on two mature Rocq…
Formal verification using proof assistants, such as Coq, is an effective way of improving software quality, but requires significant effort and expertise. Machine learning can automatically synthesize proofs, but such tools are able to…
We introduce a novel type system for enforcing secure information flow in an imperative language. Our work is motivated by the problem of statically checking potential information leakage in Android applications. To this end, we design a…
Quantum error correction (QEC) is fundamental for suppressing noise in quantum hardware and enabling fault-tolerant quantum computation. In this paper, we propose an efficient verification framework for QEC programs. We define an assertion…
Formal verification provides mathematical guarantees that a software is correct. Design-level verification tools ensure software specifications are correct, but they do not expose defects in actual implementations. For this purpose,…
Android is a widely used operating system that employs a permission-based access control model. The Android Permissions System (APS) is responsible for mediating application resource requests. APS is a critical component of the Android…
This document shows how Z specifications can be translated into $\{log\}$ and, later, on how $\{log\}$ can be used to run simulations and automated proofs. This can help users of other specification languages such as B and VDM to use…
Agentic systems have recently emerged as state-of-the-art approaches for automated theorem proving in formal mathematics. To assess how far these capabilities extend to program verification, we evaluate Claude Code in an agentic proving…
Formal verification can provably guarantee the correctness of critical system software, but the high proof burden has long hindered its wide adoption. Recently, Large Language Models (LLMs) have shown success in code analysis and synthesis.…
Proof-oriented programming languages (POPLs) empower developers to write code alongside formal correctness proofs, providing formal guarantees that the code adheres to specified requirements. Despite their powerful capabilities, POPLs…
In this report we describe a tool framework for certifying properties of PLCs: CERTPLC. CERTPLC can handle PLC descriptions provided in the Sequential Function Chart (SFC) language of the IEC 61131-3 standard. It provides routines to…