Journal article icon

Journal article

Incremental bounded model checking for embedded software

Abstract:

Program analysis is on the brink of mainstream usage in embedded systems development. Formal verification of behavioural requirements, finding runtime errors and test case generation are some of the most common applications of automated verification tools based on bounded model checking (BMC). Existing industrial tools for embedded software use an off-the-shelf bounded model checker and apply it iteratively to verify the program with an increasing number of unwindings. This approach unnecessa...

Expand abstract
Publication status:
Published
Peer review status:
Peer reviewed
Version:
Publisher's version

Actions


Access Document


Files:
Publisher copy:
10.1007/s00165-017-0419-1

Authors


More by this author
Institution:
University of Oxford
Department:
Oxford, MPLS, Computer Science
More by this author
Institution:
University of Oxford
Department:
Oxford, MPLS, Computer Science
More by this author
Institution:
University of Oxford
Department:
Oxford, MPLS, Computer Science
More by this author
Institution:
University of Oxford
Department:
Oxford, MPLS, Computer Science
Expand authors...
More from this funder
Grant:
Project 280053 “CPROVER”
Publisher:
Springer Verlag Publisher's website
Journal:
Formal Aspects of Computing Journal website
Publication date:
2017-02-22
Acceptance date:
2016-12-16
DOI:
EISSN:
1433-299X
ISSN:
0934-5043
Pubs id:
pubs:686091
URN:
uri:822cf6fd-788d-4a9d-89fc-770b04fb9c8b
UUID:
uuid:822cf6fd-788d-4a9d-89fc-770b04fb9c8b
Local pid:
pubs:686091

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