journal contribution
posted on 1996-09-01, 00:00 authored by John C Reynolds After some general remarks about program verification, we introduce separation logic, a novel extension of Hoare logic that can strengthen the applicability and scalability of program verification for imperative programs that use shared mutable data structures or shared memory concurrency.
History
Publisher Statement
Copyright © 1996 by the VLDB Endowment. Permission to copy without fee all or part of this material is granted provided that the copies are not made or distributed for direct commercial advantage, the VLDB copyright notice and the title of the publication and its date appear, and notice is given that copying is by the permission of the Very Large Data Base Endowment. To copy otherwise, or to republish, requires a fee and/or special permission from the Endowment.Date
1996-09-01