arXiv subjects

Alex Potanin

Publications and source records attributed to Alex Potanin.

17 recordsLinked to original sources

arXiv2026

Reshaping Undergraduate Computer Science Education in the Generative AI Era

Generative AI represents a turning point for Computer Science (CS) education. In recent decades, post-secondary CS education has largely focused on what has been seen as practical software engineering skills: implementation-level programming, debugging, testing, and software design, analysis, and documentation. However, this framing is becoming less tenable as generative AI automates many of these tasks, challenging their centrality in CS education. To keep pace with advances in AI technology, CS curricula should consider a shift toward understanding and verifying AI-generated artifacts. This white paper outlines the findings of two international NUS-Google Workshops in Singapore, where we convened faculty members, industry practitioners, and students, and proposes a strategic response to reshape how CS should be taught at the undergraduate level. Based on the findings, we identify critical skills that must be preserved and those that are becoming less important. By incorporating these skills as "breadcrumbs," we can provide helpful nudges and engaging exercises within the current curriculum, enhancing learning experiences for everyone. We believe that to effectively prepare future computer science graduates, capable of creating, solving problems, and managing, as well as co-creating, artifacts with AI. It is important to consider a shift in curricula. Emphasizing system design, abstraction, and critical evaluation could greatly enhance their education and readiness for the challenges ahead. We propose prerequisites for solutions to reform CS education by fostering AI-native competencies, re-centering fundamental education, enhancing advanced pathways, embracing new pedagogies, and shifting institutional support.

cs.CY↗

arXiv2026

React-ing to Grace Hopper 200: Five Open-Weights Coding Models, One React Native App, One GH200, One Weekend

We evaluate five state-of-the-art open-weights coding language models -- Kimi-K2.5 (at Q3 and Q4 quantizations), GLM-5.1, Qwen3-Coder-480B, and DeepSeek-V3.2 -- on a single multi-file React Native application generation task on NVIDIA GH200 576 GB hardware. The task specifies authentication, per-user per-day counting, and web compatibility, and is evaluated on whether the generated project runs out-of-the-box and on feature-level correctness. We find that SWE-Bench rankings do not predict task performance: Kimi-K2.5 at aggressive 3-bit quantization (UD-Q3_K_XL, 480 GB) produces the most complete and specification-compliant output, outranking models with substantially higher SWE-Bench Pro scores. We document three novel deployment findings: (1) default temperature=0 in coding tools causes sampling hangs with reasoning-model architectures, (2) reasoning-model thinking traces can leak through integration tools' file-path parsers, and (3) web-platform adaptation of native-mobile APIs is a universal training-data gap across every model tested. We also map the hardware-tier structure of April 2026 open-weights coding models, identifying two architectural schools and showing that the efficiency school (10-15 B active parameters) delivers equivalent SWE-Bench results at roughly 1/7th the hardware cost of the scale school (32-40 B active parameters).

cs.SE↗

arXiv2026

A Survey of Algorithm Debt in Machine and Deep Learning Systems: Definition, Smells, and Future Work

The adoption of Machine and Deep Learning (ML/DL) technologies introduces maintenance challenges, leading to Technical Debt (TD). Algorithm Debt (AD) is a TD type that impacts the performance and scalability of ML/DL systems. A review of 42 primary studies expanded AD's definition, uncovered its implicit presence, identified its smells, and highlighted future directions. These findings will guide an AD-focused study, enhancing the reliability of ML/DL systems.

cs.SE↗

arXiv2026

A Security Analysis of CheriBSD and Morello Linux

Memory corruption attacks have been prevalent in software for a long time. Some mitigation strategies against these attacks do exist, but they are not as far-reaching or as efficient as the CHERI architecture. CHERI uses capabilities to restrict pointers to certain regions of memory and with certain access restrictions. These capabilities are also used to implement "compartmentalisation": dividing a binary into smaller components with limited privilege, while adhering to the principle of least privilege. However, while this architecture successfully mitigates memory corruption attacks, the compartmentalisation mechanisms in place are less effective in containing malicious code to a separate compartment. This paper details four ways to bypass compartmentalisation, with a focus on Linux and BSD operating systems ported to this architecture. We find that although compartmentalisation is implemented in these two operating systems, simple bugs and attacks can still allow malicious code to bypass it. We conclude with mitigation measures to prevent these attacks, a proof-of-concept demonstrating their use, and recommendations for further securing Linux and BSD against unknown attacks.

cs.CR↗

arXiv2026

Refactoring and Equivalence in Rust: Expanding the REM Toolchain with a Novel Approach to Automated Equivalence Proofs

