Upstate
Programming Languages
Seminar

Dynamic languages defer type checking to runtime, enabling flexibility but leaving type errors undetected until execution. Static type systems catch errors early but are overly conservative, rejecting programs that would execute safely. Existing approaches either cannot simultaneously provide static safety guarantees and precise refutation of erroneous programs, or do so only at the cost of significant annotation burden and type-checking overhead.

We propose a type system with three contributions: (1) a modal type abstraction classifying terms as definitely safe, possibly crashing, or definitely crashing; (2) tabular types, which unify sufficiency and necessity analyses in a single framework, structured analogously to database tables and composed via joins; and (3) a type compression mechanism trading precision for simplicity. Together, these allow the system to refute more erroneous programs while preserving the guarantee that well-typed programs cannot go wrong.

Floating-point exceptions - including Not-a-Number, infinity, and division by zero present significant challenges to GPU-accelerated programs. These exceptions can silently propagate the programs leading to inaccurate results that might go unnoticed. Existing tools like FPChecker and GPU-FPX detect these exceptions dynamically but pose a significant runtime overhead making them impractical for large-scale GPU applications.

We propose a probabilistic static analysis framework that instruments only the floating-point instructions most likely to produce exceptional values. We explore two different ways to selectively instrument instructions directly from compiled SASS code: an instruction-level analysis (ILA) that derives probability from IEEE 754 bit pattern semantics and a data-flow propagation analysis that derives the propagated probability along data dependencies within the basic blocks. We are evaluating our framework across a suite of CUDA benchmarks comparing our reduced instrumentation against the full dynamic instrumentation in GPU-FPX as ground truth. This talk will present the framework, early results, and the challenges we are still working through in selecting the thresholds and making sure we don't miss real exceptions.

Bounding floating-point roundoff error is important for many mathematical and scientific programs. However, it is challenging to develop scalable and precise techniques for automatically verifying floating-point roundoff error. The Numerical Fuzz language and type system offers a compositional and performant approach to automated numerical analysis, but it lacks support for negative numbers and subtraction.

To address this problem, we define a novel paired model for Numerical Fuzz supporting floating-point programs with negative numbers and subtraction. We derive rigorous roundoff error bounds from our types by combining the error bounds in our paired model with a modular interval-style bound analysis. To perform our bound analysis, we extend our type system with bound annotations and bound polymorphism. To reduce the user annotation burden, we develop a sound type inference algorithm that can infer types tracking numerical error, as well as instances of bound polymorphism. Additionally, we introduce a new primitive to more precisely reason about the combination of rounded computations under addition, and use the primitive to achieve tighter error bounds.

We implement our approach and show that it is significantly faster than existing methods for floating-point error analysis, sometimes by orders of magnitude, while giving useful error bounds that are competitive with state-of-the-art tools.

We are proposing a new logical language for applied ontology modeling and querying, that would compete with the current standards OWL and SPARQL. The current standard fails to respect the open-world assumption, since the SPARQL queries are closed-world, and the modeling language OWL is unable to express the negation connective. Instead, our new language addresses this issue with a intuitionistic Kripke semantics with special negative relations to avoid undecidability. Moreover, we started to substitute the set-theoretic framework of OWL with a type-theoretic approach, which gains the functionalities of a type-checker for taxonomical reasoning and for checking the semantic malformedness of queries at compile time, against the current run time standard. Future work consists in implementing this new logic into a Datalog extension.

In this talk, I will introduce work towards on-disk query evaluation in the Draupnir datalog engine. Evaluation of query languages like datalog is typically implemented through pipelined operators: functions that operate over collections of records. To improved memory locality, operator implementations are typically designed to communicate at the granularity of individual records. However, because certain "blocking" operators, like joins, need visibility over the entire collection, it is common for operator implementations to materialize their inputs.

Implementing materialization purely in the operator leaves this complex task opaque to the runtime, vastly simplifying runtime implementation. However doing so also precludes global optimizations at compile time (e.g., materialization sharing), or at runtime (dynamic memory allocation, and co-scheduling IO and compute). Although prior work has explored how to implement these optimizations in classical runtimes, these efforts invariably create leaks in the operator abstraction. In this talk, I will present a new "flow-oriented" query evaluation abstraction, implemented in Draupnir, and show how it enables both static and dynamic optimization of query evaluation.

This is joint work with the Draupnir team.

Optimizing memory locality remains a critical challenge in high-performance computing, where non-contiguous data access and complex loop structures heavily degrade cache performance. While loop tiling is widely used to improve data reuse, evaluating and tuning tiling parameters symbolically at compile time remains challenging.

In this talk, we introduce SALT (Symbolic Analysis of Loop Tiling), a framework that performs symbolic analysis on tiled loops to optimize memory locality. By symbolically modeling loop iteration spaces and data reuse patterns, SALT enables static cache performance predictions without relying solely on heuristic dynamic profiling. We will discuss the underlying symbolic formulation, implementation considerations, and preliminary results demonstrating how SALT helps guide loop transformations for efficient memory behavior.

Effective inseparability is a well-established technique for proving undecidability. We formalize this technique in Rocq, building on the coq-synthetic-computability and coq-library-undecidability libraries, proving that effective inseparability of a pair of sets implies creativity of each, and that creative sets are Σ₀¹-complete. This gives a reusable interface for proving undecidability of arbitrary problems via reduction, using Markov's principle rather than the excluded middle throughout.

We apply this technique to a recently proven result: Kleene algebras with partial commutativity conditions have an undecidable equational theory (in contrast to fully commutative Kleene algebras, whose equational theory is decidable). The talk focuses on the formalization of the effective inseparability proof and our ongoing work reducing terms in this theory to 2-counter machines, and from there to effectively inseparable sets, without Gödel-numbered encodings.

