title: Flow-Graph-Aware Tiling and Rescheduling for Memory-Efficient On-Device Inference

authors:
Yeonoh Jeong
Taehyeong Park
Yongjun Park

abstract: With the increasing popularity of artificial intelligence (AI) applications, deep neural networks (DNNs) are in demand for on-device serving in various real-life fields. Running DNN inference on a resource-constrained edge device requires aggressive memory optimization. While several recent tiling-based techniques reduce peak memory usage by partitioning large tensors into micro-tensors, they are specialized for the MCU environment and do not provide scalability to various edge platforms. Moreover, they greedily search for the target of tiling without considering the memory flow across the model while partitioning. In this paper, we propose OKO, a compiler-based optimization technique that minimizes peak memory usage by considering both tiling and the corresponding operation rescheduling. OKO estimates the memory savings from the tiling method based on the lifetime and dependencies of the tensor, and then algorithmically selects the optimal tiling strategy. It further maximizes the reuse of memory spaces by efficiently reordering operations and immediately releasing unnecessary tensors. Evaluations on various edge devices show that OKO achieves effective memory savings of up to 80% and an average of 59% with no loss of accuracy and negligible overhead, supporting memory-efficient inference across a broad range of target devices.


venue: cgo

title: PIP: Making Andersen's Points-to Analysis Sound and Practical for Incomplete C Programs

authors:
Håvard Rognebakke Krogstie
Helge Bahmann
Magnus Själander
Nico Reissmann

abstract: Compiling files individually lends itself well to parallelization, but forces the compiler to operate on incomplete programs. State-of-the-art points-to analyses guarantee sound solutions only for complete programs, requiring summary functions to describe any missing program parts. Summary functions are rarely available in production compilers, however, where soundness and efficiency are non-negotiable. This paper presents an Andersen-style points-to analysis that efficiently produces sound solutions for incomplete C programs. The analysis accomplishes soundness by tracking memory locations and pointers that are accessible from external modules, and efficiency by performing this tracking implicitly in the constraint graph. We show that implicit pointee tracking makes the constraint solver 15× faster than any combination of five different state-of-the-art techniques using explicit pointee tracking. We also present the Prefer Implicit Pointees (PIP) technique that further reduces the use of explicit pointees. PIP gives an additional speedup of 1.9×, compared to the fastest solver configuration not benefiting from PIP. The precision of the analysis is evaluated in terms of an alias-analysis client, where it reduces the number of MayAlias-responses by 40% compared to LLVM’s BasicAA pass alone. Finally, we show that the analysis is scalable in terms of memory, making it suitable for optimizing compilers in practice.


title: VFlatten: Selective Value-Object Flattening using Hybrid Static and Dynamic Analysis

authors:
Arjun H. Kumar
Bhavya Hirani
Hang Shao
Tobi Ajila
Vijay Sundaresan
Daryl Maier
Manas Thakur

abstract: Object flattening is a non-trivial optimization that inlines the fields of an object inside its containers. Owing to its direct applicability for immutable objects, Java would soon allow programmers to mark compatible classes as "value types", and Java Virtual Machines (JVMs) to transparently flatten their instances (value objects). Expectations include reduced memory footprint, faster field access, and overall improvement in performance. This paper describes the surprises and challenges we faced while experimenting with value types and object flattening on a real-world JVM, and presents the design of an efficient strategy that selectively flattens profitable value objects, using a novel combination of static and dynamic analyses.Our value-object flattening strategy is based on insights that span the source program, the just-in-time (JIT) compiler employed by the JVM, as well as the underlying hardware. The first insight identifies source-level patterns that favour and oppose value-object flattening. The second insight finds an interesting dependence of object flattening on object scalarization, and estimates the capability of the JIT in avoiding overheads using escape analysis. Finally, the third insight correlates container objects with cache-line size, based on the load semantics of object fields. In order to develop an efficient strategy to flatten potentially profitable objects, we capture these insights in a tool called VFLATTEN that uses a novel combination of static and dynamic analyses and flattens value objects selectively in a production Java runtime.


title: Compiler-Runtime Co-operative Chain of Verification for LLM-Based Code Optimization

authors:
Hyunho Kwon
Sanggyu Shin
Ju Min Lee
Hoyun Youm
Seungbin Song
Seongho Kim
Hanwoong Jung
Seungwon Lee
Hanjun Kim

abstract: Large Language Models (LLMs) have recently shown promise in compiler optimizations such as loop vectorization and memory access restructuring. However, due to their generative nature, LLM-optimized code may contain syntax errors or semantic inconsistencies. While state-of-the-art compilers using LLMs employ symbolic verification to ensure correctness, they fail to fully utilize LLM-based optimizations due to the limited and unreliable verification coverage. This work introduces CoV, a compiler-runtime co-operative Chain of Verification framework that safely integrates LLM-based code transformations into modern compilation workflows. CoV employs a multi-stage verification pipeline that begins with lightweight static checks such as syntax validation and profiling-based checksum filtering, and then applies symbolic equivalence verification using tools like Alive2. For code fragments that cannot be statically verified, CoV inserts runtime verification mechanisms to ensure correctness during execution. These runtime checks are optimized through verification parallelization and batching to minimize overhead. This work implements a prototype CoV framework atop an LLM-based automatic vectorizer within LLVM, and evaluates it using 151 loops in the TSVC benchmark suite and three realistic applications. CoV expands vectorization coverage by 13.9% and 10.6% over LLVM and GCC -O3 vectorization, respectively. In addition, CoV successfully vectorizes loops in three realistic applications that are not handled by the -O3 vectorization.


title: GRANII: Selection and Ordering of Primitives in GRAph Neural Networks using Input Inspection

authors:
Damitha Lenadora
Vimarsh Sathia
Gerasimos Gerogiannis
Serif Yesil
Josep Torrellas
Charith Mendis

abstract: Over the years, many frameworks and optimization techniques have been proposed to accelerate graph neural networks (GNNs). In contrast to the optimizations explored in these systems, we observe that different matrix re-associations of GNN computations lead to novel input-sensitive performance behavior. We leverage this observation to propose GRANII, a system that exposes different compositions of sparse and dense matrix primitives based on different matrix re-associations of GNN computations and selects the best among them based on input attributes. GRANII executes in two stages: (1) an offline compilation stage that enumerates all valid re-associations leading to different sparse-dense matrix compositions and uses input-oblivious pruning techniques to prune away clearly unprofitable candidates, and (2) an online runtime system that explores the remaining candidates and uses lightweight cost models to select the best re-association based on the input graph and the embedding sizes. On a wide range of configurations, GRANII achieves a geo-mean speedup of 1.56× for inference and 1.4× for training across multiple GNN models and systems. We also show GRANII’s technique functions on diverse implementations and with techniques such as sampling.


title: From Threads to Tiles: T2T, a Compiler for CUDA-to-NPU Translation via 2D Vectorization

authors:
Shuaijiang Li
Jiacheng Zhao
Ying Liu
Shuoming Zhang
Lei Chen
Yijin Li
Yangyu Zhang
Zhicheng Li
Runyu Zhou
Xiyu Shi
Chunwei Xia
Yuan Wen
Xiaobing Feng
Huimin Cui

abstract: CUDA’s programming model, exposing massive parallelism via fine-grained scalar threads, has become the de facto standard for GPU computing. Concurrently, NPUs are emerging as highly efficient accelerators, but their architecture is fundamentally different, relying on coarse-grained, explicit 2-D tile-based instructions. This creates a critical challenge: bridging the semantic gap "From Threads to Tiles". A direct translation is infeasible, as it requires lifting the implicit parallelism of CUDA’s scalar model into the explicit, multi-dimensional vector space of NPUs, a problem we formalize as a lifting challenge.This paper introduces T2T, a compiler framework that automates this "Threads to Tiles" translation via the 2-D Vectorization technique. T2T first transforms a CUDA kernel’s implicit SIMT parallelism into a structured, explicit loop nest via our Unified Parallelism Abstraction (UPA), making the parallelism analyzable. From this representation, T2T’s core vectorization engine systematically selects optimal pairs of loops and maps them onto the NPU’s 2-D tile instructions to maximize hardware utilization. To ensure correctness and handle performance-critical CUDA features, a final set of semantics-preserving optimizations is applied, including efficient control-flow management and vectorization of warp-level intrinsics.We implement T2T based on Polygeist and evaluate representative NPU architectures. On a diverse set of benchmarks, kernels translated by T2T achieve up to 73% of native CUDA performance on an A100 GPU and outperform baseline translation approaches by up to 6.9×. Our work demonstrates that a systematic, compiler-driven approach to 2-D vectorization is a principled and high-performance path for porting the rich CUDA ecosystem to the evolving landscape of NPU accelerators.


title: PASTA: A Modular Program Analysis Tool Framework for Accelerators

authors:
Mao Lin
Hyeran Jeon
Keren Zhou

abstract: The increasing complexity and diversity of hardware accelerators in modern computing systems demand flexible, low-overhead program analysis tools. We present PASTA, a low-overhead and modular Program AnalysiS Tool Framework for Accelerators. PASTA abstracts over low-level profiling APIs and diverse deep learning frameworks, offering users a unified interface to capture and analyze runtime events at multiple levels. Its extensible design enables researchers and practitioners to rapidly prototype custom tools with minimal overhead. We demonstrate the utility of PASTA by developing several analysis tools, including tools for deep learning workload characterization and UVM optimization. Through extensive evaluations on mainstream deep learning workloads tested on NVIDIA and AMD GPUs under both single- and multi-GPU scenarios, we demonstrate PASTA’s broad applicability. On NVIDIA GPUs, we further show that PASTA provides detailed performance insights with significantly lower overhead (up to 1.3×104faster) than conventional analysis tools, thanks to its GPU-accelerated backend. PASTA strikes a practical balance between usability, extensibility, and efficiency, making it well-suited for modern accelerator-based computing environments.


title: BIT: Empowering Binary Analysis through the LLVM Toolchain

authors:
Puzhuo Liu
Peng Di
Jingling Xue
Yu Jiang

