Contract Based Program Models for Software Model Checking

• URL: http://arxiv.org/abs/2503.11236v1
• Date: Fri, 14 Mar 2025 09:34:59 GMT
• Title: Contract Based Program Models for Software Model Checking
• Authors: Jesper Amilon, Dilian Gurov,
• Abstract summary: We propose a formalism previously developed for the purposes of compositional model checking.<n>We describe how we envisage the work flow and tool chain to support the proposed verification approach in the context of embedded, safety-critical software written inC.
• Score: 0.0
• License: http://creativecommons.org/licenses/by-sa/4.0/
• Abstract: Model checking temporal properties of software is algorithmically hard. To be practically feasible, it usually requires the creation of simpler, abstract models of the software, over which the properties are checked. However, creating suitable abstractions is another difficult problem. We argue that such abstract models can be obtained with little effort, when the state transformation properties of the software components have already been deductively verified. As a concrete, language-independent representation of such abstractions we propose the use of \emph{flow graphs}, a formalism previously developed for the purposes of compositional model checking. In this paper, we describe how we envisage the work flow and tool chain to support the proposed verification approach in the context of embedded, safety-critical software written in~C.

Related papers

• Self-Steering Language Models [113.96916935955842]
  DisCIPL is a method for "self-steering" language models. DisCIPL uses a Planner model to generate a task-specific inference program. Our work opens up a design space of highly-parallelized Monte Carlo inference strategies.
  arXiv  Detail & Related papers  (2025-04-09T17:54:22Z)
• Establishing tool support for a concept DSL [0.0]
  This thesis describes Conceptual, a DSL for modeling the behavior of software systems using self-contained and highly reusable units of concepts.<n>The suggested strategy is then implemented with a simple compiler, allowing developers to access and utilize Alloy's existing analysis tools for program reasoning.
  arXiv  Detail & Related papers  (2025-03-07T09:18:31Z)
• Accessible Smart Contracts Verification: Synthesizing Formal Models with Tamed LLMs [7.087237546722617]
  One of the most powerful ways of establishing software correctness is by using formal methods.<n>Our work addresses this critical disadvantage by automating the creation of a formal model.<n>In this way, we significantly reduce the amount of time necessary to create formal models.
  arXiv  Detail & Related papers  (2025-01-22T15:57:29Z)
• Formal Analysis of the Contract Automata Runtime Environment with Uppaal: Modelling, Verification and Testing [0.3807314298073301]
  A distributed runtime application called tt CARE has been introduced to realise service applications specified using a dialect of finite-state automata.<n>We detail the formal modelling, verification and testing of tt CARE.
  arXiv  Detail & Related papers  (2025-01-22T15:03:25Z)
• Runtime Verification on Abstract Finite State Models [0.0]
  We show how to extract finite state models from a run of a multi-threaded Java program and carry out runtime verification of correctness properties. The main contribution of this paper is in showing how runtime verification can be made efficient through online property checking on property-preserving abstract models.
  arXiv  Detail & Related papers  (2024-06-18T15:32:31Z)
• Fine-Tuning Enhances Existing Mechanisms: A Case Study on Entity Tracking [53.66999416757543]
  We study how fine-tuning affects the internal mechanisms implemented in language models. Fine-tuning enhances, rather than alters, the mechanistic operation of the model.
  arXiv  Detail & Related papers  (2024-02-22T18:59:24Z)
• Formal Verification Of A Shopping Basket Application Model Using PRISM [0.0]
  We present the results of a simulation using Prism Model Checker for a Shopping Basket Application Model. The objective is to simulate the behavior of shoppers as they go through a number of defined states of the shopping process.
  arXiv  Detail & Related papers  (2023-07-16T00:14:40Z)
• Model-Invariant State Abstractions for Model-Based Reinforcement Learning [54.616645151708994]
  We introduce a new type of state abstraction called textitmodel-invariance. This allows for generalization to novel combinations of unseen values of state variables. We prove that an optimal policy can be learned over this model-invariance state abstraction.
  arXiv  Detail & Related papers  (2021-02-19T10:37:54Z)
• DirectDebug: Automated Testing and Debugging of Feature Models [55.41644538483948]
  Variability models (e.g., feature models) are a common way for the representation of variabilities and commonalities of software artifacts. Complex and often large-scale feature models can become faulty, i.e., do not represent the expected variability properties of the underlying software artifact.
  arXiv  Detail & Related papers  (2021-02-11T11:22:20Z)
• Goal-directed Generation of Discrete Structures with Conditional Generative Models [85.51463588099556]
  We introduce a novel approach to directly optimize a reinforcement learning objective, maximizing an expected reward. We test our methodology on two tasks: generating molecules with user-defined properties and identifying short python expressions which evaluate to a given target value.
  arXiv  Detail & Related papers  (2020-10-05T20:03:13Z)
• Exploring Software Naturalness through Neural Language Models [56.1315223210742]
  The Software Naturalness hypothesis argues that programming languages can be understood through the same techniques used in natural language processing. We explore this hypothesis through the use of a pre-trained transformer-based language model to perform code analysis tasks.
  arXiv  Detail & Related papers  (2020-06-22T21:56:14Z)
• Interpretable Entity Representations through Large-Scale Typing [61.4277527871572]
  We present an approach to creating entity representations that are human readable and achieve high performance out of the box. Our representations are vectors whose values correspond to posterior probabilities over fine-grained entity types. We show that it is possible to reduce the size of our type set in a learning-based way for particular domains.
  arXiv  Detail & Related papers  (2020-04-30T23:58:03Z)

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.