Show simple item record

dc.contributor.author
Li, Jialin
dc.contributor.author
Lattuada, Andrea
dc.contributor.author
Zhou, Yi
dc.contributor.author
Cameron, Jonathan
dc.contributor.author
Howell, Jon
dc.contributor.author
Parno, Bryan
dc.contributor.author
Hawblitzel, Chris
dc.date.accessioned
2022-07-27T07:23:32Z
dc.date.available
2022-05-15T02:45:23Z
dc.date.available
2022-07-27T07:23:32Z
dc.date.issued
2022
dc.identifier.issn
2475-1421
dc.identifier.other
10.1145/3527313
en_US
dc.identifier.uri
http://hdl.handle.net/20.500.11850/547209
dc.identifier.doi
10.3929/ethz-b-000547209
dc.description.abstract
Reasoning about memory aliasing and mutation in software verification is a hard problem. This is especially true for systems using SMT-based automated theorem provers. Memory reasoning in SMT verification typically requires a nontrivial amount of manual effort to specify heap invariants, as well as extensive alias reasoning from the SMT solver. In this paper, we present a hybrid approach that combines linear types with SMT-based verification for memory reasoning. We integrate linear types into Dafny, a verification language with an SMT backend, and show that the two approaches complement each other. By separating memory reasoning from verification conditions, linear types reduce the SMT solving time. At the same time, the expressiveness of SMT queries extends the flexibility of the linear type system. In particular, it allows our linear type system to easily and correctly mix linear and nonlinear data in novel ways, encapsulating linear data inside nonlinear data and vice-versa. We formalize the core of our extensions, prove soundness, and provide algorithms for linear type checking. We evaluate our approach by converting the implementation of a verified storage system (similar to 24K lines of code and proof) written in Dafny, to use our extended Dafny. The resulting system uses linear types for 91% of the code and SMT-based heap reasoning for the remaining 9%. We show that the converted system has 28% fewer lines of proofs and 30% shorter verification time overall. We discuss the development overhead in the original system due to SMT-based heap reasoning and highlight the improved developer experience when using linear types.
en_US
dc.format
application/pdf
en_US
dc.language.iso
en
en_US
dc.publisher
ACM
en_US
dc.rights.uri
http://creativecommons.org/licenses/by/4.0/
dc.subject
linear types
en_US
dc.subject
systems verification
en_US
dc.title
Linear Types for Large-Scale Systems Verification
en_US
dc.type
Journal Article
dc.rights.license
Creative Commons Attribution 4.0 International
ethz.journal.title
Proceedings of the ACM on Programming Languages
ethz.journal.volume
6
en_US
ethz.journal.issue
OOPSLA1
en_US
ethz.journal.abbreviated
Proc. ACM Program. Lang.
ethz.pages.start
69
en_US
ethz.size
28 p.
en_US
ethz.version.deposit
publishedVersion
en_US
ethz.identifier.wos
ethz.identifier.scopus
ethz.publication.place
New York, NY
en_US
ethz.publication.status
published
en_US
ethz.date.deposited
2022-05-15T02:46:00Z
ethz.source
WOS
ethz.eth
yes
en_US
ethz.availability
Open access
en_US
ethz.rosetta.installDate
2022-07-27T07:23:40Z
ethz.rosetta.lastUpdated
2022-07-27T07:23:40Z
ethz.rosetta.exportRequired
true
ethz.rosetta.versionExported
true
ethz.COinS
ctx_ver=Z39.88-2004&rft_val_fmt=info:ofi/fmt:kev:mtx:journal&rft.atitle=Linear%20Types%20for%20Large-Scale%20Systems%20Verification&rft.jtitle=Proceedings%20of%20the%20ACM%20on%20Programming%20Languages&rft.date=2022&rft.volume=6&rft.issue=OOPSLA1&rft.spage=69&rft.issn=2475-1421&rft.au=Li,%20Jialin&Lattuada,%20Andrea&Zhou,%20Yi&Cameron,%20Jonathan&Howell,%20Jon&rft.genre=article&rft_id=info:doi/10.1145/3527313&
 Search print copy at ETH Library

Files in this item

Thumbnail

Publication type

Show simple item record