abstract: Binary analysis plays a critical role in software comprehension and security analysis, especially when source code is unavailable or difficult to analyze. Lifting binaries to LLVM IR enables reuse of the rich LLVM toolchain for downstream binary analyses. However, existing binary lifters often fail to produce syntactically valid LLVM IR or to restore sufficient semantics, making downstream analyses unreliable or unfeasible. This paper introduces BIT, a novel binary lifter designed to ensure syntactic compliance as well as semantic adequacy BIT achieves this through a multistage approach that includes anchor variable identification, analysis context collection, and IR refinement. In the evaluation, BIT achieved excellent results across multiple downstream analyses when compared with various lifters In static analysis, the F1 score of bug detection is 0.85, which is better than Plankton’s 0.81; in symbolic execution, it outperforms McSema by 3,049× in path exploration and by 1.36× in test case generation, respectively; in reanalysis, BIT can complete all tasks and is consistent with the advanced work McSema. These results highlight BIT’s ability to bridge the gap between binary-level analysis and the LLVM toolchain.


title: Compilation of Generalized Matrix Chains with Symbolic Sizes

authors:
Francisco López
Lars Karlsson
Paolo Bientinesi

abstract: Generalized Matrix Chains (GMCs) are products of matrices where each matrix carries features (e.g., general, symmetric, triangular, positive-definite) and is optionally transposed and/or inverted. GMCs are commonly evaluated via sequences of calls to BLAS and LAPACK kernels. When matrix sizes are known, one can craft a sequence of kernel calls to evaluate a GMC that minimizes some cost, e.g., the number of floating-point operations (FLOPs). Even in these circumstances, high-level languages and libraries, upon which users usually rely, typically perform a suboptimal mapping of the input GMC onto a sequence of kernels. In this work, we go one step beyond and consider matrix sizes to be symbolic (unknown); this changes the nature of the problem since no single sequence of kernel calls is optimal for all possible combinations of matrix sizes. We design and evaluate a code generator for GMCs with symbolic sizes that relies on multi-versioning. At compile-time, when the GMC is known but the sizes are not, code is generated for a few carefully selected sequences of kernel calls. At run-time, when sizes become known, the best generated variant for the matrix sizes at hand is selected and executed. The code generator uses new theoretical results that guarantee that the cost is within a constant factor from optimal for all matrix sizes and an empirical tuning component that further tightens the gap to optimality in practice. In experiments, we found that the increase above optimal in both FLOPs and execution time of the generated code was less than 15% for 95% of the tested chains.


title: Progressive Low-Precision Approximation of Tensor Operators on GPUs: Enabling Greater Trade-Offs between Performance and Accuracy

authors:
Fan Luo
Guangli Li
Zhaoyang Hao
Xueying Wang
Xiaobing Feng
Huimin Cui
Jingling Xue

abstract: Recent GPUs integrate specialized hardware for low-precision arithmetic (e.g., FP16, INT8), offering substantial speedups for tensor operations. However, existing methods typically rely on coarse, operator-level trial-and-error tuning, which restricts the performance–accuracy trade-off space and limits achievable gains.We present Platensor, a progressive low-precision approximation framework that expands this trade-off space through ne-grained, tile-level strategies. The key idea is to exploit the tiled computation patterns of GPUs to enable flexible precision control and richer optimization opportunities. Platensor performs a two-phase exploration: a fast rule-based pass that selects promising tile-level configurations, followed by an evolutionary search that refines them. It then automatically generates optimized kernels that combine tiles of different precisions.Experiments on GEMM operators and representative applications—including kNN, LLMs, and HPL-MxP—show that Platensor significantly broadens the attainable performance– accuracy trade-offs and more fully leverages low-precision arithmetic on modern GPUs compared to operator-level tuning.


title: Automatic Data Enumeration for Fast Collections

authors:
Tommy McMichen
Simone Campanoni

abstract: Data collections provide a powerful abstraction to organize data, simplifying development and maintenance. Choosing an implementation for each collection is a critical decision, with performance, memory and energy tradeoffs that need to be balanced for each use case. Specialized implementations offer significant benefits over their general-purpose counterparts, but also require certain properties of the data they store, such as uniqueness or ordering. To employ them, developers must either possess domain knowledge or transform their data to exhibit the desired property, which is a tedious, manual process. One such transformation—commonly used in data mining and program analysis—is data enumeration, where data items are assigned unique identifiers to enable fast equality checks and compact memory layout. In this paper, we present an automated approach to data enumeration, eliminating the need for manual developer effort. Our implementation in the MemOIR compiler achieves speedups of 2.16× on average (up to 8.72×) and reduces peak memory consumption by 5.6% on average (up to 50.7%). This work shows that automated techniques can manufacture data properties to unlock specialized collection implementations, pushing the envelope of collection-oriented optimization.


title: PriTran: Privacy-Preserving Inference for Transformer-Based Language Models under Fully Homomorphic Encryption

authors:
Yuechen Mu
Guangli Li
Shiping Chen
Jingling Xue

abstract: Transformer-based language models power many cloud services, but inference on sensitive data raises confidentiality concerns. Fully Homomorphic Encryption (FHE) enables computation on encrypted inputs while preserving privacy, but at high computational cost, making Transformers difficult to deploy. This paper presents PriTran, an efficient CKKS-based library for privacy-preserving Transformer inference on CPUs. Complementing the only prior work, RoLe, which supports only Berttiny(2 encoders), PriTran introduces two novel algorithms with optimized data layouts that accelerate ciphertext–plaintext (CP) and ciphertext–ciphertext (CC) matrix multiplications (MMs) across all Bert models by reducing costly rotations and multiplications. On the MNLI dataset, RoLe fails on inputs longer than 36 tokens within a 5-hour per-token budget, while PriTran achieves average speedups of 29.3% and 22.2% for CP- and CC-MMs, respectively, and 24.1% end-to-end. We further evaluate PriTran on scaled Berttinyvariants with additional encoders and on Bertmini(4 encoders), demonstrating correctness and scalability beyond RoLe’s limits. Within current FHE limits, these gains and RoLe’s failure on longer inputs underscore PriTran’s promise as a practical approach for FHE-based Transformer inference.


title: Practical: Are Abstract-Interpreter Baseline JITs Worth It? An Empirical Evaluation through Metacompilation

authors:
Nahuel Palumbo
Guillermo Polito
Stéphane Ducasse
Pablo Tesone

abstract: Baseline JIT compilers need to compile early and as fast as possible, while still performing optimizations. One powerful technique to write fast baseline JIT compilers is abstract interpretation. Several implementations of this technique exist in practice, implementing in a single pass optimizations such as register allocation, constant propagation, and instruction scheduling. However, although they share the same technique, all these implementations vary in the exact optimizations performed, their internal design and further implementation details (e.g., the implementation language and framework). Thus, it is challenging to understand and isolate the benefits of the technique by simply studing these existing implementations.Understanding the real impact of compile-time abstract interpreters requires isolating performance differences and experimenting with different variations of the same implementation, which demands extensive engineering work. In this paper, we propose to analyse the impact of abstract interpreters through metacompilation. We use metacompilation as a means to (a) reduce the experimentation effort and (b) to produce compiler variants that are comparable, reducing implementation noise.We implemented our solution to generate several JIT compiler variants for the Pharo VM. We describe the adaptations required in the metacompilation framework to target both abstract interpreters and direct translators, in combination with Static Type Prediction optimizations.Our benchmarks show that compile-time abstract interpreters, on average, reduce the emitted machine code size by 12% and increase execution speed by 10%, up to 30%, without increasing JIT compilation overhead, compared to direct translators.


title: QIGen: A Kernel Generator for Inference on Nonuniformly Quantized Large Language Models

authors:
Tommaso Pegolotti
Dan Alistarh
Markus Püschel

abstract: Efficient inference on large language models (LLMs) has become a popular topic in both academia and industry. Roughly speaking, LLMs consist of a collection of weight matrices, and generative inference on these models essentially computes a sequence of matrix-vector products and thus can be heavily memory-bound. Consequently, much work has been devoted to reducing the size of the weights to lower bit-widths through various forms of quantization. In turn, these diverse precision formats complicate both the arithmetic and optimized kernel implementation. So far, the vast majority of implementation work for mixed-precision LLM computation has been done manually. Currently, one of the most powerful and complex scalar LLM compression techniques is nonuniform quantization, in which a matrix is divided unevenly into parts that are quantized with different bit-widths, minimizing the output compression error. In this paper, we present QIGen, the first kernel generator for LLM inference on CPUs to support nonuniform quantization in full generality. Given a nonuniformly quantized LLM and target CPU characteristics, QIGen first generates the diverse set of needed custom matrix-vector product kernels and combines them with a suitable storage format. We benchmark and analyze QIGen-generated code in various experiments. In particular, we show that our code achieves Pareto optimality in terms of performance and accuracy with respect to the most used open-source tool. We show a speedup of up to 1.3× for the matrix-vector and 3.4× for the matrix-matrix computations even when using uniform quantization.


title: Unlocking Python Multithreading Capabilities using OpenMP-Based Programming with OMP4Py

authors:
César Piñeiro
Juan Carlos Pichel

abstract: Python exhibits inferior performance relative to traditional high performance computing (HPC) languages such as C, C++, and Fortran. This performance gap is largely due to Python’s interpreted nature and the Global Interpreter Lock (GIL), which restricts multithreading efficiency. However, the introduction of a GIL-free variant in the Python interpreter opens the door to more effective exploitation of multithreading parallelism in Python. Based on this important new feature, we introduce OMP4Py with the aim of bringing OpenMP’s familiar directive-based parallelization paradigm to Python. Its dual-runtime architecture design combines the benefits of a pure Python implementation with the performance and low-level capabilities required to maximize efficiency in compute-intensive tasks. In this way, OMP4Py offers both full Python support and the high performance required by HPC workloads.


title: Towards Path-Aware Coverage-Guided Fuzzing

authors:
Giacomo Priamo
Daniele Cono D'Elia
Mathias Payer
Leonardo Querzoni

abstract: Automated fuzz testing is now standard practice, yet key blind spots persist. Coverage-guided fuzzers typically rely on edge coverage as a lightweight proxy for program behavior. However, this metric captures path variations only weakly: it cannot differentiate executions that follow distinct control-flow paths but traverse the same edges—causing many path-dependent bugs to go undetected. Path awareness would offer a richer coverage view but has been considered too costly for fuzzing.We introduce a lightweight method for tracking intra-procedural execution paths, enabling efficient path-aware feedback. This enhances the fuzzer’s ability to detect subtle bugs, even in well-tested software. To counter the resulting seed explosion, we evaluate two strategies—culling and opportunistic path-aware fuzzing—that balance precision and throughput. Our findings show that path-aware fuzzing, when properly guided, uncovers more bugs and reveals untapped potential in fuzzing research.


title: DyPARS: Dynamic-Shape DNN Optimization via Pareto-Aware MCTS for Graph Variants

