Parallelization of programs is of essence in the high-performance computing (HPC) area. But parallelization is only correct if certain data dependences can be reliably excluded, for example, read-after-write dependences, where a read access occurs as the subsequent access on a data element after a write access. Data dependence analyses should not merely be correct, but as precise as possible, so as not to miss any opportunity for parallelization. Various dynamic and static analyses were proposed in the HPC community, but, until recently, none based on program logic and deductive verification, even though the latter approach has important advantages, including soundness, precision, and modularity. Previously a proof-of-concept was given that fully automatic dependence analysis based on deductive verification is possible, but it suffered from limitations that rendered it impractical: the restriction to one-dimensional arrays and flat loops and, importantly, it does not differentiate between inter- and intra-iteration data dependences, which often results in a loss of precision. In this paper we lift all three limitations and show that a deductive approach is a competitive alternative to the kinds of dependence analyses used hitherto in HPC. Our axiomatization in a deduction system constitutes the first formalization of the semantics of inter-iteration dependence.
We demonstrate the benefit of computer assisted reasoning by proving correctness of some matching algorithms for regular expressions. We give a brief survey of the VeriFun system used for verification, illustrate the problem, discuss the computation and usage of derivatives, present the machine assisted proofs and report on the effort for creating them.
Existing active automata learning (AAL) algorithms have demonstrated their potential in capturing the behavior of complex systems (e.g., in analyzing network protocol implementations). The most widely used AAL algorithms generate finite state machine models, such as Mealy machines or deterministic finite automata. For many analysis tasks, however, it is crucial to generate richer classes of models that also show how relations between data parameters affect system behavior. Such models have shown potential to uncover critical bugs, but their learning algorithms do not scale beyond small and well curated experiments. In this article, we present SL^λ , an effective and scalable register automata (RA) learning algorithm that significantly reduces the number of membership queries required for inferring models. It achieves this by combining a tree-based cost-efficient data structure with mechanisms for computing short and restricted tests. We prove that SL^λ is guaranteed to learn an acceptor, in the form of a register automaton with n locations and t transitions, for a given data language of finite index, and that it can do so with at most O(t^2 (2n)^n + m t^2 m^m) membership queries and O(t) equivalence queries, where m is the length of the longest counterexample received during learning. We have implemented SL^λ as a new algorithm in RALib. We evaluate its performance by comparing it against SL^* , the current state-of-the-art RA learning algorithm. Experiments on a series of benchmarks show that it reduces the number of membership queries by up to an order of magnitude, and also shows substantial asymptotic improvements in bigger systems.
Non-degenerate conditions (NDGs) are essential prerequisites that ensure the validity of geometric theorems. While algebraic methods such as Wu’s method generate NDGs in polynomial form and provide geometric interpretations, these interpretations are often not expressed in terms of intuitive geometric quantities, such as lengths, angles, and areas, and instead remain peripheral annotations. Consequently, such NDGs are rarely integrated into the core geometric reasoning process. This paper proposes a methodology based on complex number identities to provide a unifying viewpoint for interpreting NDGs in the following settings. First, we systematically transform algebraic NDGs into expressions involving explicit geometric quantities, thereby incorporating them more directly into the reasoning chain. Second, by leveraging these geometric-quantity-based NDGs, we progressively connect the given conditions to the conclusion, ultimately deriving complex number identities that unify the original theorem, its converse, and quantitative extensions. Experimental evaluation on over 100 geometric problems, including classical theorems and Olympiad-level challenges, indicates that more than 90
We present a formalization in Lean4 of some multi-graded algebraic geometry constructions, focusing on the Brenner–Schröer Proj construction and algebraic dilatations of rings. Multi-graded Proj schemes, defined from rings graded by more general monoids than ℕ or ℤ , have recently attracted increasing attention and play an important role in several areas of modern algebraic geometry. Our work follows the algebraic approach developed in the literature and provides a formal implementation of multi-graded Proj within the Lean4 theorem prover. In addition, we formalize dilatations of rings, an operation in commutative algebra closely related to localization and to blowup constructions. This article gives a comprehensive account of the definitions, main results, and design choices underlying the formalization. It is intended both as documentation of the development and as a foundation for future extensions in formalized algebraic geometry. The corresponding code is made publicly available, supporting further developments in the formalization of advanced geometric structures.