Refactoring tools are central to modern development, with extract-function refactorings used heavily in day-to-day work. For Rust, however, ownership, borrowing, and advanced type features make automated extract-function refactoring challenging. Existing tools either rely on slow compiler-based analysis, support only restricted language fragments, or provide little assurance beyond "it still compiles." This paper presents REM2.0, a new extract-function and verification toolchain for Rust. REM2.0 works atop rust-analyzer as a persistent daemon, providing low-latency refactorings with a VSCode front-end. It adds a repairer that automatically adjusts lifetimes and signatures when extraction exposes borrow-checker issues, and an optional verification pipeline connecting to CHARON and AENEAS to generate Coq equivalence proofs for a supported Rust subset. The architecture is evaluated on three benchmark suites. On the original REM artefact, REM2.0 achieves 100% compatibility while reducing latency from ~1000ms to single-digit milliseconds in the daemon. On 40 feature-focused extractions from 20 highly starred GitHub repositories, REM2.0 handles most examples involving async/await, const fn, non-local control flow, generics, and higher-ranked trait bounds. On twenty verification benchmarks, the CHARON/AENEAS pipeline constructs end-to-end equivalence proofs for cases within its current subset. Overall, results show that a rust-analyzer-based design can provide fast, feature-rich extract-function refactoring for real Rust programs, while opt-in verification delivers machine-checked behaviour preservation.

cs.PL↗

arXiv2025

Semantically Separating Nominal Wyvern for Usability and Decidability

The Dependent Object Types (DOT) calculus incorporates concepts from functional languages (e.g. modules) with traditional object-oriented features (e.g. objects, subtyping) to achieve greater expressivity (e.g. F-bounded polymorphism). However, this merger of paradigms comes at the cost of subtype decidability. Recent work on bringing decidability to DOT has either sacrificed expressiveness or ease of use. The unrestricted construction of recursive types and type bounds has made subtype decidability a much harder problem than in traditional object-oriented programming. Recognizing this, our paper introduces Nominal Wyvern, a DOT-like dependent type system that takes an alternative approach: instead of having a uniform structural syntax like DOT, Nominal Wyvern is designed around a "semantic separation" between the nominal declaration of recursive types on the one hand, and the structural refinement of those types when they are used on the other. This design naturally guides the user to avoid writing undecidably recursive structural types. From a technical standpoint, this separation also makes guaranteeing decidability possible by allowing for an intuitive adaptation of material/shape separation, a technique for achieving subtype decidability by separating types responsible for subtyping constraints from types that represent concrete data. The result is a type system with syntax and structure familiar to OOP users that achieves decidability without compromising the expressiveness of F-bounded polymorphism and module systems as they are used in practice.

cs.PL↗

arXiv2025

A Coq implementation of a Theory of Tagged Objects

We present a first step towards the Coq implementation of the Theory of Tagged Objects formalism. The concept of tagged types is encoded, and the soundness proofs are discussed with some future work suggestions.

cs.PL↗

arXiv2025

Validating Quantum State Preparation Programs (Extended Version)

One of the key steps in quantum algorithms is to prepare an initial quantum superposition state with different kinds of features. These so-called state preparation algorithms are essential to the behavior of quantum algorithms, and complicated state preparation algorithms are difficult to develop correctly and effectively. This paper presents Pqasm: a high-assurance framework implemented with the Coq proof assistant, allowing us to certify our Pqasm tool to correctly reflect quantum program behaviors. The key in the framework is to reduce the program correctness assurance of a program containing a quantum superposition state to the program correctness assurance for the program state without superposition. The reduction allows the development of an effective testing framework for testing quantum state preparation algorithm implementations on a classical computer - considered to be a hard problem with no clear solution until this point. We utilize the QuickChick property-based testing framework to test state preparation programs. We evaluated the effectiveness of our approach over 5 case studies implemented using Pqasm; such cases are not even simulatable in the current quantum simulators.

quant-ph↗

arXiv2024

Automated Detection of Algorithm Debt in Deep Learning Frameworks: An Empirical Study

Context: Previous studies demonstrate that Machine or Deep Learning (ML/DL) models can detect Technical Debt from source code comments called Self-Admitted Technical Debt (SATD). Despite the importance of ML/DL in software development, limited studies focus on automated detection for new SATD types: Algorithm Debt (AD). AD detection is important because it helps to identify TD early, facilitating research, learning, and preventing the accumulation of issues related to model degradation and lack of scalability. Aim: Our goal is to improve AD detection performance of various ML/DL models. Method: We will perform empirical studies using approaches: TF-IDF, Count Vectorizer, Hash Vectorizer, and TD-indicative words to identify features that improve AD detection, using ML/DL classifiers with different data featurisations. We will use an existing dataset curated from seven DL frameworks where comments were manually classified as AD, Compatibility, Defect, Design, Documentation, Requirement, and Test Debt. We will explore various word embedding methods to further enrich features for ML models. These embeddings will be from models founded in DL such as ROBERTA, ALBERTv2, and large language models (LLMs): INSTRUCTOR and VOYAGE AI. We will enrich the dataset by incorporating AD-related terms, then train various ML/DL classifiers, Support Vector Machine, Logistic Regression, Random Forest, ROBERTA, and ALBERTv2.

