Neural Network Verification is a Programming Language Challenge

2025-01-30T14:12:35Z

Neural network verification is a new and rapidly developing field of research. So far, the main priority has been establishing efficient verification algorithms and tools, while proper support from the programming language perspective has been considered secondary or unimportant. Yet, there is mounting evidence that insights from the programming language community may make a difference in the future development of this domain. In this paper, we formulate neural network verification challenges as programming language challenges and suggest possible future solutions.

Exo 2: Growing a Scheduling Language

2025-01-30T04:19:54Z

User-schedulable languages (USLs) help programmers productively optimize programs by providing safe means of transforming them. Current USLs are designed to give programmers exactly the control they want, while automating all other concerns. However, there is no universal answer for what performance-conscious programmers want to control, how they want to control it, and what they want to automate, even in relatively narrow domains. We claim that USLs should, instead, be designed to grow. We present Exo 2, a scheduling language that enables users to define new scheduling operations externally to the compiler. By composing a set of trusted, fine-grained primitives, users can safely write their own scheduling library to build up desired automation. We identify actions (ways of modifying code), inspection (ways of interrogating code), and references (ways of pointing to code) as essential for any user-extensible USL. We fuse these ideas into a new mechanism called Cursors that enables the creation of scheduling libraries in user code. We demonstrate libraries that amortize scheduling effort across more than 80 high-performance kernels, reducing total scheduling code by an order of magnitude and delivering performance competitive with state-of-the-art implementations on three different platforms.

Coverage Semantics for Dependent Pattern Matching

2025-01-30T01:57:19Z

Dependent pattern matching is a key feature in dependently typed programming. However, there is a theory-practice disconnect: while many proof assistants implement pattern matching as primitive, theoretical presentations give semantics to pattern matching by elaborating to eliminators. Though theoretically convenient, eliminators can be awkward and verbose, particularly for complex combinations of patterns. This work aims to bridge the theory-practice gap by presenting a direct categorical semantics for pattern matching, which does not elaborate to eliminators. This is achieved using sheaf theory to describe when sets of arrows (terms) can be amalgamated into a single arrow. We present a language with top-level dependent pattern matching, without specifying which sets of patterns are considered covering for a match. Then, we give a sufficient criterion for which pattern-sets admit a sound model: patterns should be in the canonical coverage for the category of contexts. Finally, we use sheaf-theoretic saturation conditions to devise some allowable sets of patterns. We are able to express and exceed the status quo, giving semantics for datatype constructors, nested patterns, absurd patterns, propositional equality, and dot patterns.

Gray-Box Fuzzing in Local Space

2025-01-29T23:17:50Z

We consider gray-box fuzzing of a program instrumented such that information about evaluation of program expressions converting values of numerical types to Boolean, like x <= y, is recorded during each program's execution. Given that information for an executed program path, we formally define the problem for finding input such that program's execution with that input evaluates all those expressions in the same order and with the same Boolean values as in the original execution path, except for the last one, which is evaluated to the opposite value. Then we also provide an algorithm searching for a solution of the problem effectively. The effectiveness of the algorithm is demonstrated empirically via its evaluation on the TestComp 2024 benchmark suite.

SMT-Boosted Security Types for Low-Level MPC

2025-01-29T18:16:20Z

Secure Multi-Party Computation (MPC) is an important enabling technology for data privacy in modern distributed applications. We develop a new type theory to automatically enforce correctness,confidentiality, and integrity properties of protocols written in the \emph{Prelude/Overture} language framework. Judgements in the type theory are predicated on SMT verifications in a theory of finite fields, which supports precise and efficient analysis. Our approach is automated, compositional, scalable, and generalizes to arbitrary prime fields for data and key sizes.

Iso-Recursive Multiparty Sessions and their Automated Verification -- Technical Report

2025-01-29T17:14:29Z

Most works on session types take an equi-recursive approach and do not distinguish among a recursive type and its unfolding. This becomes more important in recent type systems which do not require global types, also known as generalised multiparty session types (GMST). In GMST, in order to establish properties as deadlock-freedom, the environments which type processes are assumed to satisfy extensional properties holding in all infinite sequences. This is a problem because: (1) the mechanisation of GMST and equi-recursion in proof assistants is utterly complex and eventually requires co-induction; and (2) the implementation of GMST in type checkers relies on model checkers for environment verification, and thus the program analysis is not self-contained. In this paper, we overcome these limitations by providing an iso-recursive typing system that computes the behavioural properties of environments. The type system relies on a terminating function named compliance that computes all final redexes of an environment, and determines when these redexes do not contain mismatches or deadlocks: compliant environments cannot go wrong. The function is defined theoretically by introducing the novel notions of deterministic LTS of environments and of environment closure, and can be implemented in mainstream programming languages and compilers. We showcase an implementation in OCaml by using exception handling to tackle the inherent non-determinism of synchronisation of branching and selection types. We assess that the implementation provides the desired properties, namely absence of mismatches and of deadlocks in environments, by resorting to automated deductive verification performed in tools of the OCaml ecosystem relying on Why3.