authors:
Hao Qian
Guangli Li
Qiuchu Yu
Xueying Wang
Jingling Xue

abstract: Dynamic-shape DNNs are widely used in applications such as variable-resolution image processing and language modeling with variable-length sequences. Existing DL (Deep-Learning) compilers apply rule-based rewriting to either transform a subgraph into a fixed variant at compile time (leading to suboptimal performance) or generate multiple variants at runtime, incurring significant overhead. The challenge is discovering and applying shape-dependent subgraph variants that maintain high efficiency across diverse inputs with minimal runtime cost.We propose DyPARS, a dynamic-shape DL compiler approach that discovers high-performance subgraph variants at compile time and applies the best ones at runtime. Leveraging Pareto-aware MCTS, DyPARS identifies shape-aware variants, incorporating shape-dependent kernel adaptations. These variants are integrated into a prediction-enhanced computational graph, enabling efficient variant selection based on input shapes with minimal overhead. DyPARS achieves average speedups of 1.31× and 1.80× over TorchInductor (JIT) and BladeDISC (non-JIT), respectively, across five DNN models, demonstrating robust efficiency across diverse inputs.


title: Thinking Fast and Correct: Automated Rewriting of Numerical Code through Compiler Augmentation

authors:
Siyuan Brant Qian
Vimarsh Sathia
Ivan R. Ivanov
Jan Hückelheim
Paul D. Hovland
William S. Moses

abstract: Floating-point numbers are finite-precision approximations to real numbers and are ubiquitous in computer applications in nearly every field. Selecting the right floating-point representation that balances performance and numerical accuracy is a difficult task – one that has become even more critical as hardware trends toward high-performance, low-precision operations. Although the common wisdom around changing floating-point precision implies that accuracy and performance are inversely correlated, more advanced techniques can often circumvent this tradeoff. Applying complex numerical optimizations to real-world code, however, is an arduous engineering task that requires expertise in numerical analysis and performance engineering, and application-specific numerical context. While there is a plethora of existing tools that partially automate this process, they are limited in the scope of optimization techniques or still require substantial human intervention. We present Poseidon, a modular and extensible framework that fully automates floating-point optimizations for real-world applications within a production compiler. Our key insight is that a small surrogate profile often reveals sufficient numerical context to drive effective rewrites. Poseidon operates as a two-phase compiler: the first compilation instruments the program to capture numerical context; the second compilation consumes profiled data, generates and evaluates candidate rewrites, and solves for optimal performance/accuracy tradeoffs. Poseidon’s interoperability with standard compiler analyses and optimizations grants it analysis and optimization advantages unavailable to existing source- and binary-level approaches. On multiple large-scale applications, Poseidon leads to outsized benefits in performance without substantially changing accuracy, and outsized accuracy benefits without diminishing performance. On a quaternion differentiator, Poseidon enables a 1.46× speedup with a relative error of 10−7. On DOE’s LULESH hydrodynamics application, Poseidon improves program accuracy to exactly match a 512-bit simulation run without substantially reducing performance.


title: Compiler-Assisted Instruction Fusion

authors:
Ravikiran Ravindranath Reddy
Sawan Singh
Arthur Perais
Alberto Ros
Alexandra Jimborean

abstract: Hardware instruction fusion combines multiple architectural instructions into a single operation, improving performance by freeing up resources. While fusion typically involves consecutive instructions, there are proposals to fuse non-consecutive instructions to maximize potential. However, such approaches require complex and costly hardware to predict and either validate fusion or unfuse, which significantly increases the cost of fusion. In this work, we propose a compiler technique, CAIF - Compiler Assisted Instruction Fusion, for fusion-aware instruction scheduling. CAIF identifies fusible but nonconsecutive memory operations and reorders eligible pairs of instructions such that they appear consecutively in the instruction stream.Our experiments demonstrate that for neural network workloads, a hardware that only fuses consecutive instructions obtains 1.2% average performance improvements over a no-fusion baseline when applications are compiled with a standard compiler and 19.6% when compiled with CAIF. In addition, when non-consecutive hardware fusion (Helios) is enabled, CAIF boosts performance from 6.6% to 20.3%. Moreover, CAIF can effectively handle the statically challenging general-purpose application and boost performance on SPEC CPU 2017 from 2.4% to 6.4%, and from 14.4% to 17.7%, respectively, on the hardware configurations mentioned above.


title: Binary Diffing via Library Signatures

authors:
Andrei Rimsa
Anderson Faustino da Silva
Camilo Santana
Fernando Magno Quintão Pereira

abstract: Binary diffing is the problem of determining whether two binary programs originate from the same source code. Binary diffing tools are used to identify malware, plagiarism, or code theft. Many instances of binary diffing assume an adversarial setting, where a malicious actor transforms binary code by changing the compiler. Traditional diffing techniques rely on statistical similarity analysis, often leveraging stochastic models. However, recent studies have shown that these classifiers perform poorly in the face of adversarial code transformations. To mitigate this scenario, this paper introduces a new diffing technique that is resilient against current obfuscation approaches. We propose comparing executables by matching their library signatures (libsig). A program’s library signature is the sequence of calls it makes to functions outside its .text section. The proposed classifier, LibSIG, is faster than off-the-shelf alternatives, such as ltrace, and, like it, works on stripped binaries or binaries running with address space layout randomization (ASLR) enabled. Furthermore, in contrast to ltrace, LibSIG can be engineered to detect even library calls that bypass conventional application binary interface patterns. Our experiments on the GNU Core Utilities demonstrate that LibSIG remains robust against obfuscators like Khaos and ollvm, as well as typical optimization patterns, outperforming binary diffing approaches such as SAFE, BinDiff, or Asm2Vec.


title: TPDE: A Fast Adaptable Compiler Back-End Framework

authors:
Tobias Schwarz
Tobias Kamm
Alexis Engelke

abstract: Fast machine code generation is especially important for fast start-up in just-in-time compilation, where the compilation time is part of the end-to-end latency. However, widely used compiler frameworks like LLVM do not prioritize fast compilation and require an extra IR translation step increasing latency even further; and rolling a custom code generator is a large engineering effort, especially when targeting multiple architectures.Therefore, in this paper, we present TPDE, a compiler back-end framework that adapts to existing code representations in SSA form. Using an IR-specific adapter providing canonical access to IR data structures and a specification of the IR semantics, the framework performs one analysis pass and then performs the compilation in just a single pass, combining instruction selection, register allocation, and instruction encoding. The generated target instructions are primarily derived code written in a high-level language through LLVM’s Machine IR, easing portability to different architectures while enabling optimizations during code generation.To show the generality of our framework, we build a new back-end for LLVM from scratch targeting x86-64 and AArch64. Performance results on SPECint 2017 show that we can compile LLVM-IR 8–26x faster than LLVM -O0 while being on-par in terms of run-time performance. We also demonstrate the benefits of adapting to domain-specific IRs in JIT contexts, particularly WebAssembly and database query compilation, where avoiding the extra IR translation further reduces compilation latency.


title: PolyUFC: Polyhedral Compilation Meets Roofline Analysis for Uncore Frequency Capping

authors:
Nilesh Rajendra Shah
M. V. V. S. Manoj Kumar
Dhairya Baxi
Ramakrishna Upadrasta

abstract: We present PolyUFC, an MLIR based compilation flow for uncore frequency capping that combines (performance and power) roofline analyses and polyhedral compilation-based static analysis for characterization of affine programs. We introduce a parametric mathematical model that links operational intensity and uncore frequency to derive frequency caps, validated through empirical evaluation on real hardware. By embedding these caps into Pluto optimized code generated by Polygeist, we achieve improvements in Energy Delay Product (EDP) up to 42% on compute-bound, and up to 54% on bandwidth-bound programs—carefully selected from ML-models from vision/NLP domains and PolyBench—over Intel UFS driver. Our framework is retargetable across multiple micro-architectures; and can handle multiple optimization goals like performance, energy and EDP, and is applicable across inter/intra dialects.


title: Space-Time Optimisations for Early Fault-Tolerant Quantum Computation

authors:
Sanaa Sharma
Prakash Murali

abstract: Fault-tolerance is the future of quantum computing, ensuring error-corrected quantum computation that can be used for practical applications. Resource requirements for fault-tolerant quantum computing (FTQC) are daunting, and hence, compilation techniques must be designed to ensure resource efficiency. There is a growing need for compilation strategies tailored to the early FTQC regime, which refers to the first generation of fault-tolerant machines operating under stringent resource constraints of fewer physical qubits and limited distillation capacity. Present-day compilation techniques are largely focused on overprovisioning of routing paths and make liberal assumptions regarding the availability of distillation factories. Our work develops compilation techniques that are tailored to the needs of early FTQC systems, including distillation-adaptive qubit layouts and routing techniques. In particular, we show that simple greedy heuristics are extremely effective for this problem, offering significant reduction in the number of qubits compared to prior works. Our techniques offer results with an average overhead of 1.2× in execution time for a 53 % reduction in qubits against the theoretical lower bounds. As the industry develops early FTQC systems with tens to hundreds of logical qubits over the coming years, our work has the potential to be widely useful for optimising program executions.


title: On the Precision of Dynamic Program Fingerprints Based on Performance Counters

authors:
Anderson Faustino Da Silva
Marcelo Borges Nogueira
Sérgio Queiroz de Medeiros
Jerónimo Castrillón
Fernando Magno Quintão Pereira

abstract: Task classification is the challenge of determining whether two binary programs perform the same task. This problem is essential in scenarios such as malware identification, plagiarism detection, and redundancy elimination. Classification can be performed statically or dynamically. In the former case, the classifier analyzes the binary image of the program, whereas in the latter it observes the program’s execution. Recent research has demonstrated that dynamic classification is more accurate, particularly in adversarial settings where programs may be obfuscated. This remains true even when both classifiers use the exact representation of programs, such as histograms of instruction opcodes. The superior accuracy of dynamic classification stems from its ability to disregard dead code inserted during the obfuscation process. However, state-of-the-art dynamic techniques, such as Valgrind plugins, can slow down program execution by as much as 100 times due to binary instrumentation. This paper proposes to eliminate this overhead by replacing program instrumentation with the sampling of hardware performance counters. Our findings reveal both advantages and limitations of this approach. On the positive side, classifiers based on hardware counters impose almost no runtime overhead while retaining greater accuracy than purely static classifiers, particularly in the presence of obfuscation. On the downside, counter-based classifiers are slightly less accurate than instrumentation-based approaches and offer coarser granularity, being limited to whole-program classification rather than individual functions. Despite these limitations, our results challenge the conventional belief that dynamic code classifiers are too costly to be deployed in environments such as online servers, operating systems, and virtual machines.


