Search events for 'all'
A logic for all reasons
TPSA 2026 People: Flavio Ascari, Roberto Bruni, Lorenzo Gazzella, Roberta Gori
… …
One rig to control them all
PLanQC 2026 People: Chris Heunen, Robin Kaarsgaard, Louis Lemonnier
… …
All for One and One for All: Program Logics for Exploiting Internal Determinism in Parallel Programs
POPL When: Fri 16 Jan 2026 10:30 - 10:55 People: Alexandre Moine, Sam Westrick, Joseph Tassarotti
… that the program is safe across all orderings, it
suffices to show that one … such
programs.
All results in this paper have been verified in Rocq using the Iris …
Verification of Generic VHDL Designs and Their Translation to Rocq
VMCAI 2026 When: Mon 12 Jan 2026 16:00 - 16:30 People: Ocan Sankur , Benoît Boyer, Florian Faissole
… by first translating them to Rocq. Because our translation keeps all parameters (a.k.a. … of given VHDL designs under all parameter valuations. These checks detect whether … that is valid for all parameter valuations, and which allows us to translate …
A positive perspective on term representation (Invited Talk)
PADL 2026 People: Dale Miller
… approaches to term representation. When all primitive types are given the negative … of substitution. On the other hand, when all primitive types are given the positive …
Compiling Quantum Lambda-Terms into Circuits via the Geometry of Interaction
PLanQC 2026 People: Kostia Chardonnet, Ugo Dal Lago, Naohiko Hoshino, Paolo Pistone
… , performs all the \emph{quantum} operations in the underlying $\lambda$-term …
Using Prolog to Translate Set Theory and B to SAT
PADL 2026 People: Michael Leuschel
… ) constraint solving to infer finite bounds for all variables. Second, Prolog …
Hole Refinements for Polymorphic Type-and-Example Driven Synthesis
PEPM 2026 People: Niek Mulleners, Johan Jeuring, Wouter Swierstra
… for shortcutting the synthesis when a subspecification covers all cases. We …
Gradually Retrofitting Assurance into Systems Software: A Separation-Logic Approach
TPSA 2026 People: Zain K Aamer, Rini Banerjee, Hiroyuki Katsura, David Kaloper-Meršinjak, Dimitrios J. Economou, Kayvan Memarian, Dhruv Makwana, Neel Krishnaswami, Benjamin C. Pierce, Christopher Pulte, Peter Sewell
… a chance of proving the function correct at all. It is clear that there are many …
Recursive Mutexes in Separation Logic
Rocq for Programming Languages 2026 When: Sat 17 Jan 2026 16:51 - 17:08 People: Ke Du, William Mansky, Paolo G. Giarrusso, Gregory Malecha
… by the same thread, and our specifications treat all acquires/releases uniformly …
Declarative Debugging for Modern Networks
PADL 2026 People: Anduo Wang, Matthew Caesar
… Network troubleshooting today relies largely on ticket systems, which log, record, replay, and analyze live events, while overlooking recent advances in SDNs, programmable networks, and verified data centers, all of which have produced …
Multi-Agent Systems for Traceable Bayesian Workflow
LAFI 2026 People: Xianda Sun, Andy Gordon, Hong Ge
… models and exploration traces documenting all modeling decisions. In experiments …
Try-Mopsa: Relational Static Analysis in Your Pocket
VMCAI 2026 When: Mon 12 Jan 2026 10:00 - 10:30 People: Raphaël Monat
… features all core components of Mopsa, and in particular it supports relational …
Mechanically Verified Universe Checking and Variance Inference for The Rocq Prover
Rocq for Programming Languages 2026 When: Sat 17 Jan 2026 14:30 - 14:45 People: Matthieu Sozeau, Marc Bezem
… will present all these aspects along with examples and our preliminary performance …
Verifying Synchronous Dataflow Programs with SMTCoq
Rocq for Programming Languages 2026 When: Sat 17 Jan 2026 15:15 - 15:30 People: Basile Pesin
… generic lemmas written once and for all, and discharges the program-specific …
Interpretable Configuration Optimization for Static Program Verification via Rule-Based and Counterfactual Reasoning
PADL 2026 People: Jaeseong Lee, Sopam Dasgupta, Gopal Gupta, Shiyi Wei
… baseline across all verification tools. On Jayhorn, CBMC, and Symbiotic, ConfigTuneX …
Input-based Three-Valued Abstraction Refinement
VMCAI 2026 When: Tue 13 Jan 2026 10:00 - 10:30 People: Jan Onderka, Stefan Ratschan
… Unlike Counterexample-Guided Abstraction Refinement (CEGAR), Three-Valued Abstraction Refinement (TVAR) is able to verify all properties of the mu-calculus. We present a novel algorithmic framework for TVAR that employs a simulator-like …
The HOL-Light library of Multivariate real analysis in Rocq
Rocq for Programming Languages 2026 When: Sat 17 Jan 2026 10:15 - 10:30 People: Abdelghani Alidra, Claudio Sacerdoti Coen, Frédéric Blanqui
… for the Rocq community. All tools underpinning out methodology are publicly available …
On Contextual Distances in Randomized Programming: Amplification and Lower Bounds
LAFI 2026 People: Houssein Mansour, Raphaëlle Crubillé
… is allowed and all programs terminate, this distance becomes trivial: any two non …
A Design for Massively Parallel Gibbs Sampling on the GPU via Static and Dynamic Analysis of Probabilistic Programs
LAFI 2026 People: Matin Ghavami, Martin C. Rinard, Vikash Mansinghka
… , or hierarchically on both levels. Hence, there are no one-size-fits-all solutions …
Efficiently Verifying Quantum Programs with Few T Gates
VMCAI 2026 When: Tue 13 Jan 2026 16:00 - 16:30 People: Youngchan Cho, Robert Rand
… rules, reduces all obligations to syntactic well-formedness side-conditions …
Probabilistic Verification for Modular Network-on-Chip Systems
VMCAI 2026 When: Tue 13 Jan 2026 17:00 - 17:30 People: Nick Waddoups, Jonah Boe, Arnd Hartmanns, Prabal Basu, Sanghamitra Roy, Koushik Chakraborty, Zhen Zhang
… models, all of which were instantiated from a generic modular router model …
Foundational Verification of Running-Time Bounds for Interactive Programs
CPP 2026 When: Mon 12 Jan 2026 17:07 - 17:30 People: Thomas Carotti, Andy Tockman, Pratap Singh, Andres Erbsen, Samuel Gruetter, Adam Chlipala
… bounds for interactive machine code, while allowing all per-application programming … machine code. All components are implemented and proved inside the Coq proof …
Can we formalise type theory intrinsically without any compromise? A case study in Cubical Agda
CPP 2026 When: Tue 13 Jan 2026 11:00 - 11:22 People: Liang-Ting Chen, Fredrik Nordvall Forsberg, Tzu-Chun Tsai
… support for quotient inductive types, all our constructions compute at a reasonable …
Lessons from Building an Auto-Active Verifier in Lean
Dafny 2026 When: Sun 11 Jan 2026 14:00 - 14:18 People: George Pîrlea, Vladimir Gladshtein, Qiyuan Zhao, Ilya Sergey
… as backend certificate checkers, Veil is a Lean library, with all its functionality …-programming facilities—like all powerful tools—can prove to be both a blessing and a curse, and it is not at all difficult to create an unmaintainable mess …
Lean4Lean: Mechanizing the Metatheory of Lean
WITS When: Sat 17 Jan 2026 09:00 - 10:00 People: Mario Carneiro
… and usable to verify all of Lean’s Mathlib library, forming an additional step …
Types as grammars
WITS When: Sat 17 Jan 2026 11:45 - 12:07 People: Gil Silva, Bernardo Almeida, Diana Costa, Andreia Mordido, Diogo Poças, Vasco T. Vasconcelos
… , this algorithm merely descends on their abstract syntax tree: there is, after all …
Verified VCG and Verified Compiler for Dafny
CPP 2026 When: Mon 12 Jan 2026 16:45 - 17:07 People: Daniel Nezamabadi, Magnus O. Myreen, Yong Kiam Tan
… executable machine code via the (already verified) CakeML compiler, all while …
Building Blocks for Step-Indexed Program Logics
CPP 2026 When: Tue 13 Jan 2026 12:06 - 12:28 People: Thomas Somers, Jonas Kastberg Hinrichsen, Lennard Gäher, Robbert Krebbers
… previously did not support. All our results are mechanized in the Rocq prover. …
Modular Specifications and Implementations of Random Samplers in Higher-Order Separation Logic
CPP 2026 When: Tue 13 Jan 2026 16:45 - 17:07 People: Virgil Marionneau, Félix Sassus-Bourda, Alejandro Aguirre, Lars Birkedal
… correctness results, as well as to derive additional reasoning principles for all …
Precise Reasoning about Container-Internal Pointers with Logical Pinning
CPP 2026 When: Tue 13 Jan 2026 16:22 - 16:45 People: Yawen Guan, Clément Pit-Claudel
… patterns not supported by traditional specifications. All of our results …
GnuZero: A Compiler-Based Zeroization Static Detection Tool for the Masses
PriSC When: Sun 11 Jan 2026 14:18 - 14:36 People: Pierrick Philippe, Mohamed Sabt, Pierre-Alain Fouque
… tool that detects missing zeroization for all stack/heap variables storing …, GnuZero passes all the relevant Juliet’s test programs, namely associated …
WP-Preserving Compilation -- Preserving Weakest Preconditions For End-to-End Verification
PriSC When: Sun 11 Jan 2026 12:12 - 12:30 People: Carmine Abate, Mohamed Elsheikh, Kleio Liotati, Frantisek Farka, Sebastian Ertel
… layers, all the way down to the hardware. Large scale end-to-end verification …
Specifying ABIs with Realizability and Type-Preserving Compilation
PriSC When: Sun 11 Jan 2026 11:18 - 11:36 People: Brianna Marshall, Ryan Doenges, Owen Duckham, Ari Prakash, Maxime Legoupil, Elan Semenova, Lars Birkedal, Amal Ahmed
… by WebAssembly computations—doing all the work that requires expertise …
Explicit Abstraction Barrier for Autoactive Verification
Dafny 2026 When: Sun 11 Jan 2026 11:18 - 11:36 People: Paul Patault
… them at all. …
Formal Verification of Minimax Algorithms
Dafny 2026 When: Sun 11 Jan 2026 14:18 - 14:36 People: Wieger Wesselink, Kees Huizing, Huub van de Wetering
… algorithms. All verification artifacts, including proofs and Python implementations …
Mind the Boundary: Detecting Undefined Behavior Across Rust’s FFI
PriSC When: Sun 11 Jan 2026 11:00 - 11:18 People: Andreea Costea
… Memory safety bugs are pervasive in nearly all compiled programming languages. To mitigate this, modern languages such as Rust have been designed with a sophisticated ownership system that enforces memory safety. This system controls how …
FSLH: Flexible Mechanized Speculative Load Hardening
PriSC When: Sun 11 Jan 2026 16:00 - 16:17 People: Jonathan Baumann, Roberto Blanco, Léon Ducruet, Sebastian Harwig, Cătălin Hriţcu
… for general use, since it conservatively assumes that all data is secret. In recent …
Specification-Guided Repair of Arithmetic Errors in Dafny Programs using LLMs
Dafny 2026 When: Sun 11 Jan 2026 17:25 - 17:42 People: Valentina Wu, Alexandra Mendes, Alexandre Abreu
… techniques often rely on test suites for validation, but these may not capture all …
Formal Verification for JavaScript Regular Expressions: A Proven Mechanized Semantics and Its Applications
POPL When: Wed 14 Jan 2026 10:55 - 11:20 People: Aurèle Barrière, Victor Deng, Clément Pit-Claudel
… recording all possible matches and their respective priority. All our definitions …
AdapTT: Functoriality for Dependent Type Casts
POPL When: Fri 16 Jan 2026 14:00 - 14:25 People: Arthur Adjedj, Meven Lennon-Bertrand, Thibaut Benjamin, Kenji Maillard
… The ability to cast values between related types is a leitmotiv of many flavors of dependent type theory, such as observational type theories, subtyping, or cast calculi for gradual typing. These casts all exhibit a common structural …
The Simple Essence of Boolean-Algebraic Subtyping: Semantic Soundness for Algebraic Union, Intersection, Negation, and Equi-recursive Types
POPL When: Fri 16 Jan 2026 11:20 - 11:45 People: Chun Yin Chau, Lionel Parreaux
… that if an inequality holds between two types under all five homomorphisms … surprisingly, no changes to subtyping at all.
Our new approach to the semantics … more approachable. Tellingly, all our subtyping soundness proofs fit inside …
Typing Strictness
POPL When: Wed 14 Jan 2026 15:15 - 15:40 People: Daniel Sainati, Joseph W. Cutler, Benjamin C. Pierce, Stephanie Weirich
… to the call-by-push-value one. All our results are mechanized in Rocq. …
Extensible Data Types with Ad-Hoc Polymorphism
POPL When: Wed 14 Jan 2026 14:00 - 14:25 People: Matthew Toohey, Yanning Chen, Ara Jamalzadeh, Ningning Xie
… establishing the soundness of λ⇒ρ. All proofs are mechanized in the Lean 4 proof …
Hyperfunctions: Communicating Continuations
POPL When: Wed 14 Jan 2026 11:20 - 11:45 People: Donnacha Oisín Kidney, Nicolas Wu
… the hyperfunctions hidden in all of these algorithms, and we exposit the common pattern …
Bounded Treewidth, Multiple Context-Free Grammars, and Downward Closures
POPL When: Wed 14 Jan 2026 10:30 - 10:55 People: C. Aiswarya, Pascal Baumann, Prakash Saivasan, Lia Schütze, Georg Zetzsche
… a graph; then we consider the subset of all graphs that have
a treewidth at most $k …
includes all bounded-treewidth systems studied in the literature), this work …
Discrete and Continuous Models for Concurrent Systems: From Petri Nets to Directed Spaces
Tutorials When: Sun 11 Jan 2026 14:00 - 15:30Sun 11 Jan 2026 16:00 - 17:30 People: Uli Fahrenberg
… Concurrent computing systems are those in which several events may happen in parallel; in fact that includes most modern systems. The verification of such systems is difficult: if one considers all possible interleavings of concurrent …
Veil: Automated and Interactive Verification of Transition Systems
Tutorials When: Mon 12 Jan 2026 14:00 - 15:30Mon 12 Jan 2026 16:00 - 17:30 People: George Pîrlea, Qiyuan Zhao
… with the full power of a modern proof assistant, all while maintaining …
Di- is for Directed: First-Order Directed Type Theory via Dinaturality
POPL When: Fri 16 Jan 2026 10:30 - 10:55 People: Andrea Laretto, Fosco Loregian, Niccolò Veltri
… . This directed J-rule comes with a simple syntactic restriction which recovers all …
Rows and Capabilities as Modal Effects
POPL When: Fri 16 Jan 2026 14:50 - 15:15 People: Wenhao Tang, Sam Lindley
… Effect handlers allow programmers to model and compose computational
effects modularly. Effect systems statically guarantee that all
effects are handled. Several recent practical effect systems are
based on either row polymorphism …
Recurrence Sets for Proving Fair Non-termination under Axiomatic Memory Consistency Models
POPL When: Wed 14 Jan 2026 15:15 - 15:40 People: Thomas Haas, Roland Meyer, Hernán Ponce de León, Andrés Lomelí Garduño
… non-termination on all practical memory models, and even complete on many …
A Synthetic Reconstruction of Multiparty Session Types
POPL When: Fri 16 Jan 2026 16:35 - 17:00 People: David Castro-Perez, Francisco Ferreira, Sung-Shik Jongmans
… . The entire framework, including all theorems and many examples, has been …
Endangered by the Language But Saved by the Compiler: Robust Safety via Semantic Back-Translation
POPL When: Thu 15 Jan 2026 16:35 - 17:00 People: Niklas Mück, Aina Linn Georges, Derek Dreyer, Deepak Garg, Michael Sammler
… framework for multi-language semantics. All our results are mechanized in the Rocq …
Nice to Meet You: Synthesizing Practical MLIR Abstract Transformers
POPL When: Thu 15 Jan 2026 16:10 - 16:35 People: Xuanyu Peng, Dominic Kennedy, Yuyou Fan, Ben Greenman, John Regehr, Loris D'Antoni
… Static analyses play a fundamental role during compilation: they discover facts that are true in all executions of the code being compiled, and then these facts are used to justify optimizations and diagnostics. Each static analysis …
An Equational Axiomatization of Dynamic Threads via Algebraic Effects: Presheaves on Finite Relations, Labelled Posets, and Parameterized Algebraic Theories
POPL When: Fri 16 Jan 2026 14:00 - 14:25 People: Ohad Kammar, Jack Liell-Cock, Sam Lindley, Cristina Matache, Sam Staton
… if they are equal under all closing substitutions: syntactically complete …
A Relational Separation Logic for Effect Handlers
POPL When: Thu 15 Jan 2026 10:20 - 10:45 People: Paulo Emílio de Vilhena, Simcha van Collem, Ines Wright, Robbert Krebbers
… , thereby enjoying the rigour of a mechanised theory and all the reasoning …
Optimising Density Computations in Probabilistic Programs via Automatic Loop Vectorisation
POPL When: Fri 16 Jan 2026 14:00 - 14:25 People: Sangho Lim, Hyoungjin Lim, Wonyeol Lee, Xavier Rival, Hongseok Yang
… the baseline, which is limited to a subset of models, our method effectively handled all …
The Complexity of Testing Message-Passing Concurrency
POPL When: Thu 15 Jan 2026 11:35 - 12:00 People: Zheng Shi, Lasse Møldrup, Umang Mathur, Andreas Pavlogiannis
… , as well as for database isolation levels. A common theme in all these settings …
Miri: Practical Undefined Behavior Detection for Rust
POPL When: Wed 14 Jan 2026 11:20 - 11:45 People: Ralf Jung, Benjamin Kimock, Christian Poveda, Eduardo Sánchez Muñoz, Oli Scherer, Qian (Andy) Wang
… we present Miri, the first tool that can find all de-facto Undefined Behavior …
Counting and Sampling Traces in Regular Languages
POPL When: Fri 16 Jan 2026 16:10 - 16:35 People: Alexis de Colnet, Kuldeep S. Meel, Umang Mathur
… from a distribution that is approximately uniform over all such traces …
Hardware-Software Contracts for High Assurance with Applications to Side-Channel Security
POPL When: Fri 16 Jan 2026 09:00 - 10:00 People: Caroline Trippel
… ), establishing hardware side-channel attacks as a threat to all programs that hold …
Encode the Cake and Eat It Too: Controlling Computation in Type Theory, Locally
POPL When: Fri 16 Jan 2026 14:50 - 15:15 People: Yann Leray, Théo Winterhalter
… . Additionally, all the results in this have been formalised in Rocq. …
Separating the Wheat from the Chaff: Understanding (In-)Completeness of Proof Mechanisms for Separation Logic with Inductive Definitions
POPL When: Thu 15 Jan 2026 11:35 - 12:00 People: Neta Elad, Adithya Murali, Sharon Shoham
…
that it is incomplete:
there is no procedure that will provide a proof
for all valid …
ChiSA: Static Analysis for Lightweight Chisel Verification
POPL When: Wed 14 Jan 2026 10:55 - 11:20 People: Jiacai Cui, Qinlin Chen, Zhongsheng Zhan, Tian Tan, Yue Li
… recognized by developers and scheduled for future fixes—and detected all 60 …