14,842 papers · page 10 of 743
Balázs Tóth, Martin Desharnais-Schäfer, Jasmin Blanchette
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…
David Trabish, Shachar Itzhaky
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…
Quentin Vermande
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…
Wenyao Chen, Wei Li, Jingling Xue
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…
Luyu Cheng, Lionel Parreaux
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…
Shardul Chiplunkar, Clément Pit-Claudel
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…
Yuzhou Fang, Chenyu Zhou, Jingbo Wang, Chao Wang
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…
Leon Freudenthaler, Karl Michael Göschka
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 …
Yusuke Fujiwara, Yusuke Matsushita, Kohei Suenaga, Atsushi Igarashi
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…
Florian Furbach, Lucas Clorius, Roland Kuhn, Hernán C. Melgratti, Alceste Scalas, Emilio Tuosto
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…
Tom Goalard, Karoliine Holter, Simmo Saan, Vesal Vojdani, Raphaël Monat
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…
João Gonçalves, José Fragoso Santos, Rodrigo Rodrigues, Miguel Matos
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…
Yujiang Gui, Yonggang Tao, Jingling Xue
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…
Eashan Hatti, Arthur Oliveira Vale, Zhongye Wang, Yueyang Feng, Zhong Shao
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 …
Anna Herlihy, Amir Shaikhha, Anastasia Ailamaki, Martin Odersky
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…
Pengyue Jiang, Yu Liu, Anna Guo, Milos Gligoric, Owolabi Legunsen
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…
Sven Keidel, Raphaël Monat, Sebastian Erdweg
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…
Sebastián Krynski, Filip Ríha, Filip Krikava, Jan Vitek
Artifact for ECOOP paper 2026: Efficient Symbolic Execution of Software under Fault Attacks.
Jens Kanstrup Larsen, Alceste Scalas, Guy Amir, Jules Jacobs, Jana Wagemaker, Nate Foster
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…
Yuze Li, Srinivasan Ramachandra Sharma, Charitha Saumya, Ali Raza Butt, Kirshanthan Sundararajah
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…