title: Ember: A Compiler for Embedding Operations on Decoupled Access-Execute Architectures

authors:
Marco Siracusa
Olivia Hsu
Víctor Soria Pardos
Joshua Randall
Arnaud Grasset
Eric Biscondi
Douglas J. Joseph
Randy Allen
Fredrik Kjolstad
Miquel Moretó Planas
Adrià Armejach

abstract: Decoupled Access-Execute (DAE) architectures separate memory accesses from computation in two specialized units. This design is becoming increasingly popular among hyperscalers to accelerate irregular embedding lookups in recommendation models. In this paper, we first broaden the scope by demonstrating the benefits of DAE architectures across a wider range of irregular embedding operations in several machine learning models. Then, we propose the Ember compiler to automatically compile all of these embedding operations to DAE architectures. Conversely from other DAE compilers, Ember features multiple intermediate representations specifically designed for different optimization levels. In this way, Ember can implement all optimizations to match the performance of hand-written code, unlocking the full potential of DAE architectures at scale.


title: The Parallel-Semantics Program Dependence Graph for Parallel Optimization

authors:
Yian Su
Brian Homerding
Haocheng Gao
Federico Sossai
Yebin Chon
David I. August
Simone Campanoni

abstract: Modern shared-memory parallel programming models, such as OpenMP and Cilk, enable developers to encode a parallel execution plan within their code. Existing compilers, including Clang and GCC, directly lower or add additional compatible parallelism on top of the developers’ plan. However, when better parallel execution plans exist that are incompatible with the original plan, compilers lack the capability of disregarding it and replacing it with a better one. To address this problem, this paper introduces the parallel-semantics program dependence graph (PS-PDG), an extension of the program dependence graph (PDG) abstraction that can simultaneously represent parallel semantics derived from both the developer’s original plan and the compiler’s own analysis. To demonstrate the power of PS-PDG, this paper also introduces GINO, an LLVM-based compiler capable of optimizing parallel execution plans using PS-PDG. Through exploring, reasoning, and implementing better parallel execution plans unlocked by PS-PDG, GINO outperforms the developer’s original parallel execution plan by 46.6% at most, and by 15% on average over 56 cores across 8 benchmarks from the NAS benchmark suite.


title: FHEFusion: Enabling Operator Fusion in FHE Compilers for Depth-Efficient DNN Inference

authors:
Tianxiang Sui
Jianxin Lai
Long Li
Peng Yuan
Yan Liu
Qing Zhu
Xiaojing Zhang
Linjie Xiao
Mingzhe Zhang
Jingling Xue

abstract: Operator fusion is essential for accelerating FHE-based DNN inference because it reduces multiplicative depth and, in turn, lowers the cost of ciphertext operations by keeping them at lower ciphertext levels. Existing approaches either rely on manual optimizations, which miss cross-operator opportunities, or on compiler pattern matching, which lacks generality. Standard DNN graphs omit FHE-specific behaviors, while fully lowering to primitive FHE operations introduces excessive granularity and obstructs effective optimization.We present FHEFusion, a compiler framework for the CKKS scheme that enables fusion through a new IR. This IR preserves high-level DNN semantics while introducing FHE-aware operators—masking and compaction (Strided_Slice)—that are central to CKKS, thereby exposing broader fusion opportunities. Guided by algebraic rules and an FHE-aware cost model, FHEFusion reduces multiplicative depth and identifies profitable fusions. Integrated into ANT-ACE, a state-of-the-art FHE compiler, FHEFusion outperforms NGRAPH, the only framework with graph-level fusion, achieving up to 3.02× (average 1.40×) speedup across seven DNNs (13 variants from different RELU approximations) on CPUs, while maintaining inference accuracy.


title: Dr.avx: A Dynamic Compilation System for Seamlessly Executing Hardware-Unsupported Vectorization Instructions

authors:
Yue Tang
Mianzhi Wu
Yufeng Li
Haoyu Liao
Jianmei Guo
Bo Huang

abstract: Modern processors are breaking a fundamental rule: backward compatibility within their own ISA families. We term this Generational ISA Fragmentation (GIF), where newer processors cannot execute instructions supported by prior generations within the same ISA family. This phenomenon is exemplified by Intel’s removal of AVX-512 from Alder Lake processors after years of deployment, ARM’s inconsistent support for SVE across cores, and RISC-V’s incompatible vector specifications. GIF causes illegal instruction crashes when running applications optimized for earlier processors on newer hardware, threatening the foundation of software portability that has underpinned decades of computing evolution.We introduce Dr.avx, a dynamic compilation system that enables seamless execution of AVX-512 instructions on hardware that lacks native support. Dr.avx addresses the most instructive GIF instance, x86 AVX-512 fragmentation, by targeting the integer and floating-point operations that dominate real workloads. Our rewrite engine performs a fine-grained classification of AVX-512 opcode-operand patterns and employs three complementary strategies: Instr Mirroring, AVX Lowering, and Scalar Fallback. Experiments show that Dr.avx incurs a geometric mean overhead of 1.44× on SPEC CINT2017 relative to native AVX-512 execution, 17.3% better than Intel’s closed-source SDE. On production databases, Dr.avx sustains 75%–88% (MySQL) and 86%–99% (MongoDB) of native throughput, yielding 2.0–2.7× higher throughput than SDE. For LLM inference (llama.cpp), Dr.avx keeps 95%–99% of native tokens/s and delivers 2.5–4.8× speedup over SDE. Unlike Intel’s proprietary SDE, which provides no visibility into its implementation details, Dr.avx achieves functional correctness while providing an open, extensible, near-native performance implementation. Our work offers both a remedy for AVX-512 fragmentation and a blueprint for addressing similar compatibility challenges emerging across all major ISAs.


title: LEGO: A Layout Expression Language for Code Generation of Hierarchical Mapping

authors:
Amir Mohammad Tavakkoli
Cosmin E. Oancea
Mary W. Hall

abstract: We describe LEGO, a new approach to optimizing data movement whereby code is expressed as a layout-independent computation and composed with layouts for data and computation. This code generator organization derives complex indexing expressions associated with hierarchical parallel code and data movement for GPUs. LEGO maps from layout specification to indexing expressions, and can be integrated into existing compilers and code templates. It facilitates the explo-ration of data layouts in combination with other optimizations. We demonstrate LEGO’s integration with the Triton and MLIR compilers, and with CUDA templates. We show that LEGO is capable of deriving performance competitive with Triton, and shows broad applicability for data and thread layout mapping optimizations in its integration with CUDA and MLIR.


title: A Reinforcement Learning Environment for Automatic Code Optimization in the MLIR Compiler

authors:
Mohammed Tirichine
Nassim Ameur
Nazim Bendib
Iheb Nassim Aouadj
Djad Bouchama
Rafik Bouloudene
Riyadh Baghdadi

abstract: Code optimization is a crucial task that aims to enhance code performance. However, this process is often tedious and complex, highlighting the necessity for automatic code optimization techniques. Reinforcement Learning (RL) has emerged as a promising approach for tackling such complex optimization problems. In this project, we introduce MLIR RL, an RL environment for the MLIR compiler, dedicated to facilitating MLIR compiler research and enabling automatic code optimization. We propose a multi-discrete formulation of the action space where the action space is the Cartesian product of simpler action subspaces. We also propose a new method, called level pointers, to reduce the size of the action space related to the loop interchange transformation. This enables more efficient and effective learning of the policy. To demonstrate the effectiveness of MLIR RL, we train an RL agent to optimize MLIR Linalg code, targeting CPU. The code is generated from two domain-specific frameworks: deep-learning models generated from PyTorch, and LQCD (Lattice Quantum Chromodynamics) code generated from an LQCD compiler. The result of this work is a research environment that allows the community to experiment with novel ideas in RL-driven loop-nest optimization.


title: Pyls: Enabling Python Hardware Synthesis with Dynamic Polymorphism via LCRS Encoding

authors:
Bolei Tong
Yongyan Fang
Chaorui Wang
Qingan Li
Jingling Xue
Mengting Yuan

abstract: Python dominates AI development and is the most widely used dynamic programming language, but synthesizing its polymorphic functions into hardware remains challenging. Existing HLS solutions support only static subsets of Python, forcing CPU offload with costly communication overhead. We present Pyls, the first framework that synthesizes dynamically polymorphic Python into monolithic hardware via Left-Child Right-Sibling (LCRS) encoding. Key to our approach is representing all Python objects as LCRS trees, enabling uniform hardware handling of dynamic types. Pyls automatically converts objects to fixed-width formats, generates XLS IR designs, and implements a tree memory architecture for efficient runtime type resolution. On FPGA platforms, Pyls demonstrates speedups of 5.19× and 3.98× over two ASIC CPUs, 303.29× over a soft-core processor, and 282.66× over a heterogeneous SoC design.


title: Accelerating App Recompilation across Android System Updates by Code Reusing

authors:
Hongtao Wu
Yu Chen
Mengfei Xie
Futeng Yang
Jun Yan
Jiang Ma
Jianming Fu
Chun Jason Xue
Qingan Li

abstract: Android utilizes Ahead-of-Time (AOT) compilation technology to precompile applications and stores the compiled code in OAT files, thereby improving app performance. When the Android system is updated, the old OAT files become invalidated. Applications will fall back to interpreted execution, resulting in degraded performance. To accommodate the frequent updates to the Android system that commonly occur on a monthly basis for most smartphone manufacturers, apps must be frequently recompiled into OAT files to promptly restore optimal app performance. However, recompiling applications is a resource-consuming process that cannot be completed quickly. Users have to endure issues such as device overheating and lag, which are caused by performance degradation after system updates.This paper evaluated popular Android apps across different system updates and made an important observation: up to 99% of the compiled code can be reused across different system updates, rendering most existing recompilation efforts unnecessary. Based on this observation, this paper proposes a method to accelerate app recompilation across Android system updates by reusing the old OAT files. We evaluated the proposed method with eight popular apps, on ten open-source Android system pairs and one closed-source Android system pair provided by a smartphone manufacturer. These Android system pairs have the same Android Runtime (ART) version and execute AOT compilation in both speed and speed-profile modes. Experimental results show that the proposed method reuses approximately 95% of compiled methods, achieving average speedups of 2.12× in CPU time and 1.39× in wall-clock time in speed-profile mode. In speed mode, the proposed method reuses about 99% of compiled methods, achieving average speedups of 5.15× in CPU time and 2.80× in wall-clock time, respectively. The proposed method not only accelerates app recompilation but also generates OAT files identical to those generated by native AOT compilation, without introducing security issues. Therefore, it holds significant promise for real-world deployment and has the potential to enhance user experience by speeding up the generation of new OAT files for applications.


