program verification engineers

Abstract: Program specifications in separation logic describe ownership of resources and serve as logical interfaces for local reasoning. Compiler correctness, expressed as semantics preservation, does not by itself supply such an interface for compiled code, because it does not explicitly relate source and target resources and assertions. We investigate WP-preserving compilation: when a compiler translates a source program, the weakest preconditions that the program satisfies in a separation logic carry over to the compiled program. Our proof technique consists of a resource-aware simulation over interaction trees: it relates the resources required by corresponding source and target events, and tracks ownership through target operations, such as register accesses, that have no source counterpart. We apply the approach to a compiler from a structured imperative language to an assembly-like language, first for closed programs and then extended with modules and function calls. In the extended setting, each module can be verified in the source logic and compiled separately; its specifications carry over to the compiled module and are preserved when compiled modules are linked. All results are mechanized in Rocq.

Abstract: We investigate the parameterized reachability problem for concurrent register machines over infinite data domains. In this framework, each machine is a program equipped with a set of local registers, the communication across machines is mediated through a set of shared registers. Both local and shared registers can take values from an infinite data domain. The program's primitive operations include copying values between registers, assigning constants, comparing registers for (dis-)equality, and nondeterministic assignments that store an arbitrary domain value into a local register. The parameterized reachability problem considers a program and a target location, asking whether there exists some n in Naturals such that an execution of n identical machines (referred to as instances) results in at least one instance reaching the specified location. We show that this problem is Pspace-complete in the general case and it becomes undecidable if a freshness assumption (i.e., each assignment must produce a unique value distinct from all constants) is applied to nondeterministic assignments. This undecidability persists even for systems restricted to two shared and two local registers. Finally, we establish optimal decidability results for two restricted settings: when each thread is limited to a single local register, or when the system utilizes only one shared register.

Abstract: The existence of polyhedral inductive invariants suitable for proving that a given control location is unreachable is undecidable for programs using only linear arithmetic over Z or Q, by reduction from 2-counter machines.

Abstract: We extend Fine's selection method to the setting of intuitionistic modal logic and use it to provide a model-theoretic proof that Fischer Servi-style intuitionistic $\sf K4$ has the finite model property.

Abstract: The undecidability of a program's static semantic properties is governed by Rice's theorem. Self-modifying systems, however, require analysing not whether a property holds now, but whether it is preserved when the system rewrites itself. We formalise this transition through a semantic elevation operator ΛΦ, which turns the static question "does x satisfy P?" into the dynamic question "is P preserved after x is transformed by Φ?". We prove that when Φ is intensional (depending on the source code, not only on the computed function), the elevated property remains undecidable even though it breaks the extensionality that Rice's theorem requires; the proof rests on Kleene's recursion theorem, not on Rice. Consequently the class U of non-verifiable properties is closed under the elevation operator. Unbounded iteration of the operator climbs the arithmetical hierarchy -to Π02-completeness- consolidating non-verifiability as a structural fact. We further show that the supervisory regress does not terminate: no fnite tower of increasingly capable verifiers yields an unconditional certificate. A categorical reading of these results in the efective topos, in which elevation appears as an instance of Lawvere's fxed-point theorem, is left as a direction for future work.

Abstract: Completeness of an equational presentation guarantees an equality path but need not control the resources used along it. For finite graph expressions we measure derivational space by the largest input-output interface of an intermediate raw term. For every finite doubly ranked edge alphabet $Σ$, we prove that equal closed expressions of pattern width at most $k$ are joined by a derivation in which every step applies an equation in either direction and every intermediate width is at most a computable $B_Σ(k)$, independently of graph size. The derivation uses only the structural magmoid laws and the fifteen finite-graphoid schemes. The construction compiles each expression through protected cores and finite routing windows to an encoding-canonical representative $\operatorname{NF}_k$ of width at most $4k+4$. We call this property bounded equational coherence. We also prove $\operatorname{bw}(F)\le\operatorname{patw}(F)\le4(\operatorname{tw}(F)+1)$ whenever the underlying simple graph has at least two edges, separate layered linear from branching expressions on cliques, and provide machine-checkable witnesses and finite invariants for the first five nontrivial clique values.