Elpi is a higher-order logic programming language derived from λ Prolog and widely used to extend the Rocq interactive theorem prover. Typical users are familiar with types and functional programming but often lack experience with backtracking. We introduce a language of signatures to declare that a predicate is operationally deterministic, meaning that calling the predicate does not leave any choice points. The signature language handles higher-order programs and dynamic programs. We present a static analyzer that verifies these signatures and report its application to the majority of public Elpi code in the Rocq ecosystem.
Static program verification tools are essential for ensuring software correctness and reliability without executing the code. However, their effectiveness relies heavily on precise configuration, which must be tailored to specific project requirements, coding standards, and quality objectives. Selecting appropriate configurations is challenging due to the unique properties of each codebase and the need for an in-depth understanding of the analysis techniques. Current methods often default to standard settings or rely on random exploration, leading to sub-optimal results. In this paper, we introduce ConfigTuneX, a novel rule-based machine learning approach that optimizes configuration settings in static program verification tools through composite FOLD-SE rules. These rules simultaneously address two critical challenges: (1) reducing inconclusive outcomes by distinguishing unresolved cases from resolved outcomes, and (2) improving verification accuracy by separating correct outcomes from incorrect ones. The extracted rules are transformed into stratified answer set program (ASP) compatible with the s(CASP) solver, which systematically generates counterfactual configurations to avoid undesired outcomes. This targeted reasoning narrows the search space to the most promising configurations, reducing computational overhead while enhancing both interpretability and effectiveness. Experimental results show that ConfigTuneX with composite FOLD-SE rules consistently outperforms the state-of-the-art baseline across verification tools. On Jayhorn, CBMC, and Symbiotic, ConfigTuneX improves success rates by 76.34
Answer Set Programming with Quantifiers (ASP(Q)) extends classical ASP to naturally capture problems within the polynomial hierarchy (PH). Recently, the formalism has been enriched with weak constraints to express both local and global optimization criteria, enabling the modeling of problems in _n+1^P . In this paper, we present the first implementation of ASP(Q) with global weak constraints, built on top of the state-of-the-art ASP(Q) system PyQASP, based on an upper-bound improving strategy that effectively guides the search toward optimal solutions. Experiments demonstrate that our approach can be effectively applied to solve hard optimization problems.
Functional reactive programming (FRP) is a programming paradigm for implementing software that continuously interacts with its environment and manipulates highly dynamic data. Asynchronous FRP, in particular, is very expressive and can be used to implement graphical user interfaces and other reactive systems interacting with data streams and events that are not synchronized. Testing such asynchronous FRP programs is difficult since a program’s behaviour depends not only on the concrete data it receives from its environment but also the relative timing of when each piece of data arrives. In this paper, we propose PropRatt, a property-based testing framework for asynchronous FRP. The key component of PropRatt is its specification language, which extends basic linear temporal logic with a means to express properties of several concurrent signals. This allows us to express temporal properties that relate data coming from different signals at different points in time. PropRatt is implemented in Haskell and targets a recently introduced asynchronous FRP language embedded in Haskell. We demonstrate the utility of PropRatt through a case study testing a signal combinator library as well as a graphical user interface, in which we suggest how the strategy for generating signals can be modified to better model specific domains.
Various approaches to solving set theory constraints exist, for example within verification tools for the TLA+ and B formal methods. In this paper we present a way to solve set theory constraints in general and B formulas in particular using SAT solvers, by using Prolog technology. First, a preliminary analysis uses CLP(FD) constraint solving to infer finite bounds for decision variables. Second, Prolog translation rules map constraints to answer set programming (ASP), by encoding logical and set-theoretic operators as Horn clauses. Finally, the Clingo tool translates the ASP encoding to SAT to produce ASP models, which we translate back to set theory and B using Prolog DCG rules. The scheme of the paper has been implemented in SICStus Prolog, as an alternate backend for the ProB validation tool. We evaluate the new backend on a series of benchmarks. Our paper highlights the usefulness of Prolog, for analysis, inference and transformation rules and ASP as a high-level interface to SAT solving.
