This Is Boogie 2

Leino, K. R. M. (2008). This Is Boogie 2.

Type

Report

Intellectual base

Grey literature

Year

2008

Link

https://www.microsoft.com/en-us/research/publication/this-is-boogie-2-2/

Cited from

philosophy

Cited by

1 citation across 1 artifact.

Each citation links to the sentence it supports in the citing article.

Primes

• Epistemic Mode Of A Proposition
  • In programming and formal methods, the modes are explicit in the language: an assert checks a proposition that should hold and halts if it does not, an assume (in verification) is relied on without checking, an invariant is a proposition required to hold at every iteration, a precondition is a premise the caller must discharge, and a Postcondition is an asserted guarantee — and a verification tool's soundness depends on never confusing an assume (taken on trust) with an assert (checked).

    This sourceSpecifies the verification language's assert (an expression required to hold in every correct trace — checked) versus assume (an expression taken to hold in every feasible trace — relied on without checking), with preconditions/postconditions — supporting the assert/assume/precondition modes, that soundness depends on not confusing assume with assert, and the catastrophic mode error of writing assume where assert was required.

Verification

Does it exist? Not checked yet. This entry carries no identifier to resolve. It was extracted from the citation as written in the article, normalized, and deduplicated against the rest of the registry.

Does it back the claim? Not recorded. The single citation of this work carries no recorded support check.

Support is checked per citation rather than per work — the same source can be cited soundly in one article and wrongly in another. Per-citation recording began recently, so a citation with no recorded check is a gap in the record rather than evidence it went unchecked.

See how references were verified.

Registry ID ref:c18f055364ea · see in the full table