Multiparty Session Typing, Embedded (Technical Report)

2025-01-29T16:28:19Z

Multiparty session typing (MPST) is a method to make concurrent programming simpler. The idea is to use type checking to automatically detect safety and liveness violations of implementations relative to specifications. In practice, the premier approach to combine MPST with mainstream languages -- in the absence of native support -- is based on external DSLs and associated tooling. In contrast, we study the question of how to support MPST by using internal DSLs. Answering this question positively, this paper presents the mpst.embedded library: it leverages Scala's lightweight form of dependent typing, called match types, to embed MPST directly into Scala. Our internal-DSL-based approach avoids programming friction and leaky abstractions of the external-DSL-based approach for MPST.

PolyQEnt: A Polynomial Quantified Entailment Solver

2025-01-29T12:03:55Z

Polynomial quantified entailments with existentially and universally quantified variables arise in many problems of verification and program analysis. We present PolyQEnt which is a tool for solving polynomial quantified entailments in which variables on both sides of the implication are real valued or unbounded integers. Our tool provides a unified framework for polynomial quantified entailment problems that arise in several papers in the literature. Our experimental evaluation over a wide range of benchmarks shows the applicability of the tool as well as its benefits as opposed to simply using existing SMT solvers to solve such constraints.

Programming in Brazilian Higher Education and High School: A Systematic Literature Review

2025-01-28T20:16:34Z

Programming, which is both economically significant and mentally stimulating, has been found to benefit the aging brain and to enhance cognitive function at various educational levels. Despite its advantages, challenges persist in standardizing and implementing programming education effectively across both the higher and secondary education levels in Brazil. To shed light on these issues, we carried out a systematic review of programming teaching methods in the Brazilian context, examining gaps, common techniques, approaches, and action opportunities in programming education. Our findings provide valuable recommendations for educational policymakers and educators to develop effective and updated national policies to teach programming.

A Comprehensive Survey of the Lean 4 Theorem Prover: Architecture, Applications, and Advances

2025-01-28T17:15:54Z

This comprehensive survey examines Lean 4, a state-of-the-art interactive theorem prover and functional programming language. We analyze its architectural design, type system, metaprogramming capabilities, and practical applications in formal verification and mathematics. Through detailed comparisons with other proof assistants and extensive case studies, we demonstrate Lean 4's unique advantages in proof automation, performance, and usability. The paper also explores recent developments in its ecosystem, including libraries, tools, and educational applications, providing insights into its growing impact on formal methods and mathematical formalization.

An Automata-theoretic Basis for Specification and Type Checking of Multiparty Protocols

2025-01-28T14:17:58Z

We propose the Automata-based Multiparty Protocols framework (AMP) for top-down protocol development. The framework features a new very general formalism for global protocol specifications called Protocol State Machines (PSMs), Communicating State Machines (CSMs) as specifications for local participants, and a type system to check a $π$-calculus with session interleaving and delegation against the CSM specification. Moreover, we define a large class of PSMs, called "tame", for which we provide a sound and complete PSPACE projection operation that computes a CSM describing the same protocol as a given PSM if one exists. We propose these components as a backwards-compatible new backend for frameworks in the style of Multiparty Session Types. In comparison to the latter, AMP offers a considerable improvement in expressivity, decoupling of the various components (e.g. projection and typing), and robustness (thanks to the complete projection).

Type-Based Approaches to Rounding Error Analysis

2025-01-27T23:38:34Z

This dissertation explores the design and implementation of programming languages that represent rounding error analysis through typing. In the first part of this dissertation, we demonstrate that it is possible to design languages for forward error analysis with NumFuzz, a functional programming language whose type system expresses quantitative bounds on rounding error. This type system combines a sensitivity analysis, enforced through a linear typing discipline, with a novel graded monad to track the accumulation of rounding errors. We establish the soundness of the type system by relating the denotational semantics of the language to both an exact and floating-point operational semantics. To demonstrate the practical utility of NumFuzz as a tool for automated error analysis, we have developed a prototype implementation capable of automatically inferring error bounds. Our implementation produces bounds competitive with existing tools, while often achieving significantly faster analysis times. In the second part of this dissertation, we explore a type-based approach to backward error analysis with Bean, a first-order programming language with a linear type system that can express quantitative bounds on backward error. Bean's type system combines a graded coeffect system with strict linearity to soundly track the flow of backward error through programs. To illustrate Bean's potential as a practical tool for automated backward error analysis, we implement a variety of standard algorithms from numerical linear algebra in Bean, establishing fine-grained backward error bounds via typing in a compositional style. We also develop a prototype implementation of Bean that infers backward error bounds automatically. Our evaluation shows that these inferred bounds match worst-case theoretical relative backward error bounds from the literature.