cs.SE↗

arXiv2024

Higher-Order Specifications for Deductive Synthesis of Programs with Pointers (Extended Version)

Synthetic Separation Logic (SSL) is a formalism that powers SuSLik, the state-of-the-art approach for the deductive synthesis of provably-correct programs in C-like languages that manipulate Heap-based linked data structures. Despite its expressivity, SSL suffers from two shortcomings that hinder its utility. First, its main specification component, inductive predicates, only admits first-order definitions of data structure shapes, which leads to the proliferation of ''boiler-plate'' predicates for specifying common patterns. Second, SSL requires concrete definitions of data structures to synthesise programs that manipulate them, which results in the need to change a specification for a synthesis task every time changes are introduced into the layout of the involved structures. We propose to significantly lift the level of abstraction used in writing Separation Logic specifications for synthesis -- both simplifying the approach and making the specifications more usable and easy to read and follow. We avoid the need to repetitively re-state low-level representation details throughout the specifications -- allowing the reuse of different implementations of the same data structure by abstracting away the details of a specific layout used in memory. Our novel high-level front-end language called Pika significantly improves the expressiveness of SuSLik. We implemented a layout-agnostic synthesiser from Pika to SuSLik enabling push-button synthesis of C programs with in-place memory updates, along with the accompanying full proofs that they meet Separation Logic-style specifications, from high-level specifications that resemble ordinary functional programs. Our experiments show that our tool can produce C code that is comparable in its performance characteristics and is sometimes faster than Haskell.

cs.PL↗

arXiv2024

Towards improved software visualisation of parameterised REE patterns: Introducing REEkit for geological analysis

Modern geological studies and mineral exploration techniques rely heavily on being able to digitally visualise and interpret data. Rare earth elements (REEs) are vital for renewable energy technologies. REE concentrations, when normalised to a standard material, show unique geometric curves (or patterns) in geological samples due to their similar chemical properties. The lambda technique can be used to describe these patterns and turn them into points - making it easier to visualise and interpret larger datasets. Lambdas have the potential to help industry understand intricate sample relationships and the geological and economic importance of their data. This study explored the use of lambdas through the evaluation of various visualisation methods to determine their usefulness in mineral exploration. The 'REEkit' platform facilitated the evaluation of the different visualisation methods and gauged industry interest and acceptance of such a service. Qualitative data was gathered through contextual inquiry, utilising semi-structured interviews and an observational session with 10 participants. Conceptual thematic analysis was applied to extract key findings. This study found that two critical factors for successful lambda data visualisation in the mineral exploration industry are familiarity and clarity: visualisations that were familiar and commonplace for users allowed for better analysis and clear communication to non-technical audiences. This included visualisations such as the 3D scatter plot and scatter plot matrix. Furthermore, visualisations that complemented each other and seamlessly integrated into the same workflow provided diverse perspectives on the data. Important aspects included understanding population grouping versus data distribution, achieved through combinations such as scatter plot and density contour plot, or 3D scatter plot and violin plot.

cs.HC↗

arXiv2024

Evaluating the Language-Based Security for Plugin Development

With the increasing popularity of plugin-based software systems, ensuring the security of plugins has become a critical concern. When users install plugins or browse websites with plugins from an untrusted source, how can we be sure that they do have any undesirable functions implicitly? In this research, we present a comprehensive study on language-based security mechanisms for plugin development. We aim to enhance the understanding of access control vulnerabilities in plugins and explore effective security measures by introducing a capability-based system. We also developed and evaluated test plugins to assess the security mechanisms in popular development environments such as IntelliJ IDEA and Visual Studio Code by utilising Java, JavaScript, and associated APIs and frameworks. We also explore the concept of capability-based module systems as an alternative approach to plugin security. A comparative analysis is conducted to evaluate the effectiveness of capability-based systems in addressing access control vulnerabilities identified in earlier sections. Finally, recommendations for improving plugin security practices and tools will be presented, emphasizing the importance of robust security measures in the ever-evolving landscape of software plugins.

cs.SE↗

