skip to main content
Ngôn ngữ:
Giới hạn tìm kiếm: Giới hạn tìm kiếm: Dạng tài nguyên Hiển thị kết quả với: Hiển thị kết quả với: Chỉ mục

Static Code Verification Through Process Models

Joosten, Sebastiaan J. C. ; Huisman, Marieke ; Margaria, Tiziana ; Steffen, Bernhard; Formal Methods and Tools

Leveraging Applications of Formal Methods, Verification and Validation. Distributed Systems, 2018, pp.343-354 [Tạp chí có phản biện]

ISBN: 978-3-030-03423-8 ; ISBN: 978-3-030-03424-5

Toàn văn sẵn có

Trích dẫn Trích dẫn bởi
  • Nhan đề:
    Static Code Verification Through Process Models
  • Tác giả: Joosten, Sebastiaan J. C. ; Huisman, Marieke ; Margaria, Tiziana ; Steffen, Bernhard
  • Formal Methods and Tools
  • Là 1 phần của: Leveraging Applications of Formal Methods, Verification and Validation. Distributed Systems, 2018, pp.343-354
  • Mô tả: In this extended abstract, we combine two techniques for program verification: one is Hoare-style static verification, and the other is model checking of state transition systems. We relate the two techniques semantically through the use of a ghost variable. Actions that are performed by the program can be logged into this variable, building an event structure as its value. We require the event structure to grow incrementally by construction, giving it behavior suitable for model checking. Invariants specify a correspondence between the event structure and the program state. The combined power of model checking and static code verification with separation logic based reasoning, gives a new and intuitive way to do program verification. We describe our idea in a tool-agnostic way: we do not give implementation details, nor do we assume that the static verification tool to which our idea might apply is implemented in a particular way.
  • Ngôn ngữ: English
  • Số nhận dạng: ISBN: 978-3-030-03423-8 ; ISBN: 978-3-030-03424-5

Đang tìm Cơ sở dữ liệu bên ngoài...