Separation Logic.
The article examines the use of separation logic in reasoning about computer programs. It looks at how separation logic supports scalable reasoning through the frame rule, an inference rule that allows a proof to be localized to the resources that a program component accesses. Concurrent separation...
| Published in: | Communications of the ACM Vol. 62; no. 2; pp. 86 - 96 |
|---|---|
| Main Author: | |
| Format: | Article |
| Published: |
Association for Computing Machinery
Feb2019
|
| Subjects: | |
| Online Access: | View this record in EBSCOhost |
| fields | @attributes: recordID: 1 pdfLink: plink: https://search.ebscohost.com/login.aspx?direct=true&db=hlh&AN=134383088&site=ehost-live header: @attributes: shortDbName: hlh uiTerm: 134383088 longDbName: Humanities International Complete uiTag: AN controlInfo: bkinfo: jinfo: jid: 00010782 ACM jtl: Communications of the ACM issn: 00010782 maglogo: N pubinfo: dt: Feb2019 vid: 62 iid: 2 pid: 68 pub: Association for Computing Machinery artinfo: ui: 134383088 10.1145/3211968 ppf: 86 ppct: 10 formats: tig: atl: Separation Logic. aug: au: O’HEARN, PETER affil: Research scientist at Facebook. Professor of computer science at University College London, U.K. su: Computer programming Logic Reasoning Frame relay (Data transmission) sug: subj: Computer programming Logic Reasoning Frame relay (Data transmission) ab: The article examines the use of separation logic in reasoning about computer programs. It looks at how separation logic supports scalable reasoning through the frame rule, an inference rule that allows a proof to be localized to the resources that a program component accesses. Concurrent separation logic is also covered. pubtype: Periodical doctype: Article src: R language: English refInfo: copyright: @attributes: flag: Y dt: @attributes: year: 2019 holdings: @attributes: islocal: N |
|---|