title: Fast Autoscheduling for Sparse ML Frameworks

authors:
Bobby Yan
Alexander J. Root
Trevor Gale
David Broman
Fredrik Kjolstad

abstract: The rapid growth in the size of deep learning models strains the capabilities of dense computation paradigms. Leveraging sparse computation has become increasingly popular for training and deploying large-scale models, but existing deep learning frameworks lack extensive support for sparse operations. Current approaches either require manual scheduling expertise or rely on exhaustive search taking hours to days, which are both incompatible with the interactive development essential to machine learning research. We present three algorithmic contributions that enable fast, automatic optimization of sparse tensor computations. First, we develop a heuristic-based loop ordering algorithm that avoids asymptotic performance cliffs while compiling in milliseconds rather than hours. Second, we introduce a tiling algorithm specialized for mixed sparse-dense computations that achieves performance comparable to hand-optimized kernels. Third, we present a format inference algorithm that automatically selects appropriate sparse tensor formats for intermediate and output tensors based on operation semantics. These algorithms are grounded in the computational properties of sparse tensor algebra, making them predictable and robust across diverse workloads. We implement these techniques in Scorch, a prototype sparse tensor compiler for PyTorch that demonstrates their practical effectiveness. With only minimal code changes, our approach achieves 1.05–5.80× speedups over PyTorch Sparse on end-to-end tasks including graph neural networks, sparse autoencoders, and sparse transformers, with compilation times fast enough for interactive ML development.


title: OpenQudit: Extensible and Accelerated Numerical Quantum Compilation via a JIT-Compiled DSL

abstract: High-performance numerical quantum compilers rely on classical optimization, but are limited by slow numerical evaluations and a design that makes extending them with new instructions a difficult, error-prone task for domain experts. This paper introduces OpenQudit, a compilation framework that solves these problems by allowing users to define quantum operations symbolically in the Qudit Gate Language (QGL), a mathematically natural DSL. OpenQudit’s ahead-of-time compiler uses a tensor network representation and an e-graph-based pass for symbolic simplification before a runtime tensor network virtual machine (TNVM) JIT-compiles the expressions into high-performance native code. The evaluation shows that this symbolic approach is highly effective, accelerating the core instantiation task by up to ~20× on common quantum circuit synthesis problems compared to state-of-the-art tools.


title: Selene: Cross-Level Barrier-Free Pipelining for Irregular Nested Loops in High-Level Synthesis

authors:
Sungwoo Yun
Seonyoung Cheon
Dongkwan Kim
Heelim Choi
Kunmo Jeong
Chan Lee
Yongwoo Lee
Hanjun Kim

abstract: The growing demand for domain-specific accelerators in fields such as machine learning, graph analytics, and scientific computing has highlighted the need for productive and efficient hardware design methodologies. High-level synthesis (HLS) offers an attractive solution by generating hardware from high-level code, with loop pipelining as a cornerstone for maximizing throughput in regular computations. However, existing static and dynamic HLS approaches fail to achieve high pipeline utilization for irregular loop nests characterized by data-dependent bounds, unpredictable memory access patterns, and loop-carried dependencies.To address the pipeline underutilization in irregular loop, this work proposes a new barrier-free pipeline architecture with a cross-level scheduling strategy and the corresponding HLS compiler Selene, that automatically synthesizes the proposed architecture. Our approach introduces a fine-grained pipeline controller and an outer-loop iteration interleaving mechanism, enabling concurrent execution of multiple outer-loop iterations and efficient handling of data dependencies. Implemented within a commercial HLS flow, Vitis HLS, Selene delivers significant speedups of 4.74× and 5.46× over both standard static and dynamic HLS tools on a range of irregular workload benchmarks, demonstrating its effectiveness in overcoming challenges to efficient hardware generation for data-dependent applications.


title: Hexcute: A Compiler Framework for Automating Layout Synthesis in GPU Programs

authors:
Xiao Zhang
Yaoyao Ding
Bolin Sun
Yang Hu
Tatiana Shpeisman
Gennady Pekhimenko

abstract: Efficient GPU programming is crucial for achieving high performance in deep learning (DL) applications. The performance of GPU programs depends on how data is parallelized across threads and arranged within memory subsystems. The mapping functions describing tensors on GPUs are known as tensor layouts. Low-level programming frameworks, such as CUTLASS and Hidet, provide expressive layout abstractions but often require considerable programming effort to manually specify optimal layouts. High-level GPU programming languages, such as Triton, rely on compiler heuristics to generate dataflow, layouts, and pipelining strategies in GPU programs. However, the heuristics for dataflow and pipelining strategies are not generalizable to complex operators. To balance expressiveness and programmability, we propose Hexcute, a compiler framework that automates layout synthesis while providing explicit control over dataflow and pipelining. Hexcute formalizes layout synthesis as a constraint programming problem and solves it with a type-inference-based algorithm. This approach enables systematic exploration of optimal layouts and instructions.Our evaluation shows that Hexcute matches the performance of libraries like cuBLAS and FlashAttention on GEMM, Attention, and their variants, while reducing the amount of code by 1.27×-7.94× compared to CUTLASS. For mixed-type mixture-of-experts (MoE) operators, Hexcute achieves an average speedup of 6.46× over Triton. In the end-to-end evaluations of vLLM, Hexcute delivers up to 2.60× speedup on DeepSeek-R1-AWQ and 2.04× on a Mamba-based model.


title: Pushing Tensor Accelerators beyond MatMul in a User-Schedulable Language

authors:
Yihong Zhang
Derek K. Gerstmann
Andrew Adams
Maaz Bin Safeer Ahmad

abstract: Tensor accelerators now represent a growing share of compute resources in modern CPUs and GPUs. However, they are hard to program, leading developers to use vendor-provided kernel libraries that support tensor accelerators. As a result, the usage of tensor accelerators is limited to the provided interface, mainly designed for traditional ML and scientific computing workloads.In this paper, we show that tensor accelerators can improve the performance of applications beyond simple variants of MatMul. For example, many image processing pipelines are linear transformations over matrices in disguise and can therefore utilize such specialized hardware. This is nonetheless hindered by the difficulties in programming tensor accelerators. We tackle this problem with compiler-based techniques. We use the Halide user-schedulable language and express operations as Halide algorithms succinctly. To this end, we implement a flexible tensor instruction selector based on equality saturation. The tensor instruction selector supports both CPU- and GPU-attached tensor accelerators and works with existing scheduling operations (e.g., producer-consumer fusion). Together, this enables developers to write diverse accelerator-leveraging applications in a few dozen lines.Using our system, we demonstrate the potential of tensor accelerators beyond their traditional domains. We implement several image processing pipelines (e.g., filtering, resampling, and denoising) in our system and evaluate them against non-accelerator-leveraging baselines. We show that these pipelines can achieve significant speedups. For example, a downsampling routine is sped up by 6.1× by utilizing Tensor Cores on an Nvidia RTX 4070 GPU.


title: FRUGAL: Pushing GPU Applications beyond Memory Limits

authors:
Lingqi Zhang
Tengfei Wang
Jiajun Huang
Chen Zhuang
Ivan R. Ivanov
Peng Chen
Toshio Endo
Mohamed Wahib

abstract: GPUs power modern scientific and AI applications, but their limited memory capacity restricts scalability. Buying GPUs with larger HBM is prohibitively expensive and still bounded by market limits. Existing solutions either exploit application-specific knowledge through out-of-core techniques, which lack generality, or rely on system-level page faulting, which is transparent but inefficient. We propose FRUGAL, an application-agnostic framework and methodology that reduces GPU memory footprint while sustaining high performance. FRUGAL formulates memory management as an optimization over an application’s execution graph, encompassing prefetching, kernel execution, and offloading. Using static analysis and profiling, FRUGAL applies a two-phase scheduling and migration strategy, solving an otherwise intractable optimization efficiently. Evaluations on Tiled Cholesky Decomposition, Tiled LU Decomposition, Tiny-CUDA-NN, and QuEST show that FRUGAL significantly reduces maximum GPU memory usage by 80.21%, 80.20%, 64.75% and 60.86% with only a geometric mean of 28.31% slowdown. FRUGAL allows applications to exceed hardware-imposed limits, and maintains strong performance scalability beyond existing GPU memory constraints, without additional hardware cost.


title: SparseX: Synergizing GPU Libraries for Sparse Matrix Multiplication on Heterogeneous Processors

authors:
Ruifeng Zhang
Xiangwei Wang
Ang Li
Xipeng Shen

abstract: Sparse Matrix-Matrix Multiplication (SpMM) on GPU is critical to applications ranging from scientific simulations to Graph Neural Networks (GNNs) and Deep Neural Networks (DNNs). Modern GPUs offer diverse processing units, such as CUDA cores, Tensor Cores, and Sparse Tensor Cores. Many SpMM libraries have been built to harness those different types of processors. Although impressive performance has been reported by each, including cuSparse, Sputnik, CLASP, and Jigsaw, a systematic study in this work shows that no single library is a clear winner across all matrices and scenarios. Based on the empirical observations, this work proposes the first solution to synergize the various libraries to best harness the heterogeneous processors and the array of cutting-edge libraries. The solution is an extensible framework, namely SparseX, that can automatically select the best matrix multiplication library (and types of processors) on the fly for a given sparse matrix on a GPU through an agile accurate predictive model. Experiments show that SparseX can speed up sparse matrix multiplications on thousands of real-world matrices significantly over the SOTA GPU libraries, achieving significant speedups (e.g., as much as 95.34x over cuSparse). Its extensible design makes it easy to be extended to cover new libraries and hardware architectures.


title: Proton: Towards Multi-level, Adaptive Profiling for Triton

authors:
Keren Zhou
Tianle Zhong
Hao Wu
Jihyeong Lee
Yue Guan
Yufei Ding
Corbin Robeck
Yuanwei Fang
Jeff Niu
Philippe Tillet