A Modular Program-Transformation Framework for Reducing Specifications to Reachability

2025-01-27T18:49:11Z

Software verification is a complex problem, and verification tools need significant tuning to achieve high performance. Due to this, many verifiers choose to specialize on reachability properties, or invest the time to implement known transformations from the given specification to reachability on their internal representations. To improve this situation, we provide transformations as stand-alone components, modifying the input program instead of the internal representation, enabling their usage as a preprocessing step by other verifiers. This way, we separate two concerns: improving the performance of reachability analyses and implementing efficient transformations of arbitrary specifications to reachability. We implement the transformations in a framework that is based on instrumentation automata, inspired by the BLAST query language. In our initial study, we support three important concrete specifications for C programs: termination, no-overflow, and memory cleanup. Moreover, we discuss the broader expressiveness of our framework and show how general liveness properties can be transformed to reachability. We demonstrate the effectiveness and efficiency of our transformations by comparing verifiers that support the specifications natively with verifiers for reachability applied on the transformed programs. The results are very promising: Our transformations can extend existing verifiers to be effective on specifications that they do not support natively, and that the efficiency is often similar to verifiers that natively support the considered specifications.

A Survey of Neural Code Intelligence: Paradigms, Advances and Beyond

2025-01-26T10:48:44Z

Neural Code Intelligence -- leveraging deep learning to understand, generate, and optimize code -- holds immense potential for transformative impacts on the whole society. Bridging the gap between Natural Language and Programming Language, this domain has drawn significant attention from researchers in both research communities over the past few years. This survey presents a systematic and chronological review of the advancements in code intelligence, encompassing over 50 representative models and their variants, more than 20 categories of tasks, and an extensive coverage of over 680 related works. We follow the historical progression to trace the paradigm shifts across different research phases (e.g., from modeling code with recurrent neural networks to the era of Large Language Models). Concurrently, we highlight the major technical transitions in models, tasks, and evaluations spanning through different stages. For applications, we also observe a co-evolving shift. It spans from initial endeavors to tackling specific scenarios, through exploring a diverse array of tasks during its rapid expansion, to currently focusing on tackling increasingly complex and varied real-world challenges. Building on our examination of the developmental trajectories, we further investigate the emerging synergies between code intelligence and broader machine intelligence, uncovering new cross-domain opportunities and illustrating the substantial influence of code intelligence across various domains. Finally, we delve into both the opportunities and challenges associated with this field, alongside elucidating our insights on the most promising research directions. An ongoing, dynamically updated project and resources associated with this survey have been released at https://github.com/QiushiSun/Awesome-Code-Intelligence.

Transformers are Efficient Compilers, Provably

2025-01-25T04:05:56Z

Transformer-based large language models (LLMs) have demonstrated surprisingly robust performance across a wide range of language-related tasks, including programming language understanding and generation. In this paper, we take the first steps towards a formal investigation of using transformers as compilers from an expressive power perspective. To this end, we introduce a representative programming language, Mini-Husky, which encapsulates key features of modern C-like languages. We show that if the input code sequence has a bounded depth in both the Abstract Syntax Tree (AST) and type inference (reasonable assumptions based on the clean code principle), then the number of parameters required by transformers depends only on the logarithm of the input sequence length to handle compilation tasks, such as AST construction, symbol resolution, and type analysis. A significant technical challenge stems from the fact that transformers operate at a low level, where each layer processes the input sequence as raw vectors without explicitly associating them with predefined structure or meaning. In contrast, high-level compiler tasks necessitate managing intricate relationships and structured program information. Our primary technical contribution is the development of a domain-specific language, Cybertron, which generates formal proofs of the transformer's expressive power, scaling to address compiler tasks. We further establish that recurrent neural networks (RNNs) require at least a linear number of parameters relative to the input sequence, leading to an exponential separation between transformers and RNNs. Finally, we empirically validate our theoretical results by comparing transformers and RNNs on compiler tasks within Mini-Husky.