Execution Time Program Verification With Tight Bounds

• URL: http://arxiv.org/abs/2210.11105v1
• Date: Thu, 20 Oct 2022 09:02:13 GMT
• Title: Execution Time Program Verification With Tight Bounds
• Authors: Ana Carolina Silva, Manuel Barbosa and Mario Florido
• Abstract summary: This paper presents a proof system for reasoning about execution time bounds for a core imperative programming language. We define a Hoare logic for the three cases and prove its soundness with respect to an annotated cost-aware operational semantics. The practicality of the proof system is demonstrated with an implementation in OCaml of the different modules needed to apply it to example programs.
• Score: 6.36836017515443
• License: http://creativecommons.org/licenses/by/4.0/
• Abstract: This paper presents a proof system for reasoning about execution time bounds for a core imperative programming language. Proof systems are defined for three different scenarios: approximations of the worst-case execution time, exact time reasoning, and less pessimistic execution time estimation using amortized analysis. We define a Hoare logic for the three cases and prove its soundness with respect to an annotated cost-aware operational semantics. Finally, we define a verification conditions (VC) generator that generates the goals needed to prove program correctness, cost, and termination. Those goals are then sent to the Easycrypt toolset for validation. The practicality of the proof system is demonstrated with an implementation in OCaml of the different modules needed to apply it to example programs. Our case studies are motivated by real-time and cryptographic software.

Related papers

• Inductive Predicate Synthesis Modulo Programs (Extended) [1.7372615815088566]
  A growing trend in program analysis is to encode verification conditions within the language of the input program. We propose Inductive Predicate Synthesis Modulo Programs (IPS-MP) which extends high-level languages with minimal synthesis features.
  arXiv  Detail & Related papers  (2024-07-11T12:51:08Z)
• Evaluating LLM-driven User-Intent Formalization for Verification-Aware Languages [6.0608817611709735]
  We propose a metric for evaluating the quality of specifications for verification-aware languages. We show that our metric agrees closely on a human-labeled dataset of Dafny specifications for the popular MBPP code-generation benchmark. We also outline formal verification challenges that need to be addressed to apply the technique more widely.
  arXiv  Detail & Related papers  (2024-06-14T06:52:08Z)
• Bisimulation Learning [55.859538562698496]
  We compute finite bisimulations of state transition systems with large, possibly infinite state space. Our technique yields faster verification results than alternative state-of-the-art tools in practice.
  arXiv  Detail & Related papers  (2024-05-24T17:11:27Z)
• NExT: Teaching Large Language Models to Reason about Code Execution [50.93581376646064]
  Large language models (LLMs) of code are typically trained on the surface textual form of programs. We propose NExT, a method to teach LLMs to inspect the execution traces of programs and reason about their run-time behavior.
  arXiv  Detail & Related papers  (2024-04-23T01:46:32Z)
• Log Probabilities Are a Reliable Estimate of Semantic Plausibility in Base and Instruction-Tuned Language Models [50.15455336684986]
  We evaluate the effectiveness of LogProbs and basic prompting to measure semantic plausibility. We find that LogProbs offers a more reliable measure of semantic plausibility than direct zero-shot prompting. We conclude that, even in the era of prompt-based evaluations, LogProbs constitute a useful metric of semantic plausibility.
  arXiv  Detail & Related papers  (2024-03-21T22:08:44Z)
• Parallel Program Analysis on Path Ranges [3.018638214344819]
  Ranged symbolic execution performs symbolic execution on program parts, so called path ranges, in parallel. We present a verification approach that splits programs into path ranges and then runs arbitrary analyses on the ranges in parallel.
  arXiv  Detail & Related papers  (2024-02-19T08:26:52Z)
• Decidable Reasoning About Time in Finite-Domain Situation Calculus Theories [9.45355418401911]
  Most commonly used approach represents time by adding a real-valued fluent $mathittime(a)$ that attaches a time point to each action and consequently to each situation. We show that in this approach, checking whether there is a reachable situation that satisfies a given formula is undecidable, even if the domain of discourse is restricted to a finite set of objects.
  arXiv  Detail & Related papers  (2024-02-05T16:32:12Z)
• Unlocking Temporal Question Answering for Large Language Models with Tailor-Made Reasoning Logic [84.59255070520673]
  Large language models (LLMs) face a challenge when engaging in temporal reasoning. We propose TempLogic, a novel framework designed specifically for temporal question-answering tasks.
  arXiv  Detail & Related papers  (2023-05-24T10:57:53Z)
• Fact-Checking Complex Claims with Program-Guided Reasoning [99.7212240712869]
  Program-Guided Fact-Checking (ProgramFC) is a novel fact-checking model that decomposes complex claims into simpler sub-tasks. We first leverage the in-context learning ability of large language models to generate reasoning programs. We execute the program by delegating each sub-task to the corresponding sub-task handler.
  arXiv  Detail & Related papers  (2023-05-22T06:11:15Z)
• Time-varying Gaussian Process Bandit Optimization with Non-constant Evaluation Time [93.6788993843846]
  We propose a novel time-varying Bayesian optimization algorithm that can effectively handle the non-constant evaluation time. Our bound elucidates that a pattern of the evaluation time sequence can hugely affect the difficulty of the problem.
  arXiv  Detail & Related papers  (2020-03-10T13:28:33Z)

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.