abstract: Domain-Specific languages (DSLs) such as Triton enable developers to write high-performance GPU kernels in a Python-friendly manner; however, profiling these kernels with existing tools often incurs runtime and storage overhead while failing to deliver actionable insights for both kernel authors and framework developers. We present Proton, a multi-level, adaptive profiler tailored for the Triton programming language and compiler. Proton provides frontend APIs to selectively profile relevant regions, aggregate results, capture custom metrics not available through hardware counters, and query profiles using a SQL-like language. Proton’s backend design unifies vendor profiling APIs with instrumentation-based profiling, ensuring portability and extensibility. Using Proton, users are able to query custom and hardware metrics across the relevant levels of abstraction—full end-to-end model execution, isolated neural network layers, language-specific Triton operators, and compiler intermediate representations. We demonstrate the tool’s effectiveness through case studies on production-grade kernel development, continuous integration, multi-GPU analysis, language model inference, and intra-kernel profiling. Our evaluations on end-to-end workloads, as well as standalone Triton kernels, demonstrate that Proton imposes lower runtime overhead and delivers significant reductions in profile sizes relative to existing framework and vendor profilers while being fully open source.


venue: cpp

title: VeriSmall: Verified Smallfoot Shape Analysis


title: A Modular Integration of SAT/SMT Solvers to Coq through Proof Witnesses

authors:
Michaël Armand
Germain Faure
Benjamin Grégoire
Chantal Keller
Laurent Théry
Benjamin Werner


title: Automatically Verifying Typing Constraints for a Data Processing Language

authors:
Michael Backes
Catalin Hritcu
Thorsten Tarrach


title: Modular SMT Proofs for Fast Reflexive Checking Inside Coq

authors:
Frédéric Besson
Pierre-Emmanuel Cornilleau
David Pichardie


title: Engineering Theories with Z3


title: Full Reduction at Full Throttle

authors:
Mathieu Boespflug
Maxime Dénès
Benjamin Grégoire


title: Reconstruction of Z3's Bit-Vector Proofs in HOL4 and Isabelle/HOL

authors:
Sascha Böhme
Anthony C. J. Fox
Thomas Sewell
Tjark Weber


title: Coquet: A Coq Library for Verifying Hardware

abstract: We propose a new library to model and verify hardware circuits in the Coq proof assistant. This library allows one to easily build circuits by following the usual pen-and-paper diagrams. We define a deep-embedding: we use a (dependently typed) data-type that models the architecture of circuits, and a meaning function. We propose tactics that ease the reasoning about the behavior of the circuits, and we demonstrate that our approach is practicable by proving the correctness of various circuits: a text-book divide and conquer adder of parametric size, some higher-order combinators of circuits, and some sequential circuits: a buffer, and a register.


title: Tactics for Reasoning Modulo AC in Coq

authors:
Thomas Braibant
Damien Pous

abstract: We present a set of tools for rewriting modulo associativity and commutativity (AC) in Coq, solving a long-standing practical problem. We use two building blocks: first, an extensible reflexive decision procedure for equality modulo AC; second, an OCaml plug-in for pattern matching modulo AC. We handle associative only operations, neutral elements, uninterpreted function symbols, and user-defined equivalence relations. By relying on type-classes for the reification phase, we can infer these properties automatically, so that end-users do not need to specify which operation is A or AC, or which constant is a neutral element.


title: Mechanizing the Metatheory of mini-XQuery

authors:
James Cheney
Christian Urban


title: A Decision Procedure for Regular Expression Equivalence in Type Theory

authors:
Thierry Coquand
Vincent Siles


title: Certified Security Proofs of Cryptographic Protocols in the Computational Model: An Application to Intrusion Resilience

authors:
Pierre Corbineau
Mathilde Duclos
Yassine Lakhnech


title: Constructive Formalization of Hybrid Logic with Eventualities

authors:
Christian Doczkal
Gert Smolka


title: Formalization of Wu's Simple Method in Coq

authors:
Jean-David Génevaux
Julien Narboux
Pascal Schreck


title: Teaching Experience: Logic and Formal Methods with Coq

authors:
Martin Henz
Aquinas Hobor


title: Proof Pearl: The Marriage Theorem

authors:
Dongchen Jiang
Tobias Nipkow


title: The Teaching Tool CalcCheck A Proof-Checker for Gries and Schneider's "Logical Approach to Discrete Math"


title: Reasoning about Constants in Nominal Isabelle or How to Formalize the Second Fixed Point Theorem

authors:
Cezary Kaliszyk
Henk Barendregt


title: Coq Mechanization of Featherweight Fortress with Multiple Dispatch and Multiple Inheritance

authors:
Jieung Kim
Sukyoung Ryu


title: Verification of Scalable Synchronous Queue

authors:
Jinjiang Lei
Zongyan Qiu


title: A Proposal for Broad Spectrum Proof Certificates


title: Hardware-Dependent Proofs of Numerical Programs

authors:
Thi Minh Tuyen Nguyen
Claude Marché


title: Algebra, Logic, Locality, Concurrency


title: Proof-Carrying Code in a Session-Typed Process Calculus

authors:
Frank Pfenning
Luís Caires
Bernardo Toninho


title: Simple, Functional, Sound and Complete Parsing for All Context-Free Grammars


title: First Steps towards the Certification of an ARM Simulator Using Compcert

authors:
Xiaomu Shi
Jean-François Monin
Frédéric Tuong
Frédéric Blanqui

abstract: The simulation of Systems-on-Chip (SoC) is nowadays a hot topic because, beyond providing many debugging facilities, it allows the development of dedicated software before the hardware is available. Low-consumption CPUs such as ARM play a central role in SoC. However, the effectiveness of simulation depends on the faithfulness of the simulator. To this effect, we propose here to prove significant parts of such a simulator, SimSoC. Basically, on one hand, we develop a Coq formal model of the ARM architecture while on the other hand, we consider a version of the simulator including components written in Compcert-C. Then we prove that the simulation of ARM operations, according to Compcert-C formal semantics, conforms to the expected formal model of ARM. Size issues are partly dealt with using automatic generation of significant parts of the Coq model and of SimSoC from the official textual definition of ARM. However, this is still a long-term project. We report here the current stage of our efforts and discuss in particular the use of Compcert-C in this framework.


title: Automated Certification of Implicit Induction Proofs

authors:
Sorin Stratulat
Vincent Demange


title: Univalent Semantics of Constructive Type Theories


title: Proof Pearl: Abella Formalization of λ-Calculus Cube Property


title: Rating Disambiguation Errors

authors:
Andrea Asperti
Wilmer Ricciotti


title: Automation in Computer-Aided Cryptography: Proofs, Attacks and Designs

authors:
Gilles Barthe
Benjamin Grégoire
César Kunz
Yassine Lakhnech
Santiago Zanella-Béguelin


title: Improving Real Analysis in Coq: A User-Friendly Approach to Integrals and Derivatives

authors:
Sylvie Boldo
Catherine Lelay
Guillaume Melquiond


title: The New Quickcheck for Isabelle - Random, Exhaustive and Symbolic Testing under One Roof


title: An Executable Semantics for CompCert C


title: A String of Pearls: Proofs of Fermat's Little Theorem

authors:
Hing-Lun Chan
Michael Norrish


title: Compact Proof Certificates for Linear Logic


title: Coherent and Strongly Discrete Rings in Type Theory

authors:
Thierry Coquand
Anders Mörtberg
Vincent Siles


title: Constructive Completeness for Modal Logic with Transitive Closure


title: Program Certification by Higher-Order Model Checking


title: Mechanized Semantics for Compiler Verification


title: Scalable Formal Machine Models


title: On the Correctness of an Optimising Assembler for the Intel MCS-51 Microprocessor

authors:
Dominic P. Mulligan
Claudio Sacerdoti Coen


title: Noninterference for Operating System Kernels

authors:
Toby C. Murray
Daniel Matichuk
Matthew Brassil
Peter Gammie
Gerwin Klein


title: Shall We Juggle, Coinductively?


title: A Formal Proof of Square Root and Division Elimination in Embedded Programs


title: Proving Concurrent Noninterference

authors:
Andrei Popescu
Johannes Hölzl
Tobias Nipkow


title: A Formally-Verified Alias Analysis

authors:
Valentin Robert
Xavier Leroy


title: Producing Certified Functional Code from Inductive Specifications

authors:
Pierre-Nicolas Tollitte
David Delahaye
Catherine Dubois


title: Compositional Verification of a Baby Virtual Memory Manager

authors:
Alexander Vaynberg
Zhong Shao


title: Mechanized Verification of Computing Dominators for Formalizing Compilers

authors:
Jianzhou Zhao
Steve Zdancewic


title: Formalizing Probabilistic Noninterference


title: A Formal Proof of Borodin-Trakhtenbrot's Gap Theorem


title: Programming Type-Safe Transformations Using Higher-Order Abstract Syntax

authors:
Olivier Savary Bélanger
Stefan Monnier
Brigitte Pientka


title: Certifiably Sound Parallelizing Transformations


title: Refinements for Free!

authors:
Cyril Cohen
Maxime Dénès
Anders Mörtberg


title: A Constructive Theory of Regular Languages in Coq

authors:
Christian Doczkal
Jan-Oliver Kaiser
Gert Smolka


title: Mostly Sound Type System Improves a Foundational Program Verifier

authors:
Josiah Dodds
Andrew W. Appel


title: Certified Parsing of Regular Languages

authors:
Denis Firsov
Tarmo Uustalu


title: Formalizing the SAFECode Type System

authors:
Daniel Huang
Greg Morrisett


title: Lifting and Transfer: A Modular Design for Quotients in Isabelle/HOL

authors:
Brian Huffman
Ondrej Kuncar


title: Machine Assisted Proof of ARMv7 Instruction Level Isolation Properties

authors:
Narges Khakpour
Oliver Schwarz
Mads Dam


title: Aliasing Restrictions of C11 Formalized in Coq


title: π n (S n ) in Homotopy Type Theory

authors:
Daniel R. Licata
Guillaume Brunerie


title: Extracting Proofs from Tabled Proof Search

authors:
Dale Miller
Alwen Tiu


title: Proof Pearl: A Verified Bignum Implementation in x86-64 Machine Code

authors:
Magnus O. Myreen
Gregorio Curello


title: Nonfree Datatypes in Isabelle/HOL - Animating a Many-Sorted Metatheory

authors:
Andreas Schropp
Andrei Popescu


title: Certified Kruskal's Tree Theorem


title: Computational Verification of Network Programs in Coq


title: A Formal Model and Correctness Proof for an Access Control Policy Framework

authors:
Chunhan Wu
Xingyuan Zhang
Christian Urban


