Handling expression evaluation under interference

• URL: http://arxiv.org/abs/2409.07741v1
• Date: Thu, 12 Sep 2024 04:16:22 GMT
• Title: Handling expression evaluation under interference
• Authors: Ian J. Hayes, Cliff B. Jones, Larissa A. Meinicke,
• Abstract summary: Hoare-style inference rules for program constructs permit the copying of expressions and tests from program text into logical contexts. The "rely-guarantee" approach does tackle the issue of recording acceptable interference and offers a way to provide safe inference rules.
• Score: 0.0
• License: http://creativecommons.org/licenses/by/4.0/
• Abstract: Hoare-style inference rules for program constructs permit the copying of expressions and tests from program text into logical contexts. It is known that this requires care even for sequential programs but further issues arise for concurrent programs because of potential interference to the values of variables. The "rely-guarantee" approach does tackle the issue of recording acceptable interference and offers a way to provide safe inference rules. This paper shows how the algebraic presentation of rely-guarantee ideas can clarify and formalise the conditions for safely re-using expressions and tests from program text in logical contexts for reasoning about programs.

Related papers

• Splitting Answer Set Programs with respect to Intensionality Statements (Extended Version) [10.15627964021711]
  Splitting a logic program allows us to reduce the task of computing its stable models to similar tasks for its subprograms. We generalize the conditions under which this technique is applicable, by considering not only dependencies between predicates but also their arguments and context.
  arXiv  Detail & Related papers  (2025-03-25T15:27:05Z)
• Few-shot Policy (de)composition in Conversational Question Answering [54.259440408606515]
  We propose a neuro-symbolic framework to detect policy compliance using large language models (LLMs) in a few-shot setting. We show that our approach soundly reasons about policy compliance conversations by extracting sub-questions to be answered, assigning truth values from contextual information, and explicitly producing a set of logic statements from the given policies. We apply this approach to the popular PCD and conversational machine reading benchmark, ShARC, and show competitive performance with no task-specific finetuning.
  arXiv  Detail & Related papers  (2025-01-20T08:40:15Z)
• Weakly Supervised Semantic Parsing with Execution-based Spurious Program Filtering [19.96076749160955]
  We propose a domain-agnostic filtering mechanism based on program execution results. We run a majority vote on these representations to identify and filter out programs with significantly different semantics from the other programs.
  arXiv  Detail & Related papers  (2023-11-02T11:45:40Z)
• A Unifying Framework for Learning Argumentation Semantics [50.69905074548764]
  We present a novel framework, which uses an Inductive Logic Programming approach to learn the acceptability semantics for several abstract and structured argumentation frameworks in an interpretable way. Our framework outperforms existing argumentation solvers, thus opening up new future research directions in the area of formal argumentation and human-machine dialogues.
  arXiv  Detail & Related papers  (2023-10-18T20:18:05Z)
• Assume but Verify: Deductive Verification of Leaked Information in Concurrent Applications (Extended Version) [1.3749490831384268]
  We consider the problem of specifying and proving the security of non-trivial, concurrent programs that intentionally leak information. We present a method that decomposes the problem into (a) proving that the program only leaks information via assume annotations already widely used in deductive program verification. We also show how condition (a) can be enforced by an extension of the existing program logic SecCSL, and how (b) can be checked by proving a set of simple entailments.
  arXiv  Detail & Related papers  (2023-09-07T01:51:41Z)
• Argumentative Characterizations of (Extended) Disjunctive Logic Programs [2.055949720959582]
  We show that assumption-based argumentation can represent not only normal logic programs, but also disjunctive logic programs and their extensions. We consider some inference rules for disjunction that the core logic of the argumentation frameworks should respect.
  arXiv  Detail & Related papers  (2023-06-12T14:01:38Z)
• Rationale-Augmented Ensembles in Language Models [53.45015291520658]
  We reconsider rationale-augmented prompting for few-shot in-context learning. We identify rationale sampling in the output space as the key component to robustly improve performance. We demonstrate that rationale-augmented ensembles achieve more accurate and interpretable results than existing prompting approaches.
  arXiv  Detail & Related papers  (2022-07-02T06:20:57Z)
• Probing as Quantifying the Inductive Bias of Pre-trained Representations [99.93552997506438]
  We present a novel framework for probing where the goal is to evaluate the inductive bias of representations for a particular task. We apply our framework to a series of token-, arc-, and sentence-level tasks.
  arXiv  Detail & Related papers  (2021-10-15T22:01:16Z)
• Enforcing Consistency in Weakly Supervised Semantic Parsing [68.2211621631765]
  We explore the use of consistency between the output programs for related inputs to reduce the impact of spurious programs. We find that a more consistent formalism leads to improved model performance even without consistency-based training.
  arXiv  Detail & Related papers  (2021-07-13T03:48:04Z)
• Representing Partial Programs with Blended Abstract Semantics [62.20775388513027]
  We introduce a technique for representing partially written programs in a program synthesis engine. We learn an approximate execution model implemented as a modular neural network. We show that these hybrid neuro-symbolic representations enable execution-guided synthesizers to use more powerful language constructs.
  arXiv  Detail & Related papers  (2020-12-23T20:40:18Z)
• Sequential composition of propositional logic programs [0.0]
  We show that acyclic programs can be decomposed into single-rule programs and provide a general decomposition result for arbitrary programs. We show that the immediate consequence operator of a program can be represented via composition which allows us to compute its least model without any explicit reference to operators.
  arXiv  Detail & Related papers  (2020-09-12T11:57:30Z)
• Verifying Tight Logic Programs with anthem and Vampire [7.804960968120875]
  We extend the definition of program completion to programs with input and output in a subset of the input language of the ASP grounder gringo. We study the relationship between stable models and completion in this context, and describe preliminary experiments with the use of two software tools.
  arXiv  Detail & Related papers  (2020-08-05T10:01:33Z)
• Can We Learn Heuristics For Graphical Model Inference Using Reinforcement Learning? [114.24881214319048]
  We show that we can learn programs, i.e., policies, for solving inference in higher order Conditional Random Fields (CRFs) using reinforcement learning. Our method solves inference tasks efficiently without imposing any constraints on the form of the potentials.
  arXiv  Detail & Related papers  (2020-04-27T19:24:04Z)

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.