Search events for 'all'
How to secure a distributed database such as OpenRiak with open-source tools
Tutorials When: Sun 12 Oct 2025 16:00 - 17:30Sun 12 Oct 2025 14:00 - 15:30 People: Nicholas Adams, Peter Clark
… For ease of use, many pieces of software are insecure in their default settings. Not realising this, users in all the major categories - academic, industry and hobbyist, will often run said software in a configuration where vulnerabilities …
Concurrent Algorithms under the hood of Kotlin Coroutines
Tutorials When: Sun 12 Oct 2025 14:00 - 15:30Sun 12 Oct 2025 16:00 - 17:30 People: Nikita Koval
… the Lincheck framework designed to test all … the problems we have faced when improving Kotlin Coroutines, present all …
Testing concurrent code on JVM with Lincheck
Tutorials When: Sun 12 Oct 2025 09:00 - 10:30Sun 12 Oct 2025 11:00 - 12:30 People: Evgenii Moiseenko, Nikita Koval
… in the Java standard library. All tasks run locally on attendees’ laptops. By the end …
A Programming Language for Feasible Solutions
SAS 2025 When: Tue 14 Oct 2025 15:00 - 15:20 People: Weijun Chen, Yuxi Fu, Huan Long
… equivalence property: All definable programs are guaranteed to run in polynomial time; Conversely, all problems solvable in polynomial time can be solved by some …
On a simple problem due to Yves Bertot
SAS 2025 When: Mon 13 Oct 2025 11:05 - 12:05 People: Olivier Danvy
… in elementary mathematics, but tackling it mobilizes all the growing cognitive …
Comparing the Precision of Abstract Operators in the eBPF Verifier using Differential Synthesis
SAS 2025 When: Tue 14 Oct 2025 14:40 - 15:00 People: Matan Shachnai, Harishankar Vishwanathan, Srinivas Narayana, Santosh Nagarakatte
… between two abstract operators across all valid abstract inputs. However, reasoning about all valid abstract inputs over-approximates what is actually reachable …
Enhancing Neural Network Robustness via Synthesis of Repair Programs
SAS 2025 When: Mon 13 Oct 2025 15:00 - 15:20 People: Tom Yuviler, Dana Drachsler Cohen
… , and others do not scale to deep networks. To mitigate all these shortcomings …
Ductape: Optimizing Dynamically Typed Programs using Ahead-of-Time Compilation and Data-Flow Analysis
SAS 2025 When: Tue 14 Oct 2025 11:45 - 12:05 People: Adi Harif, Shachar Itzhaky
… runtime at all. We have preliminary evidence with promising results showing that AOT …
Modular Reasoning about Error Bounds for Concurrent Probabilistic Programs
ICFP Papers When: Wed 15 Oct 2025 11:15 - 11:40 People: Kwing Hei Li, Alejandro Aguirre, Simon Oddershede Gregersen, Philipp G. Haselwarter, Joseph Tassarotti, Lars Birkedal
… examples and larger case studies.
All of the presented results, including …
Reasoning about Weak Isolation Levels in Separation Logic
ICFP Papers When: Wed 15 Oct 2025 14:55 - 15:20 People: Anders Alnor Mathiasen, Léon Gondelman, Léon Ducruet, Amin Timany, Lars Birkedal
… as proof that all of our specifications are realizable. All results …
Type Theory in Type Theory using a Strictified Syntax
ICFP Papers When: Tue 14 Oct 2025 14:30 - 14:55 People: Ambrus Kaposi, Loïc Pujet
… as metatheoretical functions. This has the effect of strictifying all the equations …
Multi-stage Programming with Splice Variables
ICFP Papers When: Mon 13 Oct 2025 14:55 - 15:20 People: Tsung-Ju Chiang, Ningning Xie
… a Kripke-style model, and prove adequacy results. All proofs have been
fully …
Almost Fair Simulations
ICFP Papers When: Mon 13 Oct 2025 16:50 - 17:15 People: Arthur Correnson, Iona Kuhn, Bernd Finkbeiner
… .
The simulation relations we present can all be equipped with intuitive …
Robust Dynamic Embedding for Gradual Typing
ICFP Papers When: Tue 14 Oct 2025 10:50 - 11:15 People: Koen Jacobs, Matías Toro, Nicolas Tabareau, Éric Tanter
… simply-typed language. All the results are formalized in the Rocq proof assistant …
Verified Interpreters for Dynamic Languages with Applications to the Nix Expression Language
ICFP Papers When: Wed 15 Oct 2025 14:05 - 14:30 People: Rutger Broekhoff, Robbert Krebbers
… based on deferred substitutions.</p>
<p>We mechanize all our …
Incremental and Unbounded Loop Analysis
Posters When: Thu 16 Oct 2025 18:00 - 20:00 People: Arpita Dutta, Joxan Jaffar
… all iterations, ie. to have unbounded verification. Failing this, our … all iterations. …
Towards a Theoretically-Backed and Practical Framework for Selective Object-Sensitive Pointer Analysis
OOPSLA When: Fri 17 Oct 2025 15:00 - 15:15 People: Chaoyue Zhang, Longlong Lu, Yifei Lu, Minxue Pan, Xuandong Li
… observed, all these research works are usually based on specific code patterns …, respectively. To note, our theory selects all heaps that improve precision, and our … flow graphs, enabling it to systematically capture all heaps that improve …
Faster Explicit-Trace Monitoring-Oriented Programming for Runtime Verification of Software Tests
OOPSLA When: Sat 18 Oct 2025 16:30 - 16:45 People: Kevin Guan, Marcelo d'Amorim, Owolabi Legunsen
… optimizations. First, whereas all existing online MOP algorithms eagerly monitor all … TraceMOP’s eager and wasteful synchronization of all accesses.
On 179 Java open … version, LazyMOP$^𝑒$ finds all pairs of method 𝑚 and spec 𝑠 …
RestPi: Path-Sensitive Type Inference for REST APIs
OOPSLA When: Fri 17 Oct 2025 14:45 - 15:00 People: Mark W. Aldrich, Kyla H. Levin, Michael Coblenz, Jeffrey S. Foster
… describe all response types, but automatically generating specifications …-constraints directly into a type system. This allows RestPi to enumerate all …
Notions of Stack-manipulating Computation and Relative Monads
OOPSLA When: Fri 17 Oct 2025 11:30 - 11:45 People: Yuchen Jiang, Runze Xue, Max S. New
… for embedded CBPV programming within a CBPV programming language. This means that all ….
All examples are executable in Zydeco, a stack-based functional language we …
Scaling Instruction-Selection Verification against Authoritative ISA Semantics
OOPSLA When: Sat 18 Oct 2025 11:45 - 12:00 People: Michael McLoughlin, Ashley Sheng, Chris Fallin, Bryan Parno, Fraser Brown, Alexa VanHattum
… specifications.
Our work verifies nearly all AArch64 instruction-selection rules reachable …: 60% of all specifications benefit from our automation, thereby requiring 2.6X …
Lexical Effect Handler: Fast by Design, Correct by Proof
Doctoral Symposium People: Cong Ma
… implementation and theory. Lexa outperforms existing compilers, and all techniques …
The Quest Toward that Perfect Compiler
SPLASH Keynotes When: Fri 17 Oct 2025 09:00 - 10:00 People: Zhendong Su
… Compilers are essential, foundational tools for engineering software. Indeed, we would all want to have a perfect compiler—one that is fully trustworthy and produces the best-performing code. This is a lofty goal and a long-standing …
Modal Effect Types
OOPSLA When: Sat 18 Oct 2025 10:45 - 11:00 People: Wenhao Tang, Leo White, Stephen Dolan, Daniel Hillerström, Sam Lindley, Anton Lorenzen
… Effect handlers are a powerful abstraction for defining, customising, and composing computational effects. Statically ensuring that all effect operations are handled requires some form of effect system, but using a traditional effect …
Symbolic MRD: Dynamic Memory, Undefined Behaviour, and Extrinsic Choice
OOPSLA When: Sat 18 Oct 2025 15:15 - 15:30 People: Jay Richards, Daniel Wright, Simon Cooksey, Mark Batty
… compilation mappings for atomics, and it matches all tests in the recently …
Universal Scalability in Declarative Program Analysis (with Choice-Based Combination Pruning)
OOPSLA When: Fri 17 Oct 2025 15:15 - 15:30 People: Anastasios Antoniadis, Ilias Tsatiris, Neville Grech, Yannis Smaragdakis
… evaluation is bottom-up, meaning that all inferences (from a set of initial facts) are performed and all their conclusions are outputs of the computation … for some inputs, due to the worst-case blowup of computing all results, even …
Pyrosome: Verified Compilation for Modular Metatheory
OOPSLA When: Fri 17 Oct 2025 17:15 - 17:30 People: Dustin Jamner, Gabriel Kammer, Ritam Nag, Adam Chlipala
… for all other cases. The novel enabling idea is an inductive formulation … equational theories, so all compiler-correctness proofs boil down to type-checking …, all while reusing the original theorems. We also present a linear version …
Float Self-Tagging
OOPSLA When: Thu 16 Oct 2025 11:15 - 11:30 People: Olivier Melançon, Manuel Serrano, Marc Feeley
… pointers entail a heap allocation of all float objects, and NaN/NuN-boxing puts … machine word. Such a transformation can only map a subset of all floats … eliminates heap allocation of nearly all floating-point numbers and provides good …
Software Stacks for Confidential Computing Hardware
SPLASH Keynotes When: Sat 18 Oct 2025 09:00 - 10:00 People: Frank Piessens
… is rapidly gaining traction in industry. All major hardware vendors have …
Automating maintenance of the Linux kernel: a perspective over 20 years
SPLASH Keynotes When: Thu 16 Oct 2025 09:00 - 10:00 People: Julia Lawall
… in thousands of kernel commits. However, not all software issues can be neatly …
FO-Complete Program Verification for Heap Logics
OOPSLA When: Sat 18 Oct 2025 10:30 - 10:45 People: Adithya Murali, Hrishikesh Balakrishnan, Aaron Councilman, P. Madhusudan
… We develop the first two heap logics that have implicit heaplets and that admit FO-complete program verification. The notion of FO-completeness is a theoretical guarantee that all theorems that are valid when recursive definitions …
Destination calculus: A linear λ-calculus for purely functional memory writes
OOPSLA When: Sat 18 Oct 2025 14:00 - 14:15 People: Thomas BAGREL, Arnaud Spiwack
… calculus subsumes all the similar systems, and can be used to reason about …
Dynamic Wind for Effect Handlers
OOPSLA When: Fri 17 Oct 2025 14:30 - 14:45 People: David Voigt, Philipp Schuster, Jonathan Immanuel Brachthäuser
… Effect handlers offer an attractive way of abstracting over effectful computation. Moreover, languages with effect handlers usually statically track effects, which ensures the user is aware of all side effects different parts of a program …
Type-Preserving Flat Closure Optimization
OOPSLA When: Fri 17 Oct 2025 15:15 - 15:30 People: Adam Geller, Sean Bocirnea, Chester Gould, Paulette Koronkevich, William J. Bowman
… ) that admits all these optimizations, prove type safety and subject reduction …
Revamping Verilog Semantics for Foundational Verification
OOPSLA When: Sat 18 Oct 2025 14:45 - 15:00 People: Joonwon Choi, Jaewoo Kim, Jeehoon Kang
… of a pipelined RISC-V processor’s functional correctness and progress guarantees. All …
A complete formal semantics of eBPF instruction set architecture for Solana
OOPSLA When: Fri 17 Oct 2025 13:45 - 14:00 People: Shenghao Yuan, Zhuoruo Zhang, Jiayi Lu, David Sanan, Rui Chang, Yongwang Zhao
… We present the first and most comprehensive formal semantics for the Solana eBPF bytecode language used in smart contracts on the Solana blockchain platform. Our formalization accurately captures all binary-level instructions of the Solana …
Active Learning for Neurosymbolic Program Synthesis
OOPSLA People: Celeste Barnaby, Jocelyn Qiaochu Chen, Ramya Ramalingam, Osbert Bastani, Işıl Dillig
… proposed method iteratively makes CCE more precise until all remaining programs …
qblaze: An Efficient and Scalable Sparse Quantum Simulator
OOPSLA When: Sat 18 Oct 2025 11:45 - 12:00 People: Hristo Venev, Thien Udomsrirungruang, Dimitar Dimitrov, Timon Gehr, Martin Vechev
… and highly-scalable algorithms for all quantum operations.
Our extensive experimental …
A Flow-Sensitive Refinement Type System for Verifying eBPF Programs
OOPSLA When: Fri 17 Oct 2025 16:00 - 16:15 People: Ameer Hamza, Lucas Zavalia, Arie Gurfinkel, Jorge A. Navas, Grigory Fedyukovich
… requires all programs to be verified before deploying them inside the kernel …
Automated Discovery of Tactic Libraries for Interactive Theorem Proving
OOPSLA When: Thu 16 Oct 2025 10:30 - 10:45 People: Yutong Xin, Jimmy Xin, Gabriel Poesia, Noah D. Goodman, Jocelyn Qiaochu Chen, Işıl Dillig
… $\times$ as many tactics as Peano and reduces the size of proofs by 26% across all …
Translation Validation for LLVM's AArch64 Backend
OOPSLA When: Fri 17 Oct 2025 17:00 - 17:15 People: Ryan Berger, Mitch Briles, Nader Boushehrinejad Moradi, Nicholas Coughlin, Kait Lam, Nuno P. Lopes, Stefan Mada, Tanmay Tirpankar, John Regehr
… , with all of the correctness hazards entailed by a million lines of intricate C …
Liberating Merges via Apartness and Guarded Subtyping
OOPSLA When: Thu 16 Oct 2025 11:30 - 11:45 People: Han Xu, Xuejing Huang, Bruno C. d. S. Oliveira
… {extensible records}, and \emph{nested composition} all at once in a single …
Exploring the Theory and Practice of Concurrency in the Entity-Component-System Pattern
OOPSLA When: Thu 16 Oct 2025 16:15 - 16:30 People: Patrick Redmond, Jonathan Castello, Jose Calderon, Lindsey Kuper
… frameworks and find that they all leave opportunities for deterministic concurrency …
Fast Client-Driven CFL-Reachability via Regularization-Based Graph Simplification
OOPSLA When: Fri 17 Oct 2025 10:30 - 10:45 People: Chenghang Shi, Dongjie He, Haofeng Li, Jie Lu, Lian Li, Jingling Xue
… employs a regular approximation to ensure exact reachability results for all …
Qualified Types with Boolean Algebras
OOPSLA When: Fri 17 Oct 2025 14:30 - 14:45 People: Edward Lee, Jonathan Lindegaard Starup, Ondřej Lhoták, Magnus Madsen
… to eliminate all effect upcasts present in the current Flix Standard Library …
Finch: Sparse and Structured Tensor Programming with Control Flow
OOPSLA When: Thu 16 Oct 2025 16:30 - 16:45 People: Willow Ahrens, Teodoro F. Collin, Radha Patel, Kyle Deeds, Changwan Hong, Saman Amarasinghe
… From FORTRAN to NumPy, tensors have revolutionized how we express computation. However, tensors in these, and almost all prominent systems, can only handle dense rectilinear integer grids. Real world tensors often contain underlying …
The Power of Regular Constraint Propagation
OOPSLA When: Thu 16 Oct 2025 15:15 - 15:30 People: Matthew Hague, Artur Jez, Anthony Widjaja Lin, Oliver Markgraf, Philipp Ruemmer
… concatenation, replace, and almost all flavors of string transductions. We …
Non-interference Preserving Optimising Compilation
OOPSLA When: Thu 16 Oct 2025 16:45 - 17:00 People: Julian Rosemann, Sebastian Hack, Deepak Garg
… be handled in a very limited and less modular way (if at all) by existing approaches …
A Mechanized Semantics for Dataflow Circuits
OOPSLA When: Fri 17 Oct 2025 14:15 - 14:30 People: Tony Law, Delphine Demange, Sandrine Blazy
… of circuits executions: all possible schedules of such circuits lead to a unique …
QbC: Quantum Correctness by Construction
OOPSLA When: Sat 18 Oct 2025 11:30 - 11:45 People: Anurudh Peduri, Ina Schaefer, Michael Walter
… programs using proof systems such as quantum Hoare logic. All these prior …
HpC: A Calculus for Hybrid and Mobile Systems
OOPSLA When: Fri 17 Oct 2025 11:15 - 11:30 People: Xiong Xu, Jean-Pierre Talpin, Shuling Wang, Bohua Zhan, Xinxin Liu, Naijun Zhan
… , while allowing to lift all theoretical results (e.g. bisimulation) to the context …
Binary Cryptographic Function Identification via Similarity Analysis with Path-insensitive Emulation
OOPSLA When: Thu 16 Oct 2025 10:45 - 11:00 People: Yikun Hu, Yituo He, Wenyu He, Haoran Li, Yubo Zhao, Shuai Wang, Dawu Gu
… the emulated values are all represented as intervals. As such, it is able to analyze every …
Semantics of Sets of Programs
OOPSLA When: Fri 17 Oct 2025 15:00 - 15:15 People: Jinwoo Kim, Shaan Nagy, Thomas Reps, Loris D'Antoni
… Applications like program synthesis sometimes require proving that a property holds for all of the infinitely many programs described by a grammar—i.e., an inductively defined set of programs. Current verification frameworks …
Products of Recursive Programs for Hypersafety Verification
OOPSLA When: Sat 18 Oct 2025 17:00 - 17:15 People: Ruotong Cheng, Azadeh Farzan
… composition of individual recursive programs includes all possible alignments from …
ABC: Towards a Universal Code Styler through Model Merging
OOPSLA When: Thu 16 Oct 2025 10:30 - 10:45 People: Yitong Chen, Zhiqiang Gao, Chuanqi Shi, Baixuan Li, Miao Gao
… all model sizes in both basis and combination style transformations …
Work Packets: A New Abstraction for GC Software Engineering, Optimization, and Innovation
OOPSLA When: Sat 18 Oct 2025 17:15 - 17:30 People: Wenyu Zhao, Stephen M. Blackburn, Kathryn S McKinley
… . The design simplifies and unifies all GC tasks into work packets which define … dependencies, e.g. all mutators must stop before copying any objects. Fully parallel …
Verifying Asynchronous Hyperproperties in Reactive Systems
OOPSLA People: Raven Beutner, Bernd Finkbeiner
… traversal on traces, i.e., all traces are evaluated \emph{synchronously …
Complete the Cycle: Reachability Types with Expressive Cyclic References
OOPSLA People: Haotian Deng, Siyuan He, Songlin Jia, Yuyan Bao, Tiark Rompf
… reference tracking, where a reference’s qualifier must include all transitively …
Scalable Equivalence Checking and Verification of Shallow Quantum Circuits
OOPSLA When: Sat 18 Oct 2025 15:00 - 15:15 People: Nengkun Yu, Xuan Du Trinh, Thomas Reps
… is the unique quantum state that satisfies all the constraints. Beyond equivalence …
Mini-Batch Robustness Verification of Deep Neural Networks
OOPSLA When: Sat 18 Oct 2025 14:30 - 14:45 People: Saar Tzour-Shaday, Dana Drachsler Cohen
… , and verifies them jointly. If a mini-batch is verified, all inputs are proven …
Verification of Bit-Flip Attacks against Quantized Neural Networks
OOPSLA When: Sat 18 Oct 2025 12:00 - 12:15 People: Yedi Zhang, Lei Huang, Pengfei Gao, Fu Song, Jun Sun, Jin Song Dong
… designed to formally verify the absence of bit-flip attacks or to identify all …
(TOPLAS) Polynomial Bounds of CFLOBDDs against BDDs
OOPSLA When: Sat 18 Oct 2025 16:00 - 16:15 People: Xusheng Zhi, Thomas Reps
… for which, for all , the CFLOBDD for (using a particular variable order …
MIO: Multiverse Debugging in the face of Input/Output
OOPSLA When: Fri 17 Oct 2025 16:15 - 16:30 People: Tom Lauwaerts, Maarten Steevens, Christophe Scholliers
… non-deterministic programs by allowing programmers to explore all potential …
Quantization with Guaranteed Floating-Point Neural Network Classifications
OOPSLA When: Thu 16 Oct 2025 17:00 - 17:15 People: Anan Kabaha, Dana Drachsler Cohen
… high degree of nonlinearity, over all possible inputs. We propose CoMPAQt …
Tunneling Through the Hill: Multi-Way Intersection for Version-Space Algebras in Program Synthesis
OOPSLA When: Sat 18 Oct 2025 13:45 - 14:00 People: Guanlin Chen, Ruyi Ji, Shuhao Zhang, Yingfei Xiong
… only a few programs can pass all examples. Utilizing this observation, we …
Finding Compiler Bugs through Cross-Language Code Generator and Differential Testing
OOPSLA When: Fri 17 Oct 2025 16:45 - 17:00 People: Qiong Feng, Xiaotian Ma, Ziyuan Feng, Marat Akhin, Wei Song, Peng Liang
… in the Java compiler. Among all mutators, TypeChanger is the most effective …
Automatically Verifying Replication-aware Linearizability
OOPSLA When: Fri 17 Oct 2025 16:15 - 16:30 People: Vimala Soundarapandian, Kartik Nagar, Aseem Rastogi, KC Sivaramakrishnan
… linearizability is one such specification, which requires all replicas …
Efficient Abstract Interpretation via Selective Widening
OOPSLA When: Sat 18 Oct 2025 16:30 - 16:45 People: Jiawei Wang, Xiao Cheng, Yulei Sui
… operations and fixpoint detection uniformly across all variables …
An Empirical Study of Bugs in the rustc Compiler
OOPSLA When: Thu 16 Oct 2025 16:00 - 16:15 People: Zixi Liu, Yang Feng, Yunbo Ni, Shaohua Li, Xizhe Yin, Qingkai Shi, Baowen Xu, Zhendong Su
… the safety and correctness of all Rust programs, as compiler bugs can silently …
Syntactic Completions with Material Obligations
OOPSLA When: Fri 17 Oct 2025 11:45 - 12:00 People: David Moon, Andrew Blinn, Thomas J. Porter, Cyrus Omar
… be parsed into a well-formed term, with success guaranteed over all inputs. We …
Modular Reasoning about Global Variables and Their Initialization
OOPSLA When: Thu 16 Oct 2025 14:45 - 15:00 People: João Pereira, Isaac van Bakel, Patricia Firlejczyk, Marco Eilers, Peter Müller
… of a class, while in Go, the order depends on all packages of a program …
Statically Analyzing the Dataflow of R Programs
OOPSLA When: Fri 17 Oct 2025 11:15 - 11:30 People: Florian Sihler, Matthias Tichy
… correctly analyze almost all programs in our equivalence test suite, preserving …
Bennet: Randomized Specification Testing for Heap-Manipulating Programs
OOPSLA When: Fri 17 Oct 2025 16:00 - 16:15 People: Zain K Aamer, Benjamin C. Pierce
… in this setting must craft all their own generators by hand, rather than letting …
Interactive Bit Vector Reasoning using Verified Bitblasting
OOPSLA When: Sat 18 Oct 2025 16:45 - 17:00 People: Henrik Böving, Siddharth Bhat, Alex Keizer, Luisa Cicolini, Leon Frenot, Abdalrhman Mohamed, Leo Stefanesco, Harun Khan, Josh Clune, Clark Barrett, Tobias Grosser
… supports all operations (with reasoning principles) for the SMT-LIB 2.7 standard …
Fuzzing C++ Compilers via Type-Driven Mutation
OOPSLA When: Fri 17 Oct 2025 14:15 - 14:30 People: Bo Wang, Chong Chen, Ming Deng, Junjie Chen, Xing Zhang, Youfang Lin, Dan Hao, Jun Sun
… test oracles for nearly 80% of all generated programs. TyMut uncovered 102 bugs …
Fray: An Efficient General-Purpose Concurrency Testing Platform for the JVM
OOPSLA When: Fri 17 Oct 2025 14:00 - 14:15 People: Ao Li, Byeongjee Kang, Vasudev Vikram, Isabella Laybourn, Samvid Dharanikota, Shrey Tiwari, Rohan Padhye
… locking_ for faithfully expressing the set of all possible program behaviors …
Advancing Performance via a Systematic Application of Research and Industrial Best Practice
OOPSLA When: Thu 16 Oct 2025 11:45 - 12:00 People: Wenyu Zhao, Stephen M. Blackburn, Kathryn S McKinley, Man Cao, Sara S. Hamouda
… and uptime requirements. We address all of the limitations identified …