title: The Speedup Theorem in a Primitive Recursive Framework

abstract: Blum's speedup theorem is a major theorem in computational complexity, showing the existence of computable functions for which no optimal program can exist: for any speedup function r there exists a function fr such that for any program computing fr we can find an alternative program computing it with the desired speedup r. The main corollary is that algorithmic problems do not have, in general, a inherent complexity.


title: Fixed Precision Patterns for the Formal Verification of Mathematical Constant Approximations

abstract: We describe two approaches for the computation of mathematical constant approximations inside interactive theorem provers. These two approaches share the same basis of fixed point computation and differ only in the way the proofs of correctness of the approximations are described. The first approach performs interval computations, while the second approach relies on bounding errors, for example with the help of derivatives. As an illustration, we show how to describe good approximations of the logarithm function and we compute -- to a precision of a million decimals inside the proof system, with a guarantee that all digits up to the millionth decimal are correct. All these experiments are performed with the Coq system, but most of the steps should apply to any interactive theorem prover.


title: Verified Validation of Program Slicing

authors:
Sandrine Blazy
André Maroneze
David Pichardie

abstract: Program slicing is a well-known program transformation which simplifies a program wrt a given criterion while preserving its semantics. Since the seminal paper published by Weiser in 1981, program slicing is still widely used in various application domains. State of the art program slicers operate over program dependence graphs (PDG), a sophisticated data structure combining data and control dependences.


title: Certified Abstract Interpretation with Pretty-Big-Step Semantics

authors:
Martin Bodin
Thomas P. Jensen
Alan Schmitt

abstract: This paper describes an investigation into developing certified abstract interpreters from big-step semantics using the Coq proof assistant. We base our approach on Schmidt's abstract interpretation principles for natural semantics, and use a pretty-big-step (PBS) semantics, a semantic format proposed by Charguéraud. We propose a systematic representation of the PBS format and implement it in Coq. We then show how the semantic rules can be abstracted in a methodical fashion, independently of the chosen abstract domain, to produce a set of abstract inference rules that specify an abstract interpreter. We prove the correctness of the abstract interpreter in Coq once and for all, under the assumption that abstract operations faithfully respect the concrete ones. We finally show how to define correct-by-construction analyses: their correction amounts to proving they belong to the abstract semantics.


title: Practical Tactics for Verifying C Programs in Coq

authors:
Jingyuan Cao
Ming Fu
Xinyu Feng

abstract: Proof automation is essential for large scale proof development such as OS kernel verification. An effective approach is to develop tactics and SMT solvers to automatically prove verification conditions. However, for complex systems, it is almost impossible to achieve fully automated verification and human interactions are unavoidable. So the key challenge here is, on the one hand, to reduce manual proofs as much as possible, and on the other hand, to provide user-friendly error messages when the automated verification fails, so that users could adjust specifications or the code accordingly, or to do part of the proofs manually.


title: A Lightweight Formalization of the Metatheory of Bisimulation-Up-To

authors:
Kaustuv Chaudhuri
Matteo Cimini
Dale Miller

abstract: Bisimilarity of two processes is formally established by producing a bisimulation relation that contains those two processes and obeys certain closure properties. In many situations, particularly when the underlying labeled transition system is unbounded, these bisimulation relations can be large and even infinite. The bisimulation-up-to technique has been developed to reduce the size of the relations being computed while retaining soundness, that is, the guarantee of the existence of a bisimulation. Such techniques are increasingly becoming a critical ingredient in the automated checking of bisimilarity. This paper is devoted to the formalization of the meta theory of several major bisimulation-up-to techniques for the process calculi CCS and the π-calculus (with replication). Our formalization is based on recent work on the proof theory of least and greatest fixpoints, particularly the use of relations defined (co-)inductively, and of co-inductive proofs about such relations, as implemented in the Abella theorem prover. An important feature of our formalization is that our definitions of the bisimulation-up-to relations are, in most cases, straightforward translations of published informal definitions, and our proofs clarify several technical details of the informal descriptions. Since the logic behind Abella also supports λ-tree syntax and generic reasoning using the ∇-quantifier, our treatment of the λ-calculus is both direct and natural.


title: A Decision Procedure for Univariate Real Polynomials in Isabelle/HOL

abstract: Sturm sequences are a method for computing the number of real roots of a univariate real polynomial inside a given interval efficiently. In this paper, this fact and a number of methods to construct Sturm sequences efficiently have been formalised with the interactive theorem prover Isabelle/HOL. Building upon this, an Isabelle/HOL proof method was then implemented to prove interesting statements about the number of real roots of a univariate real polynomial and related properties such as non-negativity and monotonicity.


title: Certified Normalization of Context-Free Grammars

abstract: Every context-free grammar can be transformed into an equivalent one in the Chomsky normal form by a sequence of four transformations. In this work on formalization of language theory, we prove formally in the Agda dependently typed programming language that each of these transformations is correct in the sense of making progress toward normality and preserving the language of the given grammar. Also, we show that the right sequence of these transformations leads to a grammar in the Chomsky normal form (since each next transformation preserves the normality properties established by the previous ones) that accepts the same language as the given grammar. As we work in a constructive setting, soundness and completeness proofs are functions converting between parse trees in the normalized and original grammars.


title: Premise Selection and External Provers for HOL4

authors:
Thibault Gauthier
Cezary Kaliszyk

abstract: Learning-assisted automated reasoning has recently gained popularity among the users of Isabelle/HOL, HOL Light, and Mizar. In this paper, we present an add-on to the HOL4 proof assistant and an adaptation of the HOL(y)Hammer system that provides machine learning-based premise selection and automated reasoning also for HOL4. We efficiently record the HOL4 dependencies and extract features from the theorem statements, which form a basis for premise selection. HOL(y)Hammer transforms the HOL4 statements in the various TPTP-ATP proof formats, which are then processed by the ATPs.


title: A Verified Algorithm for Geometric Zonotope/Hyperplane Intersection

abstract: To perform rigorous numerical computations, one can use a generalization of interval arithmetic, namely affine arithmetic (AA), which works with zonotopes instead of intervals. Zonotopes are also widely used for reachability analysis of continuous or hybrid systems, where an important operation is the geometric intersection of zonotopes with hyperplanes.


title: Proving Lock-Freedom Easily and Automatically

authors:
Xiao Jia
Wei Li
Viktor Vafeiadis

abstract: Lock-freedom is a liveness property satisfied by most non-blocking concurrent algorithms. It ensures that at any point at least one thread is making progress towards termination; so the system as a whole makes progress. As a global property, lock-freedom is typically shown by global proofs or complex iterated arguments. We show that this complexity is not needed in practice. By introducing simple loop depth counters into the programs, we can reduce proving lock-freedom to checking simple local properties on those counters. We have implemented the approach in Cave and report on our findings.


title: Certified Connection Tableaux Proofs for HOL Light and TPTP

authors:
Cezary Kaliszyk
Josef Urban
Jirí Vyskocil

abstract: In recent years, the Metis prover based on ordered paramodulation and model elimination has replaced the earlier built-in methods for general-purpose proof automation in HOL4 and Isabelle/HOL. In the annual CASC competition, the leanCoP system based on connection tableaux has however performed better than Metis. In this paper we show how the leanCoP's core algorithm can be implemented inside HOL Light. leanCoP's flagship feature, namely its minimalistic core, results in a very simple proof system. This plays a crucial role in extending the MESON proof reconstruction mechanism to connection tableaux proofs, providing an implementation of leanCoP that certifies its proofs. We discuss the differences between our direct implementation using an explicit Prolog stack,to the continuation passing implementation of MESON present in HOL Light and compare their performance on all core HOL Light goals. The resulting prover can be also used as a general purpose TPTP prover. We compare its performance against the resolution based Metis on TPTP and other interesting datasets.


title: A Typed C11 Semantics for Interactive Theorem Proving

authors:
Robbert Krebbers
Freek Wiedijk

abstract: We present a semantics of a significant fragment of the C programming language as described by the C11 standard. It consists of a small step semantics of a core language, which uses a structured memory model to capture subtleties of C11, such as strict-aliasing restrictions related to unions, that have not yet been addressed by others. The semantics of actual C programs is defined by translation into this core language. We have an explicit type system for the core language, and prove type preservation and progress, as well as type correctness of the translation.


title: Correctness of Isabelle's Cyclicity Checker: Implementability of Overloading in Proof Assistants

abstract: Overloaded constant definitions are an important feature of the proof assistant Isabelle because they allow us to provide Haskell-like type classes to our users. There has been an ongoing question as to under which conditions we can practically guarantee that overloading is a safe theory extension, i.e., preserves consistency or is conservative. The natural condition is that a rewriting system generated by overloaded definitions must always terminate. The current system imposes restrictions on accepted overloaded definitions and decides the termination by an algorithm that is part of the trusted code base of Isabelle. Therefore we aim to prove its correctness.


title: A Framework for Verifying Depth-First Search Algorithms

authors:
Peter Lammich
René Neumann

abstract: Many graph algorithms are based on depth-first search (DFS). The formalizations of such algorithms typically share many common ideas. In this paper, we summarize these ideas into a framework in Isabelle/HOL.


title: A Compositional Semantics for Verified Separate Compilation and Linking

authors:
Tahina Ramananandro
Zhong Shao
Shu-Chun Weng
Jérémie Koenig
Yuchen Fu

abstract: Recent ground-breaking efforts such as CompCert have made a convincing case that mechanized verification of the compiler correctness for realistic C programs is both viable and practical. Unfortunately, existing verified compilers can only handle whole programs---this severely limits their applicability and prevents the linking of verified C programs with verified external libraries. In this paper, we present a novel compositional semantics for reasoning about open modules and for supporting verified separate compilation and linking. More specifically, we replace external function calls with explicit events in the behavioral semantics. We then develop a verified linking operator that makes lazy substitutions on (potentially reacting) behaviors by replacing each external function call event with a behavior simulating the requested function. Finally, we show how our new semantics can be applied to build a refinement infrastructure that supports both vertical composition and horizontal composition.


title: Completeness and Decidability of de Bruijn Substitution Algebra in Coq

authors:
Steven Schäfer
Gert Smolka
Tobias Tebbi

abstract: We consider a two-sorted algebra over de Bruijn terms and de Bruijn substitutions equipped with the constants and operations from Abadi et al.'s sigma-calculus. We consider expressions with term variables and substitution variables and show that the semantic equivalence obtained with the algebra coincides with the axiomatic equivalence obtained with finitely many axioms based on the sigma-calculus. We prove this result with an informative decision algorithm for axiomatic equivalence, which in the negative case returns a variable assignment separating the given expressions in the algebra. The entire development is formalized in Coq.


