Search events for 'all'
All Your Base Are Belong to Us: Sort Polymorphism for Proof Assistants
POPL When: Fri 24 Jan 2025 17:40 - 18:00 People: Josselin Poiret, Gaetan Gilbert, Kenji Maillard, Pierre-Marie Pédrot, Matthieu Sozeau, Nicolas Tabareau, Éric Tanter
… . In particular, in order to avoid duplicating definitions to inhabit all (combinations … between sorts is currently ad hoc and limited in all major proof assistants …
Formal Verification of a Software Defined Delay-Tolerant Network
CoqPL 2025 When: Sat 25 Jan 2025 15:07 - 15:30 People: Jan-Paul Ramos-Davila
… the behavior of certain P4 programs without needing to verify all aspects …
A Semantic Approach to Robust Property Preservation
PriSC 2025 When: Mon 20 Jan 2025 10:05 - 10:30 People: Niklas Mück, Michael Sammler, Aina Linn Georges, Derek Dreyer, Deepak Garg
… Compiler security can be defined as the preservation of robust properties, i.e., properties that hold in all contexts including adversarial contexts. Although attractive in concept, this approach runs into two challenges in practice …
A Semantic Logical Relation for Termination of Intuitionistic Linear Logic Session Types
CoqPL 2025 When: Sat 25 Jan 2025 14:45 - 15:07 People: Tarakaram Gollamudi, Jules Jacobs, Yue Yao, Stephanie Balzer
… not require terms to be well-typed. All results have been mechanized in the Coq …
Counterexamples in Safe Rust
PriSC 2025 When: Mon 20 Jan 2025 14:50 - 15:14 People: Muhammad Hassnain, Caleb Stanford
… attacks? All of our examples and associated data are available as an open source …
Preservation of Speculative Constant-time by Compilation
PriSC 2025 When: Mon 20 Jan 2025 11:50 - 12:14 People: Santiago Arranz Olmos, Gilles Barthe, Lionel Blatter, Benjamin Gregoire, Vincent Laporte
… speculative constant-time type checker and demonstrate that all cryptographic …
SNIP: Speculative Execution and Non-Interference Preservation for Compiler Transformations
PriSC 2025 When: Mon 20 Jan 2025 16:50 - 17:14 People: Sören van der Wall, Roland Meyer
… We address the problem of preserving non-interference across compiler transformations under speculative semantics. We develop a proof method that ensures the preservation uni- formly across all source programs. The basis of our proof …
Domain Reasoning In TopKAT: Reduction and Completeness
TPSA 2025 People: Cheng Zhang, Arthur Azevedo de Amorim, Marco Gaboardi
… models. In other words, there are properties that hold true of all relational …
Imperative Quantum Programming with Ownership and Borrowing in Guppy
PLanQC 2025 When: Sat 25 Jan 2025 17:07 - 17:30 People: Mark Koch, Agustin Borgna, Craig Roy, Alan Lawrence, Kartik Singhal, Seyon Sivarajah, Ross Duncan
… guarantees. All ideas presented here have been implemented in Quantinuum’s Guppy …
Helping users to reduce Brittleness in their Dafny programs - a success story
Dafny 2025 When: Sun 19 Jan 2025 11:00 - 11:18 People: Remy Willems, Matthias Schlaipfer, Olivier Bouissou
… Brittleness, or proof instability, is the problem where small changes to an SMT query cause the SMT solver to either take much longer to return than previously, or fail to return a result at all. Tackling this problem is critical …
Dafny as Verification-Aware Intermediate Language for Code Generation
Dafny 2025 When: Sun 19 Jan 2025 16:54 - 17:12 People: Yue Chen Li, Stefan Zetzsche, Siva Somayyajula
… program is then compiled to the target language and returned to the user. All user …
Towards Symbolic Execution for Probability and Non-determinism
LAFI 2025 When: Sun 19 Jan 2025 09:27 - 09:42 People: Jack Czenszak, John Li, Steven Holtzen
… that this semantics is sound and complete in the sense of Torlak and Bodik: it captures all …
An Isabelle formalization of co-rewrite pairs for non-reachability in conditional rewriting
CPP 2025 When: Mon 20 Jan 2025 14:00 - 14:30 People: Dohan Kim, Teppei Saito, René Thiemann, Akihisa Yamada
… (WPO) and its variant co-WPO. All of these three co-rewrite pairs are also added …
Further Tackling Post Correspondence Problem and Proof Generation
CPP 2025 When: Mon 20 Jan 2025 17:00 - 17:30 People: Akihiro Omori, Yasuhiko Minamide
… successfully solved all instances except for three. To ensure the correctness of our …
Improving Static Analysis using Information Collected at Runtime
TPSA 2025 People: Radu Grigore
… The classic theory of static analysis aims to catch all problems by overapproximating the set of executions. In practice this has the unfortunate consequence that false positives are to be expected. Soon, developers learn to ignore what …
C3G: Causally Constrained Counterfactual Generation
PADL 2025 When: Mon 20 Jan 2025 14:30 - 15:00 People: Sopam Dasgupta, Farhad Shakerin, Joaquín Arias, Elmer Salazar, Gopal Gupta
… and justified by imagining worlds where some or all factual assumptions are altered …
Solvers, unite! A simple unified semantics for reasoning with assurance and agreement
PADL 2025 When: Mon 20 Jan 2025 09:00 - 10:00 People: Y. Annie Liu
… results in all cases.
Additionally, we compare 10 different classes …
The Focked-up ZX Calculus: Picturing Continuous-Variable Quantum Computation
PLanQC 2025 People: Razin A. Shaikh, Lia Yeh, Stefano Gogioso
… interactions. We ensure this calculus is complete for all of Gaussian CVQC …
Formally verified hardening of C programs against hardware fault injection
CPP 2025 When: Tue 21 Jan 2025 11:30 - 12:00 People: Basile Pesin, Sylvain Boulmé, David Monniaux, Marie-Laure Potet
… . We used this new model to formally prove the efficacy of the countermeasure: all …
Proto-Quipper with Reversing and Control
PLanQC 2025 When: Sat 25 Jan 2025 16:45 - 17:07 People: Peng Fu, Kohei Kishida, Neil Julien Ross, Peter Selinger
… not all circuits are reversible and/or controllable, we use a type system …
QuteFuzz: Fuzzing quantum compilers using randomly generated circuits with control flow and subcircuits
PLanQC 2025 When: Sat 25 Jan 2025 10:08 - 10:30 People: Ilan Iwumbwe, Benny Zong Liu, John Wickerson
… if-else, switch), all with varying depths of nesting and a variety of gates …
Algebras for Deterministic Computation are Inherently Incomplete
POPL When: Thu 23 Jan 2025 17:20 - 17:40 People: Balder ten Cate, Tobias Kappé
… , and iteration) it is able to express all non-deterministic finite state control … a similar finite set of constructs that can capture all deterministic …
Stateless Model Checking Concurrent and Distributed Programs
Tutorials When: Tue 21 Jan 2025 09:00 - 10:30Tue 21 Jan 2025 11:00 - 12:30 People: Michalis Kokologiannakis, Viktor Vafeiadis
… . The model checker then explores all the possible executions of the program (i.e., all thread interleavings, all weak memory consistency effects) in a very …
On Extending Incorrectness Logic with Backwards Reasoning
POPL When: Thu 23 Jan 2025 13:40 - 14:00 People: Freek Verbeek, Md Syadus Sefat, Zhoulai Fu, Binoy Ravindran
… (it allows to focus on fewer than all the paths). We prove soundness … at once – is highly useful. The logic, the proof system and all theorems have …
RELINCHE: Automatically Checking Linearizability under Relaxed Memory Consistency
POPL When: Thu 23 Jan 2025 15:20 - 15:40 People: Pavel Golovin, Michalis Kokologiannakis, Viktor Vafeiadis
… all possible other more constrained clients of the library.
RELINCHE scales … for all client programs with up to 9 library method invocations, and finds …
RE#: High Performance Derivative-Based Regex Matching with Intersection, Complement and Restricted Lookarounds
POPL When: Thu 23 Jan 2025 10:40 - 11:00 People: Ian Erik Varatalu, Margus Veanes, Juhan Ernits
… the next fastest regex engine in Rust on the baseline, and outperforms all …
MPL: Provably Efficient Parallel Programming
Tutorials When: Sun 19 Jan 2025 14:00 - 15:30Sun 19 Jan 2025 16:00 - 17:30 People: Sam Westrick
… * relative to the work-span cost model, preserving all logical parallelism …
Grove: A Bidirectionally Typed Collaborative Structure Editor Calculus
POPL When: Thu 23 Jan 2025 11:20 - 11:40 People: Michael D. Adams, Eric Griffis, Thomas J. Porter, Sundara Vishnu Satish, Eric Zhao, Cyrus Omar
…
and all edits commute, i.e. the repository state forms a commutative replicated data … vertices and edges. All edits amount to edge insertion and deletion …, i.e. all editor states in Grove are statically meaningful, so developers can use …
Consistency of a Dependent Calculus of Indistinguishability
POPL When: Wed 22 Jan 2025 15:00 - 15:20 People: Yiyun Liu, Jonathan Chan, Stephanie Weirich
… , normalizing, and that type conversion is decidable. We have mechanized all results …
A quantitative probabilistic relational Hoare logic
POPL When: Wed 22 Jan 2025 15:00 - 15:20 People: Martin Avanzini, Gilles Barthe, Benjamin Gregoire, Davide Davoli
… soundness and completeness results for all \emph{almost surely terminating …
VeriRT: An End-To-End Verification Framework for Real-Time Distributed Systems
POPL When: Fri 24 Jan 2025 14:00 - 14:20 People: Yoonseung Kim, Sung-Hwan Lee, Yonghyun Kim, Chung-Kil Hur
… . We provide two case studies on realistic real-time systems. All the results …
Formal Foundations for Translational Separation Logic Verifiers
POPL When: Wed 22 Jan 2025 17:00 - 17:20 People: Thibault Dardinier, Michael Sammler, Gaurav Parthasarathy, Alexander J. Summers, Peter Müller
… and for all in the equivalence proof with the operational semantics rather than … for a subset of Viper, and all proofs. …
Simple Linear Loops: Algebraic Invariants and Applications
POPL When: Fri 24 Jan 2025 11:00 - 11:20 People: Rida Ait El Manssour, George Kenison, Mahsa Shirmohammadi, Anton Varonka
… invariant for simple linear loops, generating all polynomial equations that hold among program variables across all reachable states. The key to achieving our …
Flo: a Semantic Foundation for Progressive Stream Processing
POPL When: Fri 24 Jan 2025 15:00 - 15:20 People: Shadaj Laddad, Alvin Cheung, Joseph M. Hellerstein, Mae Milano
… Streaming systems are present throughout modern applications, enabling real-time processing of continuous data. Existing languages have a variety of semantic models and guarantees that are not composable. Yet all these languages …
Preservation of speculative constant-time by compilation
POPL When: Fri 24 Jan 2025 17:20 - 17:40 People: Santiago Arranz Olmos, Gilles Barthe, Lionel Blatter, Benjamin Gregoire, Vincent Laporte
… type checker and demonstrate that all cryptographic implementations written …
Maximal Simplification of Polyhedral Reductions
POPL When: Wed 22 Jan 2025 10:40 - 11:00 People: Louis Narmour, Tomofumi Yuki, Sanjay Rajopadhye
… automatically, but previous methods cannot exploit all available reuse …
QuickSub: Efficient Iso-Recursive Subtyping
POPL When: Fri 24 Jan 2025 11:20 - 11:40 People: Litao Zhou, Bruno C. d. S. Oliveira
… how type soundness can be proved using QuickSub. All the results have been …
Compositional imprecise probability: a solution from graded monads and Markov categories
POPL When: Wed 22 Jan 2025 15:40 - 16:00 People: Jack Liell-Cock, Sam Staton
… desiderata are that we would like our model to support all kinds of composition …
SNIP: Speculative Execution and Non-Interference Preservation for Compiler Transformations
POPL When: Fri 24 Jan 2025 17:40 - 18:00 People: Sören van der Wall, Roland Meyer
… We address the problem of preserving non-interference across compiler transformations under speculative semantics. We develop a proof method that ensures the preservation uniformly across all source programs. The basis of our proof method …
Bidirectional Higher-Rank Polymorphism with Intersection and Union Types
POPL When: Thu 23 Jan 2025 15:40 - 16:00 People: Shengyi Jiang, Chen Cui, Bruno C. d. S. Oliveira
… and inspire the design of novel type inference algorithms. To ensure rigor, all …
MimIR: An Extensible and Type-Safe Intermediate Representation for the DSL Age
POPL When: Fri 24 Jan 2025 10:40 - 11:00 People: Roland Leißa, Marcel Ullrich, Joachim Meyer, Sebastian Hack
… . We show that in all three studies, MimIR produces code that has state …
Finite-Choice Logic Programming
POPL When: Wed 22 Jan 2025 15:20 - 15:40 People: Chris Martens, Robert Simmons, Michael Arntzenius
… -choice logic programming contains all the expressive power of the stable model …
Approximate Relational Reasoning for Higher-Order Probabilistic Programs
POPL When: Wed 22 Jan 2025 15:20 - 15:40 People: Philipp G. Haselwarter, Kwing Hei Li, Alejandro Aguirre, Simon Oddershede Gregersen, Joseph Tassarotti, Lars Birkedal
… , and a collection of rejection samplers. All of the results have been mechanized in the Coq …
Program Analysis via Multiple Context Free Language Reachability
POPL When: Wed 22 Jan 2025 11:00 - 11:20 People: Giovanna Kobus Conrado, Adam Husted Kjelstrøm, Jaco van de Pol, Andreas Pavlogiannis
… . Thus, for $r=1$, our algorithm is optimal within a factor $n$ for all levels …{all} tainted information on 8 out of 11 benchmarks, while it has remarkable …
Do You Even Lift? Strengthening Compiler Security Guarantees Against Spectre Attacks
POPL When: Fri 24 Jan 2025 17:00 - 17:20 People: Xaver Fabian, Marco Patrignani, Marco Guarnieri, Michael Backes
… proofs should target a speculative semantics capturing the effects of all …
Inference Plans for Hybrid Particle Filtering
POPL When: Thu 23 Jan 2025 10:40 - 11:00 People: Ellie Y. Cheng, Eric Atkinson, Guillaume Baudart, Louis Mandel, Michael Carbin
… analysis is precise in practice, identifying all satisfiable inference plans in 27 …
Symbolic Automata: omega-Regularity Modulo Theories
POPL When: Wed 22 Jan 2025 11:20 - 11:40 People: Margus Veanes, Thomas Ball, Gabriel Ebner, Ekaterina Zhuchko
… of classic automata and logics in a unified framework that provides all the necessary …
Semantic Logical Relations for Timed Message-Passing Protocols
POPL When: Fri 24 Jan 2025 15:40 - 16:00 People: Yue Yao, Grant Iraci, Cheng-En Chuang, Stephanie Balzer, Lukasz Ziarek
… for program verification: \textit{(i)} \emph{once-and-for-all} verification …
TensorRight: Automated Verification of Tensor Graph Rewrites
POPL When: Wed 22 Jan 2025 14:00 - 14:20 People: Jai Arora, Sirui Lu, Devansh Jain, Tianfan Xu, Farzin Houshmand, Phitchaya Mangpo Phothilimthana, Mohsen Lesani, Praveen Narayanan, Karthik Srinivasa Murthy, Rastislav Bodík, Amit Sabne, Charith Mendis
… ranks, under which bounded verification of all instances implies the correctness …
Progressful Interpreters for Efficient WebAssembly Mechanisation
POPL When: Fri 24 Jan 2025 17:00 - 17:20 People: Xiaojia Rao, Stefan Radziuk, Conrad Watt, Philippa Gardner
… are currently all separately defined by WasmCert-Coq. First, the approach …