Programming languages with uniqueness type systems prevent pointer aliasing, simplifying memory safety reasoning. However, code implemented in these languages often interoperates through foreign function interfaces with external components implemented in languages lacking the same level of static safety guarantees. To verify safe updates in a combined system, one must manually verify that the external components preserve the safety invariants of the uniqueness type system. In particular, recent work showed that one can manually discharge such obligations on C components from a cross-language Cogent-C system by directly reasoning about the C code in higher-order logic. However, even for simple examples, discharging the uniqueness safety obligations, known as frame conditions, within a logic not specifically designed for direct reasoning in terms of heaps and pointers was not ideal. Separation logic is an established logic that facilitates reasoning about imperative programs by localising reasoning to the parts of the heap that the program mutates. This raises a vital question. Can we use separation logic to discharge the safety obligations imposed by uniqueness types? The answer is yes. This paper demonstrates that the frame conditions can be inferred from particular separation logic triples and, hence, discharged by reasoning using separation logic. We identify and verify the soundness of specific separation logic triples that imply the frame conditions imposed by a uniqueness type system.
As High-Performance Computing (HPC) workloads increasingly migrate to cloud infrastructures, the need for intelligent, inference-time adaptive scheduling becomes critical. Conventional schedulers such as FCFS or SJF often struggle to adapt to the heterogeneous and dynamic nature of cloud-based systems, leading to inefficient resource utilization and increased job wait times. This paper proposes a multi-stage AI-based pipeline to address these challenges through the integration of three core capabilities: job runtime prediction using supervised learning, anomaly detection via deep autoencoders, and adaptive resource scheduling using reinforcement learning. Leveraging real-world data from the MIT SuperCloud dataset, our system extracts meaningful patterns from time-series telemetry to support informed scheduling decisions. The job prediction module estimates runtimes based on CPU utilization, memory consumption, and I/O statistics. The anomaly detection module flags abnormal jobs using learned GPU performance norms. The RL scheduler dynamically matches jobs to compute nodes based on predicted duration and anomaly status, optimizing for turnaround time and utilization. Experimental evaluations demonstrate a 28
Tensor program optimization is a non-convex optimization problem, and efficiently solving it while balancing optimization efficiency and execution performance remains a challenging task. Search-based tensor program compilers have proven effective by constructing large-scale exploration spaces that include potentially high-performance program variants, thus overcoming the performance bottlenecks of traditional program optimization methods. However, these approaches still face significant challenges in search strategies, as existing compilers often require hours or even days to identify the optimal program representation. This paper proposes ELTC, an end-to-end tensor program compilation framework based on large language models (LLMs), designed for efficient optimization of tensor programs in deep neural networks. ELTC formulates the tensor program exploration problem as a generation task for language models. By training a large language model offline, it generates transformation sequences for tensor programs in an end-to-end manner based on their feature representations. While preserving the broad search space, this approach significantly improves optimization efficiency. Moreover, we introduce a language-model-friendly intermediate representation, which encodes key features of tensor programs using structured textual formats. Based on this representation, we construct a tensor program dataset tailored for language models. Experimental results demonstrate that ELTC achieves superior performance in both optimization quality and tuning speed. Compared with the fully converged Ansor-TenSet, ELTC achieves a 34.07× compilation speedup and an average performance improvement of 1.06× under convergence conditions. Furthermore, ELTC outperforms the manually optimized kernel library TensorRT, achieving a 1.3× performance gain.
In logical reasoning, specification inference attempts to synthesize an explanatory hypothesis from a given conclusion. We consider the specification synthesis problem for database-backed web-applications where only an oracle access to the application is available. Such is a real case for test teams where they are not provided access to the application. Our algorithm begins with an initial hypothesis constructed from responses of the web-application on a sampled dataset, and then improves this hypothesis iteratively via carefully constructed queries to the application (via an SMT solver). Finally, statistical tests are used to validate the soundness and maximality of the constructed hypothesis. We implement our algorithm in a tool, Vivaran, and demonstrate its capabilities on a large web-based enterprise resource planning (ERP) software. Vivaran infers semantically equivalent specifications as the ground-truth in all cases.
Probabilistic programs with sampling and scoring are used to write probabilistic models to make probabilistic inferences. Despite their effectful nature, such programs can actually be verified by means of equational reasoning. We propose a formal foundation in the Rocq prover to mechanize such verifications. For that purpose, we extend an existing library for Lebesgue integration and formalize standard probability distributions. Using the resulting library, we extend the intrinsically-typed syntax and the kernel-based semantics of an encoding of a probabilistic programming language. Thanks to these extensions, we mechanize the main running examples of Shan's tutorial on equational reasoning for probabilistic programming at POPL 2018's TutorialFest.