title: Clean-Slate Development of Certified OS Kernels

abstract: The CertiKOS project at Yale aims to develop new language-based technologies for building large-scale certified system software. Initially, we thought that verifying an OS kernel would require new program logics and powerful proof automation tools, but it should not be much different from standard Hoare-style program verification. After several years of trials and errors, we have decided to take a different path from the one we originally planned. We now believe that building large-scale certified system software requires a fundamental shift in the way we design the underlying programming languages, program logics, and proof assistants. In this talk, I outline our new clean-slate approach, explain its rationale, and describe various lessons and insights based on our experience with the development of several new certified OS kernels.


title: Recording Completion for Certificates in Equational Reasoning

authors:
Thomas Sternagel
Sarah Winkler
Harald Zankl

abstract: We introduce recording completion, a variant of Knuth-Bendix completion which facilitates the construction of certificates for various equational logic proofs (completion proofs, entailment proofs and dis-proofs). The approach generalizes to more powerful variants of completion such as ordered completion and AC completion. We implemented recording completion in the tools KBCV and MKBTT. Both tools allow to choose among different formats of proof certificates, namely conversions, proof trees, and conversions with history. We report on experimental results in which all generated certificates have been verified by the trustable checker CeTA.


title: Formal Reasoning about the C11 Weak Memory Model

abstract: This abstract introduces the C11 weak memory model, summarises known verification results, and discusses some open problems.


title: Formal proofs of transcendence for e and pi as an application of multivariate and symmetric polynomials

authors:
Sophie Bernard
Yves Bertot
Laurence Rideau
Pierre-Yves Strub

abstract: We describe the formalisation in Coq of a proof that the numbers `e` and `pi` are transcendental. This proof lies at the interface of two domains of mathematics that are often considered separately: calculus (real and elementary complex analysis) and algebra. For the work on calculus, we rely on the Coquelicot library and for the work on algebra, we rely on the Mathematical Components library. Moreover, some of the elements of our formalized proof originate in the more ancient library for real numbers included in the Coq distribution. The case of `pi` relies extensively on properties of multivariate polynomials and this experiment was also an occasion to put to test a newly developed library for these multivariate polynomials.


title: Formal verification of control-flow graph flattening

authors:
Sandrine Blazy
Alix Trieu

abstract: Code obfuscation is emerging as a key asset in security by obscurity. It aims at hiding sensitive information in programs so that they become more difficult to understand and reverse engineer. Since the results on the impossibility of perfect and universal obfuscation, many obfuscation techniques have been proposed in the literature, ranging from simple variable encoding to hiding the control-flow of a program. In this paper, we formally verify in Coq an advanced code obfuscation called control-flow graph flattening, that is used in state-of-the-art program obfuscators. Our control-flow graph flattening is a program transformation operating over C programs, that is integrated into the CompCert formally verified compiler. The semantics preservation proof of our program obfuscator relies on a simulation proof performed on a realistic language, the Clight language of CompCert. The automatic extraction of our program obfuscator into OCaml yields a program with competitive results.


title: Higher-order representation predicates in separation logic

abstract: In Separation Logic, representation predicates are used to describe mutable data structures, by establishing a relationship between the entry point of the structure, the piece of heap over which this structure spans, and the logical model associated with the structure. When a data structure is polymorphic, such as in the case of a container, its representation predicate needs to be parameterized not just by the type of the items stored in the structure, but also by the representation predicates associated with these items. Such higher-order representation predicates can be used in particular to control whether containers should own their items. In this paper, we present, through a collection of practical examples, solutions to the challenges associated with reasoning about accesses into data structures that own their elements.


title: Formalization of a newton series representation of polynomials

authors:
Cyril Cohen
Boris Djalal

abstract: We formalize an algorithm to change the representation of a poly- nomial to a Newton power series. This provides a way to compute efficiently polynomials whose roots are the sums or products of roots of other polynomials, and hence provides a base component of efficient computation for algebraic numbers. In order to achieve this, we formalize a notion of truncated power series and develop an abstract theory of poles of fractions.


title: Improving automation in interactive theorem provers by efficient encoding of lambda-abstractions

abstract: Hammers are tools for employing external automated theorem provers (ATPs) to improve automation in formal proof assistants. Strong automation can greatly ease the task of developing formal proofs. An essential component of any hammer is the translation of the logic of a proof assistant to the format of an ATP. For- malisms of state-of-the-art ATPs are usually first-order, so some method for eliminating lambda-abstractions is needed. We present an experimental comparison of several combinatory abstraction al- gorithms for HOL(y)Hammer – a hammer for HOL Light. The al- gorithms are compared on problems involving non-trivial lambda- abstractions selected from the HOL Light core library and a library for multivariate analysis. We succeeded in developing algorithms which outperform both lambda-lifting and the simple Scho ̈nfinkel’s algorithm used in Sledgehammer for Isabelle/HOL. This increases the ATPs’ success rate on translated problems, thus enhancing au- tomation in proof assistants.


title: Constructing the propositional truncation using non-recursive HITs

abstract: In homotopy type theory, we construct the propositional truncation as a colimit, using only non-recursive higher inductive types (HITs). This is a first step towards reducing recursive HITs to non-recursive HITs. This construction gives a characterization of functions from the propositional truncation to an arbitrary type, extending the universal property of the propositional truncation. We have fully formalized all the results in a new proof assistant, Lean.


title: Perspectives on formal verification (invited talk)

abstract: I will discuss the importance, uses, and future directions of formal verification from the point of view of a mathematical foundationalist. These include issues of certainty, proof structure, and (finitary) completeness and decidability.


title: A logic of proofs for differential dynamic logic: toward independently checkable proof certificates for dynamic logics

authors:
Nathan Fulton
André Platzer

abstract: Differential dynamic logic is a logic for specifying and verifying safety, liveness, and other properties about models of cyber-physical systems. Theorem provers based on differential dynamic logic have been used to verify safety properties for models of self-driving cars and collision avoidance protocols for aircraft. Unfortunately, these theorem provers do not have explicit proof terms, which makes the implementation of a number of important features unnecessarily complicated without soundness-critical and extra-logical extensions to the theorem prover. Examples include: an unambiguous separation between proof checking and proof search, the ability to extract program traces corresponding to counter-examples, and synthesis of surely-live deterministic programs from liveness proofs for nondeterministic programs. This paper presents a differential dynamic logic with such an explicit representation of proofs. The resulting logic extends both the syntax and semantics of differential dynamic logic with proof terms -- syntactic representations of logical deductions. To support axiomatic theorem proving, the logic allows equivalence rewriting deep within formulas and supports both uniform renaming and uniform substitutions.


title: Towards a mizar environment for isabelle: foundations and language

authors:
Cezary Kaliszyk
Karol Pak
Josef Urban

abstract: In this paper we explore the possibility of emulating the Mizar environment as close as possible inside the Isabelle logical framework. We introduce adaptations to the Isabelle/FOL object logic that correspond to the logic of Mizar, as well as Isar inner syntax notations that correspond to these of the Mizar language. We show how Isabelle types can be used to differentiate between the syntactic categories of the Mizar language, such as sets and Mizar types including modes and attributes, and show how they interact with the basic constructs of the Tarski-Grothendieck set theory. We discuss Mizar definitions and provide simple abbreviations that allow the introduction of Mizar predicates, functions, attributes and modes using the Isabelle/Pure language elements for introducing definitions and theorems. We finally consider the definite and indefinite description operators in Mizar and their use to introduce definitions by “means” and “equals”. We demonstrate the usability of the environment on a sample Mizar-style formalization, with cluster inferences and “by” steps performed manually.


title: The vampire and the FOOL

authors:
Evgenii Kotelnikov
Laura Kovács
Giles Reger
Andrei Voronkov

abstract: This paper presents new features recently implemented in the theorem prover Vampire, namely support for first-order logic with a first class boolean sort (FOOL) and polymorphic arrays. In addition to having a first class boolean sort, FOOL also contains if-then-else and let-in expressions. We argue that presented extensions facilitate reasoning-based program analysis, both by increasing the expressivity of first-order reasoners and by gains in efficiency.


title: Refinement based verification of imperative data structures

abstract: In this paper we present a stepwise refinement based top-down approach to verified imperative data structures. Our approach is modular in the sense that already verified data structures can be used for construction of more complex data structures. Moreover, our data structures can be used as building blocks for the verification of algorithms. Our tool chain supports refinement down to executable code in various programming languages, and is fully implemented in Isabelle/HOL, such that its trusted code base is only the inference kernel and the code generator of Isabelle/HOL. As a case study, we verify an indexed heap data structure, and use it to generate an efficient verified implementation of Dijkstra's algorithm.


title: A modular, efficient formalisation of real algebraic numbers

authors:
Wenda Li
Lawrence C. Paulson

abstract: This paper presents a construction of the real algebraic numbers with executable arithmetic operations in Isabelle/HOL. Instead of verified resultants, arithmetic operations on real algebraic numbers are based on a decision procedure to decide the sign of a bivariate polynomial (with rational coefficients) at a real algebraic point. The modular design allows the safe use of fast external code. This work can be the basis for decision procedures that rely on real algebraic numbers.


title: Dependent type practice (invited talk)

abstract: Dependent type theory is a powerful and expressive language for writing mathematical expressions and proofs, but careful design, engineering, and hard work are needed to put the theory into practice. In this talk, I will discuss some of the ideas and techniques that have been used in the design of the Lean theorem prover, a new proof system based on dependent type theory that aims to make the theorem proving process more natural, convenient, and efficient.


title: Bisimulation up-to techniques for psi-calculi

authors:
Johannes Åman Pohjola
Joachim Parrow

abstract: Psi-calculi is a parametric framework for process calculi similar to popular pi-calculus extensions such as the explicit fusion calculus, the applied pi-calculus and the spi calculus. Remarkably, machine-checked proofs of standard algebraic and congruence properties of bisimilarity apply to all calculi within the framework. Bisimulation up-to techniques are methods for reducing the size of relations needed in bisimulation proofs. In this paper, we show how these bisimulation proof methods can be adapted to psi-calculi. We formalise all our definitions and theorems in Nominal Isabelle, and show examples where the use of up to-techniques yields drastically simplified proofs of known results. We also prove new structural laws about the replication operator.