arXiv2022

Flexible Correct-by-Construction Programming

Correctness-by-Construction (CbC) is an incremental program construction process to construct functionally correct programs. The programs are constructed stepwise along with a specification that is inherently guaranteed to be satisfied. CbC is complex to use without specialized tool support, since it needs a set of predefined refinement rules of fixed granularity which are additional rules on top of the programming language. Each refinement rule introduces a specific programming statement and developers cannot depart from these rules to construct programs. CbC allows to develop software in a structured and incremental way to ensure correctness, but the limited flexibility is a disadvantage of CbC. In this work, we compare classic CbC with CbC-Block and TraitCbC. Both approaches CbC-Block and TraitCbC, are related to CbC, but they have new language constructs that enable a more flexible software construction approach. We provide for both approaches a programming guideline, which similar to CbC, leads to well-structured programs. CbC-Block extends CbC by adding a refinement rule to insert any block of statements. Therefore, we introduce CbC-Block as an extension of CbC. TraitCbC implements correctness-by-construction on the basis of traits with specified methods. We formally introduce TraitCbC and prove soundness of the construction strategy. All three development approaches are qualitatively compared regarding their programming constructs, tool support, and usability to assess which is best suited for certain tasks and developers.

cs.LO↗

arXiv2022

Information Flow Control-by-Construction for an Object-Oriented Language Using Type Modifiers

In security-critical software applications, confidential information must be prevented from leaking to unauthorized sinks. Static analysis techniques are widespread to enforce a secure information flow by checking a program after construction. A drawback of these systems is that incomplete programs during construction cannot be checked properly. The user is not guided to a secure program by most systems. We introduce IFbCOO, an approach that guides users incrementally to a secure implementation by using refinement rules. In each refinement step, confidentiality or integrity (or both) is guaranteed alongside the functional correctness of the program, such that insecure programs are declined by construction. In this work, we formalize IFbCOO and prove soundness of the refinement rules. We implement IFbCOO in the tool CorC and conduct a feasibility study by successfully implementing case studies.

cs.CR↗

arXiv2022

Traits for Correct-by-Construction Programming

We demonstrate that traits are a natural way to support correctness-by-construction (CbC) in an existing programming language in the presence of traditional post-hoc verification (PhV). With Correctness-by-Construction, programs are constructed incrementally along with a specification that is inherently guaranteed to be satisfied. CbC is complex to use without specialized tool support, since it needs a set of refinement rules of fixed granularity which are additional rules on top of the programming language. In this work, we propose TraitCbC, an incremental program construction procedure that implements correctness-by-construction on the basis of PhV by using traits. TraitCbC enables program construction by trait composition instead of refinement rules. It provides a programming guideline, which similar to CbC should lead to well-structured programs, and allows flexible reuse of verified program building blocks. We introduce TraitCbC formally and prove the soundness of our verification strategy. Additionally, we implement TraitCbC as a proof of concept.

cs.PL↗

arXiv2019

Iteratively Composing Statically Verified Traits

Static verification relying on an automated theorem prover can be very slow and brittle: since static verification is undecidable, correct code may not pass a particular static verifier. In this work we use metaprogramming to generate code that is correct by construction. A theorem prover is used only to verify initial "traits": units of code that can be used to compose bigger programs. In our work, meta-programming is done by trait composition, which starting from correct code, is guaranteed to produce correct code. We do this by extending conventional traits with pre- and post-conditions for the methods; we also extend the traditional trait composition (+) operator to check the compatibility of contracts. In this way, there is no need to re-verify the produced code. We show how our approach can be applied to the standard "power" function example, where metaprogramming generates optimised, and correct, versions when the exponent is known in advance.

cs.PL↗

arXiv2019

Sound Invariant Checking Using Type Modifiers and Object Capabilities

In this paper we use pre existing language support for type modifiers and object capabilities to enable a system for sound runtime verification of invariants. Our system guarantees that class invariants hold for all objects involved in execution. Invariants are specified simply as methods whose execution is statically guaranteed to be deterministic and not access any externally mutable state. We automatically call such invariant methods only when objects are created or the state they refer to may have been mutated. Our design restricts the range of expressible invariants but improves upon the usability and performance of our system compared to prior work. In addition, we soundly support mutation, dynamic dispatch, exceptions, and non determinism, while requiring only a modest amount of annotation. We present a case study showing that our system requires a lower annotation burden compared to Spec#, and performs orders of magnitude less runtime invariant checks compared to the widely used `visible state semantics' protocols of D, Eiffel. We also formalise our approach and prove that such pre existing type modifier and object capability support is sufficient to ensure its soundness.

cs.PL↗