arXiv subjects

Ivan Perez

Publications and source records attributed to Ivan Perez.

5 recordsLinked to original sources

arXiv2026

Trustworthy Runtime Verification via Bisimulation (Extended Experience Report)

When runtime verification is used to monitor safety-critical systems, it is essential that monitoring code behaves correctly. The Copilot runtime verification framework pursues this goal by automatically generating C monitor programs from a high-level DSL embedded in Haskell. In safety-critical domains, every piece of deployed code must be accompanied by an assurance argument that is convincing to human auditors. However, it is difficult for auditors to determine with confidence that a compiled monitor cannot crash and implements the behavior required by the Copilot semantics. In this paper we describe CopilotVerifier, which runs alongside the Copilot compiler, generating a proof of correctness for the compiled output. The proof establishes that a given Copilot monitor and its compiled form produce equivalent outputs on equivalent inputs, and that they either crash in identical circumstances or cannot crash. The proof takes the form of a bisimulation broken down into a set of verification conditions. We leverage two pieces of SMT-backed technology: the Crucible symbolic execution library for LLVM and the What4 solver interface library. Our results demonstrate that dramatically increased compiler assurance can be achieved at moderate cost by building on existing tools. This paves the way to our ultimate goal of generating formal assurance arguments that are convincing to human auditors.

cs.PL↗

arXiv2026

Logic Programming with Extensible Types

Logic programming languages present clear advantages in terms of declarativeness and conciseness. However, the ideas of logic programming have been met with resistance in other programming communities, and have not generally been adopted by other paradigms and languages. This paper proposes a novel way to incorporate logic programming in an existing codebase in a typed functional programming language. Our approach integrates with the host language without sacrificing static typing, and leverages strengths of typed functional programming such as polymorphism and higher-order. We do so by combining three ideas. First, we use the extensible types technique to allow values of the host language to contain logic variables. Second, we implement a unification algorithm that works for any data structure that supports certain operations.Third, we introduce a domain-specific language to define and query predicates. We demonstrate our proposal via a series of examples, and provide aids to make the notation convenient for users, showing that the proposed approach is not just technically possible but also practical. Our ideas have been implemented in the language Haskell with very good results.

cs.PL↗

arXiv2024

Single NV in nanodiamond for quantum sensing of protein dynamics in an ABEL trap

Enzymes are cellular protein machines using a variety of conformational changes to power fast biochemical catalysis. Our goal is to exploit the single-spin properties of the luminescent NV (nitrogen-vacancy) center in nanodiamonds to reveal the dynamics of an active enzyme complex at physiological conditions with the highest spatio-temporal resolution. Specifically attached to the membrane enzyme FoF1-ATP synthase, the NV sensor will report the adenosine triphosphate (ATP)-driven full rotation of Fo motor subunits in ten consecutive 36{\deg} steps. Conformational dynamics are monitored using either a double electron-electron resonance scheme or NV- magnetometry with optical readout or using NV- relaxometry with a superparamagnetic nanoparticle as the second marker attached to the same enzyme. First, we show how all photophysical parameters like individual size, charge, brightness, spectral range of fluorescence and fluorescence lifetime can be determined for the NV- center in a single nanodiamond held in aqueous solution by a confocal anti-Brownian electrokinetic trap (ABEL trap). Stable photon count rates of individual nanodiamonds and the absence of blinking allow for observation times of single nanodiamonds in solution exceeding hundreds of seconds. For the proposed quantum sensing of nanometer-sized distance changes within an active enzyme, we show that local magnetic field fluctuations can be detected all-optically by analyzing fluorescence lifetime changes of the NV- center in each nanodiamond in solution.

q-bio.QM↗

arXiv2022

Monitoring ROS2: from Requirements to Autonomous Robots

Runtime verification (RV) has the potential to enable the safe operation of safety-critical systems that are too complex to formally verify, such as Robot Operating System 2 (ROS2) applications. Writing correct monitors can itself be complex, and errors in the monitoring subsystem threaten the mission as a whole. This paper provides an overview of a formal approach to generating runtime monitors for autonomous robots from requirements written in a structured natural language. Our approach integrates the Formal Requirement Elicitation Tool (FRET) with Copilot, a runtime verification framework, through the Ogma integration tool. FRET is used to specify requirements with unambiguous semantics, which are then automatically translated into temporal logic formulae. Ogma generates monitor specifications from the FRET output, which are compiled into hard-real time C99. To facilitate integration of the monitors in ROS2, we have extended Ogma to generate ROS2 packages defining monitoring nodes, which run the monitors when new data becomes available, and publish the results of any violations. The goal of our approach is to treat the generated ROS2 packages as black boxes and integrate them into larger ROS2 systems with minimal effort.

cs.RO↗

arXiv2020

From Requirements to Autonomous Flight: An Overview of the Monitoring ICAROUS Project

The Independent Configurable Architecture for Reliable Operations of Unmanned Systems (ICAROUS) is a software architecture incorporating a set of algorithms to enable autonomous operations of unmanned aircraft applications. This paper provides an overview of Monitoring ICAROUS, a project whose objective is to provide a formal approach to generating runtime monitors for autonomous systems from requirements written in a structured natural language. This approach integrates FRET, a formal requirement elicitation and authoring tool, and Copilot, a runtime verification framework. FRET is used to specify formal requirements in structured natural language. These requirements are translated into temporal logic formulae. Copilot is then used to generate executable runtime monitors from these temporal logic specifications. The generated monitors are directly integrated into ICAROUS to perform runtime verification during flight.

cs.SE↗