The interactions between staged code quotations and module systems are notoriously subtle. Unfortunately, the difficulty of incorporating quotations into a modular language poses a serious barrier to adoption. This talk will examine mixed-leveledness as a key culprit for these challenges; modules unlike terms can contain bindings at different levels, which disturbs the standard assumption of staging calculi that all things can be assigned a single level. We will then present a novel higher-order, mixed-level calculus, where products may combine components of different levels, reflecting the different kinds of functions in a multi-stage language. Expressivity, compilation, and other desiderata for a staging language will also be discussed.

Many now believe that "code generation" productivity is a solved problem. With that achieved, emphasis has shifted to other properties of the code like correctness and performance. While there exists a rich theory of program correctness, attempts to rigorously reason about program performance remain limited. Arguably, the most significant progress on program performance has been the so-called "throughput" models now in use in many compilers. These still remain fairly primitive.

We will present our approach using operational analysis of queueing networks to analyze the performance of GPU kernels. Grounded in queueing theory, this approach allows us to reason about program performance rigorously and shape how programming languages can support performant programming, including through automated analyses that prevent programmers from writing slow code.

In this talk, we will present a technique for embedding a statically typed programming library into an ordinary context-free grammar (CFG). Given such a library and a reference compiler, the method we describe constructs a CFG denoting the language of well-typed expressions. This CFG models types as nonterminals, typing judgments as productions, and invocations, member accesses, and identifiers as terminals. The resulting grammar generates well-typed call chains over the target library and may be consumed by standard parsing, enumeration, synthesis, or language-modeling tools.

Our construction is effectively a resource-bounded monomorphization. We instantiate candidate productions with monomorphic type signatures over a finite set of ground types, and using the reference compiler as a typing oracle, check each candidate production for type safety. The resource bounds are user-defined parameters, e.g., function arity, type parameter nesting depth, subtyping depth, and the number of ground types. We then enumerate all combinatorial possibilities from this configuration space, yielding an CFG whose construction is fixed-tractable in the selected region.

The generated language will be a sound under-approximation of the well-typed expressions and complete relative to the ground-type universe and structural bounds. It is incomplete precisely where the chosen bounds truncate the type universe; under a sufficiently representative ground universe and practical resource limits, the grammar captures most well-typed expressions of interest. This approach allows us to treat type safety as CFL recognition and provides a compact representation for sampling, fuzzing, and constrained decoding, while preserving the essential structure of the host type system.

This project builds on prior work by Considine '25 (see: https://arxiv.org/pdf/2512.01036)

Complex P4 applications increasingly rely on in-switch stateful structures to implement functionalities such as aggregation and load balancing. However, existing P4 test generators based on symbolic execution only reason about one packet at a time, making them unable to expose stateful bugs whose feasibility depends on cross-packet state evolution.

In this talk, I will present the current progress of my Ph.D. research on extending symbolic execution to support multi-packet reasoning when generating tests for stateful P4 programs. My work models stateful data structures symbolically, summarizes the effects of individual packet executions, and composes these summaries into executable packet sequences that drive the program through the state-dependent decisions leading to incorrect states. Consequently, generated executable packet sequences would exercise those incorrect states and expose state-dependent bugs. I will discuss the design challenges encountered in building such a system, share current experimental results. Finally, I will discuss one promising direction for future work: exploring automated program repair for P4 programs.

Profiling gets the dynamic execution count of each basic block of a running program, but due to runtime instrumentation has high overheads hindering its application. We propose symbolic basic block profiling which gets the same result as traditional profiling while being much cheaper and faster. Our key insight is that many programs contain highly structured loops whose execution is statically analyzable. Therefore, unlike traditional instrumentation-based profiling technique which insert counters inside loops, our technique analyzes the loop structure to derive a reusable formula that can be statically evaluated based on input sizes to get basic block counts. Thus, we can obtain basic block counts without executing the program. We currently target on ML programs which contain regular program structures that are amenable to our technique.

In this talk, we will introduce the design of our symbolic analysis, including a graph language designed to help build symbolic formulae of basic block counts and the corresponding syntax-directed interpretation. We will also present the evaluation of our proposed technique on 78 TVM ML kernels. Our method shows over 100X speedup over LLVM PGO instrumentation pass in profiling the 78 ML kernels.

Cryptographic protocol verification in the symbolic model in the style of Dolev and Yao has seen significant advances lately. Tools such as ProVerif, Tamarin, and DY* have seen tremendous success in proving various trace properties of various complex and layered protocol designs. While trace properties has been a success story, the other big class of properties, namely the hyperproperties, has not seen much development in the symbolic model. Current tools can only verify elementary protocols with various restrictions on the protocol code.

We extend Cryptis, a separation logic built on top of the Iris framework to reason about symbolic cryptography, to the hyperproperty setting. We show the IND-CPA game implemented using this 'relational Cryptis'. We then sketch how relational Cryptis might be used in the verification of larger protocols and how such code and their proofs might compose within relational Cryptis, and with other logics built on top of Iris.

In this talk, we present a new automated approach capable of both proving and refuting properties of functional programs. We rely on symbolic execution to explore the program's behavior. Symbolic execution “runs” a program with symbolic variables, generating symbolic states that follow each possible branching path. We make use of an approximation check, which allows the symbolic execution engine to discard paths that would redundantly re-explore pieces of the search space. This enables automated verification of certain program properties, including properties with unbounded recursion.

We introduce a new technique, reversible abstractions, which enhances the effectiveness of approximation checking, allowing more pairs of states to be found equivalent. We practically implement our approach in a tool, Nova, and evaluate its effectiveness when both verifying true properties and refuting false properties on a combination of pre-existing and newly crafted benchmarks. We find that Nova is successful at verifying true properties and very successful at refuting false properties.