The bibliographic entry was discovered and compiled by a machine, and published without a person checking it against the publication. The publication itself is the authors' own work — this badge says nothing about it.

Characteristic formulae for the verification of imperative programs

The work

AuthorsArthur Charguéraud
Editors
Typemisc
Year2011
Citekeychargueraud2011characteristic

Where it appeared

Published inACM SIGPLAN International Conference on Functional Programming (ICFP)
Pages418--430

Identifiers

DOI10.1145/2034773.2034828
OpenAlexW4247464325

Access

Landing pagehttps://doi.org/10.1145/2034773.2034828

From OpenAlex, which stores abstracts as an index of words and their positions: what is shown is rebuilt from that, and reads fluently whether or not it is what the author wrote.

Abstract

In previous work, we introduced an approach to program verification based on characteristic formulae. The approach consists of generating a higher-order logic formula from the source code of a program. This characteristic formula is constructed in such a way that it gives a sound and complete description of the semantics of that program. The formula can thus be exploited in an interactive proof assistant to formally verify that the program satisfies a particular specification.

How it got here

How it got hereagent via openalex
Added2026-10-25 13:23 UTC
Not denied bya person 2026-10-29 17:12 UTC

Cite it as

@misc{chargueraud2011characteristic,
  title        = {Characteristic formulae for the verification of imperative programs},
  author       = {Arthur Charguéraud},
  year         = {2011},
  journal      = {ACM SIGPLAN International Conference on Functional Programming (ICFP)},
  pages        = {418--430},
  doi          = {10.1145/2034773.2034828},
}

This record lives at https://refs.drheap.org/chargueraud2011characteristic/ and will keep doing so.