14,842 papers · page 10 of 743
The superposition calculus has been formalized in Isabelle/HOL twice before but in both cases without a type system. Nowadays, modern superposition provers support types. We extend an existing Isabelle formalization of untyped superposition with simple monomorphic types, or sorts…
Symbolic execution (SE) is a program analysis technique that executes the program with symbolic inputs. In modern SE engines, when the analysis of a given program is exhaustive, the analyzed program is typically considered safe, i.e., free of bugs, but no formal guarantees are pr…
The Cylindrical Algebraic Decomposition (CAD in short) is a fundamental tool of semi-algebraic geometry. It is a doubly-exponential time algorithm that enables most famously to eliminate quantifiers from a formula in the theory of real closed fields. In particular, it allows to d…
Pointer analysis for Rust faces unique challenges arising from its ownership-based memory model and layered abstractions, which complicate how heap-allocated objects flow across functions. Existing k-limited callsite abstractions - designed for earlier languages - are both imprec…
Parsing well-designed computer languages should not be a hard problem, be it for humans or for machines. This is not a new idea: in 1973, Vaughan R. Pratt argued against formalistic grammar specifications and in favor of a more intuitive and meaningful approach to designing and p…
Railroad diagrams (also called "syntax diagrams") are a common, intuitive visualization of grammars, but limited tooling and a lack of formal attention to their layout mostly confines them to hand-drawn documentation. We present the first formal treatment of railroad diagram layo…
We propose a symbolic execution method for analyzing the safety of software under fault attacks both accurately and efficiently. Fault attacks leverage physically injected hardware faults in an embedded system to break the safety of a software program. While there are existing me…
Real-time collaborative programming tools synchronize source code as text, propagating keystrokes or text patches to other collaborators. This propagation of unstructured text often leads to syntactically invalid states, because edits take place by character position rather than …
Tanaka et al. proposed a type system for verifying functional correctness properties of programs that use arrays and pointer arithmetic. Their system extends ConSORT - a type system combining fractional ownership and refinement types for imperative program verification - with sup…
Swarm protocols are a recently introduced formalism for specifying, implementing, and verifying peer-to-peer systems called swarms. A swarm consists of distributed agents called machines that communicate by asynchronous event propagation. Following a local-first model, each machi…
Given an input program, sound static analyzers compute a list of potential runtime errors in it. However, measuring their precision and comparing their results remains challenging. In this work, we formalize a notion of transparent static analyzers that report the proof obligatio…
Persistent Memory offers byte-addressable persistence but exposes developers to new concurrency bugs - persistency-induced races - where a thread might read unpersisted data, potentially leading to inconsistencies after crashes. Existing tools face important practical limitations…
IFDS taint analysis is inherently context- and flow-sensitive, allowing precise encoding of field sensitivity in access-path generation. However, preserving this level of precision in practice is difficult, leading to over-tainting - marking more data facts as tainted than necess…
We present Linearizability Hoare Logic (LHL), the first mechanized, sound, and complete program logic for atomic, set, and interval linearizability. We achieve this by showing soundness and completeness of LHL w.r.t. a more general criterion, compositional linearizability, which …
Performance-critical applications, including large-scale program analyses, graph analyses, and distributed system analyses, rely on fixed-point computations. The introduction of recursion using the WITH RECURSIVE keyword in SQL:1999 extended the ability of relational database sys…
Inline tests validate individual program statements and expressions, and they detect many seeded faults (i.e., mutants) that unit tests miss in these target statements. ExLi is the only automated inline-test generation technique today; it carves inline tests from method-level uni…
Abstract interpreters enable sound static analysis, but are hard to develop. In recent years, researchers have proposed a component-based approach to developing abstract interpreters, where different parts of the abstract domain (e.g., numeric, call frame, heap) are handled by is…
Artifact for ECOOP paper 2026: Efficient Symbolic Execution of Software under Fault Attacks.
This paper introduces NEST (Network Enforced Session Types), a runtime verification framework that moves application-level protocol monitoring into the network fabric. Unlike prior work that instruments or wraps application code, we synthesise packet-level monitors that enforce p…
Branch mispredictions cause catastrophic performance penalties in modern processors, leading to performance loss. While hardware predictors and profile-guided techniques exist, data-dependent branches with irregular access patterns remain challenging. Traditional if-conversion el…