编程语言
We present a thread-modular abstract interpretation(TMAI) technique to verify programs under the release-acquire (RA) memory model for safety property violations. The main contributions of our work are: we capture the execution order of…
This paper explores the limits of the current generation of large language models for program synthesis in general purpose programming languages. We evaluate a collection of such models (with between 244M and 137B parameters) on two new…
We give thread-modular non-relational value analyses as abstractions of a local trace semantics. The semantics as well as the analyses are formulated by means of global invariants and side-effecting constraint systems. We show that a…
Assertion checking is an invaluable programmer's tool for finding many classes of errors or verifying their absence in dynamic languages such as Prolog. For Prolog programmers this means being able to have relevant properties such as modes,…
We study a dependently typed extension of a multi-stage programming language \`a la MetaOCaml, which supports quasi-quotation and cross-stage persistence for manipulation of code fragments as first-class values and an evaluation construct…
This paper complements "Writing R Extensions," the official guide for writing R extensions, for those interested in developing R packages using Rust. It highlights idiosyncrasies of R and Rust that must be addressed by any integration and…
The functional correspondence is a manual derivation technique transforming higher-order evaluators into the semantically equivalent abstract machines. The transformation consists of two well-known program transformations: translation to…
In this paper we present a new static data type inference algorithm for logic programming. Without the need of declaring types for predicates, our algorithm is able to automatically assign types to predicates which, in most cases,…
Modern separation logics allow one to prove rich properties of intricate code, e.g. functional correctness and linearizability of non-blocking concurrent code. However, this expressiveness leads to a complexity that makes these logics…
Whitby is the server-side of an Intelligent Tutoring System application for learning System-Theoretic Process Analysis (STPA), a methodology used to ensure the safety of anything that can be represented with a systems model. The underlying…
This paper explores the integration of hypothetical reasoning into an efficient implementation of the fuzzy logic language Bousi~Prolog. To this end, we first analyse what would be expected from a logic inference system, equipped with what…
We present an extension to a certified financial contract management system that allows for templated declarative financial contracts and for integration with financial stochastic models through verified compilation into so-called…
The extension of classical imperative programs with real-valued random variables and random branching gives rise to probabilistic programs. The termination problem is one of the most fundamental liveness properties for such programs. The…
Erasure coding (EC) affords data redundancy for large-scale systems. XOR-based EC is an easy-to-implement method for optimizing EC. This paper addresses a significant performance gap between the state-of-the-art XOR-based EC approach (with…
The popularity of smart contracts is on the rise, yet breaches in reliability and security linger. Among the many facets of smart contract reliability, we concentrate on faults rooted in out-of-order interactions with contract endpoints. We…
We consider the almost-sure (a.s.) termination problem for probabilistic programs, which are a stochastic extension of classical imperative programs. Lexicographic ranking functions provide a sound and practical approach for termination of…
A reliable technique for deductive program verification should be proven sound with respect to the semantics of the programming language. For each different language, the construction of a separate soundness proof is often a laborious…
We propose a simple calculus for processing data streams (infinite flows of data series), represented by finite sets of equations built on stream operators. Furthermore, functions defining streams are regularly corecursive, that is, cyclic…
We contemplate this article to help the teachers of programming in his aspiration for giving some appropriate and interesting examples. The work will be especially useful for students-future programmers, and for their lecturers. Some of the…
We enhance the calculus of string diagrams for monoidal categories with hierarchical features in order to capture closed monoidal (and cartesian closed) structure. Using this new syntax we formulate an automatic differentiation algorithm…