TPSA 2025
who it's for
formal methods researchers, programming language researchers, verification tool builders, static analysis engineers, software reliability researchers, compiler engineers, distributed systems verification engineers, quantum software researchers
topics
shared abduction; biabductive loop acceleration; summary specialization for Infer; concurrent quantum separation logic; semantics lifting for FFT; cyclic message histories for verification; incorrectness separation logic; forward-driven backward analysis; symbolic regular expressions for traces; TopKAT domain/codomain completeness; type-soundness refutation via incorrectness; total outcome logic for termination
| title | author | length |
|---|---|---|
| Compositional Shape Analysis with Shared Abduction and Biabductive Loop Acceleration(…) | Florian Sextl, Adam Rogalewicz, Tomáš Vojnar, Florian Zuleger | 16m |
Introduces Shared Abduction that maintains one shared precondition across multiple current states so biabduction discovers a single sound precondition for… | ||
| Enhancing Infer Compositional Analysis with Summary Specialization | David Pichardie | 18m |
Infer adds summary specialization to its compositional, on‑demand bottom‑up analyzer: compute per‑function summaries under lightweight assumptions… | ||
| Concurrent Quantum Separation Logic for Fine-Grained Parallelism | Yusuke Matsushita, Kengo Hirata, Ryo Wakizaka | 18m |
Introduces a concurrent quantum separation logic that verifies fine-grained parallel quantum code, with a concrete linear combination of Hoare triples rule to… | ||
| Towards Semantics Lifting for Scientific Computing: A Case Study on FFT | Naifeng Zhang, Sanil Rao, Mike Franusich, Franz Franchetti | 17m |
A stepwise semantics lifting approach uses GPT-generated FFT C code and an extended SPIRAL ICode/SigmaSPL pipeline to recover high-level FFT semantics… | ||
| Cyclic Message Histories for Automated Safety Verification of Distributed Algorithms | Christian Fontenot, Gowtham Kaki, Bor-Yuh Evan Chang | 16m |
Claims an automated verifier that uses a separation logic augmented with message histories and a goal-directed abstract interpretation to soundly… | ||
| Domain Reasoning In TopKAT: Reduction and Completeness | Cheng Zhang, Arthur Azevedo de Amorim, Marco Gaboardi | 19m |
TopKAT is incomplete over relational models: there exists an inequality true in every relational TopKAT but unprovable from TopKAT axioms, yet adding that… | ||
| Scalable Bug Detection for Internally Unsafe Libraries: A Logical Approach to Type(…) | Pedro Carrott, Sacha-Élie Ayoun, Azalea Raad | 18m |
Claims a fully automatic under-approximate method that refutes type soundness in libraries by encoding type assignments as separation-logic assertions and… | ||
| U-turn: Forward-driven backward analysis for incorrectness | Flavio Ascari, Roberto Bruni, Roberta Gori, Azalea Raad | 16m |
Combines forward IL to produce only true reachable errors with a backward SIL proof that extracts the actual preconditions responsible for those errors… | ||
| From Traces to Program Incorrectness: A Type-Theoretic Approach | Yongwei Yuan, Zhe Zhou, Julia Belyakova, Benjamin Delaware, Suresh Jagannathan | 17m |
Claims a type-theoretic, underapproximate correctness method that treats library interactions as traces encoded with symbolic regular expressions and reasoned… | ||
| Calculational design of Incorrectness Separation Logic | Lorenzo Gazzella | 17m |
A semantics-first proof recipe called calculational design derives axioms from closure operators (frame, disjunction, consequence) and picks minimal elements… | ||
| Gradual Exact Logic: Unifying Hoare Logic and Incorrectness Logic via Gradual Verification | Conrad Zimmerman, Jenna DiVincenzo | 16m |
Claims a formal semantics for optimistic verification by defining gradual exact logic as a consistent lifting of exact triples over a collecting semantics… | ||
| Partial Incorrectness Logic | Lena Verscht, Ånrán Wáng, Benjamin Lucien Kaminski | 15m |
Defines "partial incorrectness" as an underapproximation of the strongest liberal postcondition that admits final states that are provably unreachable… | ||
| Data Structure Abstraction and Incorrectness Separation Logic | Andreas Lööw | 08m |
Extends incorrectness separation logic to support data-structure abstraction (lists, sets) and reports a mostly complete Rock mechanization. Shows standard ISL… | ||
| Total Outcome Logic: Termination and Nontermination Proving for Effectful Branching | James Li, Noam Zilberstein, Alexandra Silva | 20m |
Presents Total Outcome Logic, a single logic that models program runs as maps from states to semiring-weighted outcomes and adds an explicit divergence outcome… | ||
| nothing matches | ||