Titlebook: Verified Software: Theories, Tools, Experiments; Third International Gary T. Leavens,Peter O’Hearn,Sriram K. Rajamani Conference proceedin

制定法律

To Goto Where No Statement Has Gone Before low-level code represented as blocks of code connected by . statements, ., a control flow graph (CFG). The derived expression is in a form that can be used as input to an automatic theorem prover. The method is useful for program verification systems that take as input both programs and specificati

诱拐

The Next 700 Separation Logicsr concurrency primitive to require a new separation logic. I will argue that we shouldn’t be inventing new separation logics, but should find the right logic to reason about interference, and have a powerful abstraction mechanism to enable the library’s implementation details to be correctly abstrac

Immunoglobulin

JADED

Abstraction and Refinement for Local Reasoningtion. In separation logic, we use a low-level abstraction that is close to how the machine sees the program state. In context logic, we work with high-level abstractions that are close to how the clients of modules see the program state.We apply program refinement to local reasoning, demonstrating t

HUMID

Pervasive Verification of an OS Microkernelnto a single top-level theorem of microkernel correctness. This theorem states the simulation of user processes with own, separate virtual memories — via the microkernel — by the underlying hardware with devices. All models, theorems, and proofs are formalized in the interactive proof system Isabelle/HOL.

公式

Dafny Meets the Verification Benchmarks ChallengeA Dafny program includes specifications, code, inductive invariants, and termination metrics. Each of the eight programs is fed to the Dafny verifier, which without further user interaction automatically performs the verification in a few seconds.

Adherent

Specifying Reusable Componentsthe classic Design by Contract approach with a notion of model, which underpins the precise definitions of such concepts as abstract object equivalence and specification completeness. Experiments applying model-based contracts to libraries of data structures suggest that the method enables accurate specification of practical software.

一致性

Reusable Verification of a Copying Collectoreuse; it is the first to map implementations into three different machine languages and, unlike some noteworthy published proofs, our verified implementations of memory allocation handle termination and the ‘out-of-memory’ case properly. The work presented here has been developed in the HOL4 theorem prover.

披肩

The Next 700 Separation Logicst logic to reason about interference, and have a powerful abstraction mechanism to enable the library’s implementation details to be correctly abstracted. Adding new concurrency libraries should simply be a matter of verification, not of new logics or metatheory.

好开玩笑