Conference item icon

Conference item

Efficient verification of multi-property designs (The benefit of wrong assumptions)

Abstract:

We consider the problem of efficiently checking a set of safety properties Ρ1,…,Ρk of one design. We introduce a new approach called Ja-verification, where Ja stands for “Just-Assume” (as opposed to “assume-guarantee”). In this approach, when proving a property Pi, one assumes that every property Pj for j ≠ i holds. The process of proving properties either results in showing that Ρ1,.,.,Ρk hold without any assumptions or finding a “debugging set” of properties. The latter identifies a subset ...

Expand abstract
Publication status:
Published
Peer review status:
Peer reviewed
Version:
Accepted Manuscript

Actions


Access Document


Files:
Publisher copy:
10.23919/DATE.2018.8341977

Authors


Goldberg, E More by this author
Güdemann, M More by this author
More by this author
Institution:
University of Oxford
Division:
MPLS Division
Department:
Computer Science
More by this author
Institution:
University of Oxford
Division:
MPLS Division
Department:
Computer Science
More from this funder
Grant:
280053 “CPROVER”; H2020 FET OPEN 712689 SC2
Publisher:
IEEE Publisher's website
Pages:
43-48
Publication date:
2018-04-23
Acceptance date:
2017-11-10
DOI:
ISSN:
1558-1101
Pubs id:
pubs:796607
URN:
uri:d76c386c-f3e4-483e-941b-466585ce0360
UUID:
uuid:d76c386c-f3e4-483e-941b-466585ce0360
Local pid:
pubs:796607
ISBN:
978-3-9819263-0-9

Terms of use


Metrics



If you are the owner of this record, you can report an update to it here: Report update to this record

TO TOP