an independent field guide to 23 million papers from arXiv & OpenAlex — not affiliated with arXiv.org
Author
6 papers · 2011–2026
showing 1–6 of 6 RSS
A. Bijlsma, Kees Huizing, Ruurd Kuiper +3 more
Learning how to design and implement a program is hard. Teaching methods and textbooks on Java programming often treat a new subject in terms of syntax and examples. Little attention is paid to systematically designing programs with these new concepts. Research has shown that such a complex task requires not only conceptual knowledge, but also explicit procedural support.
Wieger Wesselink, Kees Huizing, Huub van de Wetering
Formal verification of complex algorithms requires expertise in program specification, invariant construction, mathematical proof, and the management of automated theorem provers. Although large language models (LLMs) can generate program code and proof fragments, reliably developing complete machine-checked verifications remains challenging: it requires an iterative process of constructing and validating specifications and invariants, building proofs, diagnosing solver failures, and optimizing verification performance. This paper presents a systematic ten-step workflow for LLM-assisted verification of scientific algorithms using the Dafny verification system. The workflow integrates algorithm formalization, contract development, empirical invariant validation, proof construction, bottleneck profiling, and resource-driven proof optimization. We applied the workflow using Antrhopic's…
Wieger Wesselink, Kees Huizing, Huub van de Wetering
Minimax-based search algorithms with alpha-beta pruning and transposition tables are a central component of classical game-playing engines and remain widely used in practice. Despite their widespread use, these algorithms are subtle, highly optimized, and notoriously difficult to reason about, making non-obvious errors hard to detect by testing alone. Using the Dafny verification system, we formally verify a range of minimax search algorithms, including variants with alpha-beta pruning and transposition tables. For depth-limited search with transposition tables, we introduce a witness-based correctness criterion that captures when returned values can be justified by an explicit game-tree expansion. We apply this criterion to two practical variants of depth-limited negamax with alpha-beta pruning and transposition tables: for one variant, we obtain a fully mechanized correctness proof…
Harrie Passier, Lex Bijlsma, Ruurd Kuiper +1 more
To improve the quality of programs we provide an approach to guidance in the process of program development. At the higher level the various activities and their dependencies to structure the process are identified. At the lower level, detailed, practical rules are given for the decision-making in the development steps during these activities. The approach concentrates on structure and behavior of a single class. It includes design and specification and is compatible with methodologies for programming in the large. Informal specifications are introduced to help develop correct and robust code as well as corresponding tests. A strict distinction is made between external design and specification on one hand and internal design and specification on the other hand, which helps in keeping control over complexity. The approach also exploits the separation of success and failure scenarios. A…
A proof system is presented for the verification and derivation of object oriented pro-grams with as main features strong typing, dynamic binding, and inheritance. The proof system is inspired on Meyer’s system of class invariants [12] and remedies its unsound-ness, which is already recognized by Meyer. Dynamic binding is treated in a flexible way: when throughout the class hierarchy overriding methods respect the pre- and post-conditions of the overridden methods, very simple proof rules for method calls suffice; more powerful proof rules are supplied for cases where one cannot or does not want to follow this restriction. The proof system is complete relative to proofs for properties of pointers and the data domain. 1
Ho Metacomputing, Jini Lookup, Dirk Gorissen +6 more
in the United States and other countries. ServiceUI is a trademark of Artima Software, Inc and Linux is a trademark of Linus Torvalds. All other trademarks are the property of their respective owners. License