WIP: An Engaging Undergraduate Intro to Model Checking in Software Engineering Using TLA+

• URL: http://arxiv.org/abs/2407.21152v2
• Date: Sun, 18 Aug 2024 22:29:13 GMT
• Title: WIP: An Engaging Undergraduate Intro to Model Checking in Software Engineering Using TLA+
• Authors: Konstantin Läufer, Gunda Mertin, George K. Thiruvathukal,
• Abstract summary: We aim to qualitatively assess the state of formal methods in computer science programs. We construct level-appropriate examples that could be included midway into one's undergraduate studies.
• Score: 0.358439716487063
• License: http://creativecommons.org/licenses/by-sa/4.0/
• Abstract: Background: In this paper, we present our initial efforts to integrate formal methods, with a focus on model-checking specifications written in Temporal Logic of Actions (TLA+), into computer science education, targeting undergraduate juniors/seniors and graduate students. Formal methods can play a key role in ensuring correct behavior of safety-critical systems, yet remain underutilized in educational and industry contexts. Aims: We aim to (1) qualitatively assess the state of formal methods in computer science programs, (2) construct level-appropriate examples that could be included midway into one's undergraduate studies, (3) demonstrate how to address successive "failures" through progressively stringent safety and liveness requirements, and (4) establish an ongoing framework for assessing interest and relevance among students. Methods: After starting with a refresher on mathematical logic, students specify the rules of simple puzzles in TLA+ and use its included model checker (known as TLC) to find a solution. We gradually escalate to more complex, dynamic, event-driven systems, such as the control logic of a microwave oven, where students will study safety and liveness requirements. We subsequently discuss explicit concurrency, along with thread safety and deadlock avoidance, by modeling bounded counters and buffers. Results: Our initial findings suggest that through careful curricular design and choice of examples and tools, it is possible to inspire and cultivate a new generation of software engineers proficient in formal methods. Conclusions: Our initial efforts suggest that 84% of our students had a positive experience in our formal methods course. Future plans include a longitudinal analysis within our own institution and proposals to partner with other institutions to explore the effectiveness of our open-source and open-access modules.

Related papers

• Learning Task Representations from In-Context Learning [73.72066284711462]
  Large language models (LLMs) have demonstrated remarkable proficiency in in-context learning. We introduce an automated formulation for encoding task information in ICL prompts as a function of attention heads. We show that our method's effectiveness stems from aligning the distribution of the last hidden state with that of an optimally performing in-context-learned model.
  arXiv  Detail & Related papers  (2025-02-08T00:16:44Z)
• SMLE: Safe Machine Learning via Embedded Overapproximation [4.129133569151574]
  We consider the task of training differentiable ML models guaranteed to satisfy designer-chosen properties. This is very challenging, due to the computational complexity of rigorously verifying and enforcing compliance in modern neural models. We provide an innovative approach based on three components: 1) a general, simple architecture enabling efficient verification with a conservative semantic. We evaluate our approach on properties defined by linear inequalities in regression, and on mutually exclusive classes in multilabel classification.
  arXiv  Detail & Related papers  (2024-09-30T17:19:57Z)
• Scalable Language Model with Generalized Continual Learning [58.700439919096155]
  The Joint Adaptive Re-ization (JARe) is integrated with Dynamic Task-related Knowledge Retrieval (DTKR) to enable adaptive adjustment of language models based on specific downstream tasks. Our method demonstrates state-of-the-art performance on diverse backbones and benchmarks, achieving effective continual learning in both full-set and few-shot scenarios with minimal forgetting.
  arXiv  Detail & Related papers  (2024-04-11T04:22:15Z)
• Testing learning-enabled cyber-physical systems with Large-Language Models: A Formal Approach [32.15663640443728]
  The integration of machine learning (ML) into cyber-physical systems (CPS) offers significant benefits. Existing verification and validation techniques are often inadequate for these new paradigms. We propose a roadmap to transition from foundational probabilistic testing to a more rigorous approach capable of delivering formal assurance.
  arXiv  Detail & Related papers  (2023-11-13T14:56:14Z)
• Large Language Models for In-Context Student Modeling: Synthesizing Student's Behavior in Visual Programming [29.65988680948297]
  We explore the application of large language models (LLMs) for in-context student modeling in open-ended learning domains. We introduce a novel framework, LLM for Student Synthesis (LLM-SS), that leverages LLMs for a student's behavior. We instantiate several methods based on LLM-SS framework and evaluate them using an existing benchmark, StudentSyn, for student attempt synthesis in a visual programming domain.
  arXiv  Detail & Related papers  (2023-10-15T12:56:13Z)
• CoopInit: Initializing Generative Adversarial Networks via Cooperative Learning [50.90384817689249]
  CoopInit is a cooperative learning-based strategy that can quickly learn a good starting point for GANs. We demonstrate the effectiveness of the proposed approach on image generation and one-sided unpaired image-to-image translation tasks.
  arXiv  Detail & Related papers  (2023-03-21T07:49:32Z)
• Learning to Generate All Feasible Actions [4.333208181196761]
  We introduce action mapping, a novel approach that divides the learning process into two steps: first learn feasibility and subsequently, the objective. This paper focuses on the feasibility part by learning to generate all feasible actions through self-supervised querying of the feasibility model. We demonstrate the agent's proficiency in generating actions across disconnected feasible action sets.
  arXiv  Detail & Related papers  (2023-01-26T23:15:51Z)
• Evaluating Model-free Reinforcement Learning toward Safety-critical Tasks [70.76757529955577]
  This paper revisits prior work in this scope from the perspective of state-wise safe RL. We propose Unrolling Safety Layer (USL), a joint method that combines safety optimization and safety projection. To facilitate further research in this area, we reproduce related algorithms in a unified pipeline and incorporate them into SafeRL-Kit.
  arXiv  Detail & Related papers  (2022-12-12T06:30:17Z)
• Learning Multi-Objective Curricula for Deep Reinforcement Learning [55.27879754113767]
  Various automatic curriculum learning (ACL) methods have been proposed to improve the sample efficiency and final performance of deep reinforcement learning (DRL) In this paper, we propose a unified automatic curriculum learning framework to create multi-objective but coherent curricula. In addition to existing hand-designed curricula paradigms, we further design a flexible memory mechanism to learn an abstract curriculum.
  arXiv  Detail & Related papers  (2021-10-06T19:30:25Z)
• BUSTLE: Bottom-Up Program Synthesis Through Learning-Guided Exploration [72.88493072196094]
  We present a new synthesis approach that leverages learning to guide a bottom-up search over programs. In particular, we train a model to prioritize compositions of intermediate values during search conditioned on a set of input-output examples. We show that the combination of learning and bottom-up search is remarkably effective, even with simple supervised learning approaches.
  arXiv  Detail & Related papers  (2020-07-28T17:46:18Z)

This list is automatically generated from the titles and abstracts of the papers in this site.

This site does not guarantee the quality of this site (including all information) and is not responsible for any consequences.