Show simple item record

dc.contributor.author
Juhasz, Uri
dc.contributor.author
Kassios, Ioannis T.
dc.contributor.author
Müller, Peter
dc.contributor.author
Nováček, Miloš
dc.contributor.author
Schwerhoff, Malte
dc.contributor.author
Summers, Alexander J.
dc.date.accessioned
2017-09-27T14:07:01Z
dc.date.available
2017-06-11T09:26:44Z
dc.date.available
2017-09-27T14:07:01Z
dc.date.issued
2014
dc.identifier.uri
http://hdl.handle.net/20.500.11850/85086
dc.identifier.doi
10.3929/ethz-a-010151765
dc.description.abstract
The automation of verification techniques based on firstorder logic specifications has benefited greatly from verification infrastructures such as Boogie and Why. These offer an intermediate language that can express diverse language features and verification techniques, as well as back-end tools such as verification condition generators. However, these infrastructures are not well suited for verification techniques based on separation logic and other permission logics, because they do not provide direct support for permissions and because existing tools for these logics often prefer symbolic execution over verification condition generation. Consequently, tool support for these logics is typically developed independently for each technique, dramatically increasing the burden of developing automatic tools for permission-based verification. In this paper, we present a verification infrastructure whose intermediate language supports an expressive permission model natively. We provide tool support, including two back-end verifiers, one based on symbolic execution, and one on verification condition generation; this facilitates experimenting with the two prevailing techniques in automated verification. Various existing verification techniques can be implemented via this infrastructure, alleviating much of the burden of building permissionbased verifiers, and allowing the developers of higher-level techniques to focus their efforts at the appropriate level of abstraction.
en_US
dc.format
application/pdf
dc.language.iso
en
en_US
dc.publisher
ETH-Zürich
en_US
dc.rights.uri
http://rightsstatements.org/page/InC-NC/1.0/
dc.subject
VERIFICATION (SOFTWARE ENGINEERING)
en_US
dc.subject
VERIFIKATION (SOFTWARE ENGINEERING)
en_US
dc.title
Viper
en_US
dc.type
Report
dc.rights.license
In Copyright - Non-Commercial Use Permitted
dc.date.published
2014
ethz.title.subtitle
A Verification Infrastructure for Permission-Based Reasoning
en_US
ethz.size
21 p.
en_US
ethz.code.ddc
DDC - DDC::0 - Computer science, information & general works::004 - Data processing, computer science
en_US
ethz.identifier.nebis
010151765
ethz.publication.place
Zürich
en_US
ethz.publication.status
published
en_US
ethz.leitzahl
ETH Zürich::00002 - ETH Zürich::00012 - Lehre und Forschung::00007 - Departemente::02150 - Dep. Informatik / Dep. of Computer Science::02664 - Inst. f. Programmiersprachen u. -systeme / Inst. Programming Languages and Systems::03653 - Müller, Peter / Müller, Peter
en_US
ethz.leitzahl
ETH Zürich::00002 - ETH Zürich::00012 - Lehre und Forschung::00007 - Departemente::02150 - Dep. Informatik / Dep. of Computer Science
en_US
ethz.leitzahl.certified
ETH Zürich::00002 - ETH Zürich::00012 - Lehre und Forschung::00007 - Departemente::02150 - Dep. Informatik / Dep. of Computer Science::02664 - Inst. f. Programmiersprachen u. -systeme / Inst. Programming Languages and Systems::03653 - Müller, Peter / Müller, Peter
ethz.date.deposited
2017-06-11T09:28:05Z
ethz.source
ECOL
ethz.source
ECIT
ethz.identifier.importid
imp59366b5bf0a9557749
ethz.identifier.importid
imp593651f9ddb9429705
ethz.ecolpid
eth:8615
ethz.ecitpid
pub:134066
ethz.eth
yes
en_US
ethz.availability
Open access
en_US
ethz.rosetta.installDate
2017-07-25T17:14:59Z
ethz.rosetta.lastUpdated
2022-03-28T17:37:14Z
ethz.rosetta.versionExported
true
ethz.COinS
ctx_ver=Z39.88-2004&rft_val_fmt=info:ofi/fmt:kev:mtx:journal&rft.atitle=Viper&rft.date=2014&rft.au=Juhasz,%20Uri&Kassios,%20Ioannis%20T.&M%C3%BCller,%20Peter&Nov%C3%A1%C4%8Dek,%20Milo%C5%A1&Schwerhoff,%20Malte&rft.genre=report&rft.btitle=Viper
 Search print copy at ETH Library

Files in this item

Thumbnail

Publication type

Show simple item record