Typing Fallback Functions: A Semantic Approach to Type Safe Smart Contracts
Publisher Copyright: © Stian Lybech, Daniele Gorla, and Luca Aceto.
14,842 papers · page 11 of 743
Verifying Wait-Freedom for Concurrent Higher-Order Programs
Wait-freedom is the strongest non-blocking progress guarantee for concurrent data structures, ensuring that every operation completes in a finite number of steps regardless of interference from other threads. While verification of wait-freedom has been studied for first-order lan…
Foundational and Compositional Verification of Layered Concurrent Objects
Compositionality is essential for managing complexity in verification of concurrent programs, especially when proof certificates are needed. An effective verification scheme is to divide programs into abstraction layers and verify by composing refinements between layers. However,…
Faster Verified Explanations for Neural Networks
Verified explanations are a principled way to explain the decisions taken by neural networks, which are otherwise black-box in nature. However, these techniques face significant scalability challenges, as they require multiple calls to neural network verifiers, each of them with …
Meaningful Human-in-the-Loop Checking of GenAI Synthesis for Restricted Languages
Developers routinely use GenAI tools (large language models enriched in various ways) to generate useful components of programs, such as regular expressions. While pleasant and often effective, this can easily lead to subtle bugs. The developer may have been unclear in their spec…
Scaling Bottom-Up IFDS Taint Analysis with Optimized Data-Flow Encoding
Static taint analysis is an important technique for bug-finding and vulnerability detection on source-code. One commonly used technique to solve inter-procedural taint analysis problems is the well-studied Interprocedural Finite Distributive Subsets (IFDS) algorithm. However, whe…
Optimizing Record/Replay Through Relaxed Total Ordering and Multi-Version eXecution
Record/Replay (RR) allows developers to record an execution and then replay it exactly as it was recorded. RR enables deterministic replay of non-deterministic behaviors in a different environment than the one used for the recording, which can capture complex bugs in production a…
Automatic Code and Test Generation of Smart Contracts from Coordination Models
We propose a formal approach for specifying and implementing decentralised coordination in distributed systems, with a focus on smart contracts. Our model captures dynamic roles, data-driven transitions, and external coordination interfaces, enabling high-level reasoning about de…
Proof-of-Theft: Dynamic Graph-Based Fingerprinting of In-Browser Cryptomining
The decentralized and unregulated nature of cryptocurrencies, combined with their monetary value, has made them a vehicle for various illicit activities. One such activity is cryptojacking, an attack that uses stolen computing resources to mine cryptocurrencies without consent fo…
A Variation on Java Wildcards - Trading Expressiveness for Global Type Inference
In standard Java, wildcards behave like existential types: they must be opened before use in a method invocation, a process the compiler performs implicitly via capture conversion. We present Java-TX, a dialect of Java that sidesteps this existential encoding and treats wildcards…
Remote Concolic Multiverse Debugging
Debugging nondeterministic programs is inherently difficult, particularly in microcontroller environments where execution paths can diverge unpredictably due to external sensor inputs. Traditional debugging techniques often fail to capture or reproduce this nondeterministic behav…
Compile-Time Tensor Shape Checking via Staged Shape-Dependent Types
When writing programs involving matrices or tensors in general, it is desirable to rule out the inconsistency of tensor shapes (i.e., the generalization of matrix sizes) before actual computation. For this purpose, some languages provide dependent types such as Mat m n, and other…
DelExp: A Relational Container Abstraction: with Applications to Compositional Analysis
Data containers, such as lists, arrays, trees, etc, raise challenges for program verification. In static analysis by abstract interpretation, one popular approach is summarization: multiple elements of a data structure are abstracted into a single one, favoring performance over p…
Front Matter, Table of Contents, Preface, Conference Organization
Front Matter, Table of Contents, Preface, Conference Organization
Specifying and Verifying RDMA Synchronisation
Remote direct memory access (RDMA) allows a machine to directly read from and write to the memory of remote machine, enabling high-throughput, low-latency data transfer. Ensuring correctness of RDMA programs has only recently become possible with the formalisation of rdmatso sema…
Contextual Metaprogramming for Session Types
We propose the integration of staged metaprogramming into a session-typed message passing functional language. We build on a model of contextual modal type theory with multi-level contexts, where contextual values, closing arbitrary terms over a series of variables, may be boxed …
In Cantor Space No One Can Hear You Stream
Abstract We revisit the famous notion of sheaves through the lens of type theory and side-effects. Using the language of $$\textsf{MLTT}$$ MLTT , we show that they inductively approximate idealized functional objects as decision trees, realizing a generalized form of continuity. …
Deciding not to Decide - Sound and Complete Effect Inference in the Presence of Higher-Rank Polymorphism
Type-and-effect systems help the programmer to organize data and computational effects in a program. While for traditional type systems expressive variants with sophisticated inference algorithms have been developed and widely used in programming languages, type-and-effect system…
Recursive Logical Relations for Intuitionistic Linear Logic Session Types
Abstract Program equivalence is the heart of reasoning about and proving properties of programs. To assert noninterference, for example, a program is shown to be equivalent to itself up to the confidentiality level of an observer. A powerful enabler for such proofs are logical re…
Code Generation via Meta-programming in Dependently Typed Proof Assistants
Abstract Dependently typed proof assistants offer powerful meta-programming features, which allow users to implement proof automation or compile-time code generation. This paper surveys meta-programming frameworks in Rocq, Agda, and Lean, with seven implementations of a running e…