publication . Other literature type . Conference object . 2019 . Embargo end date: 12 Jul 2019

Transferring Obligations Through Synchronizations

Hamin, Jafar; Jacobs, bart;
Open Access English
  • Published: 12 Jul 2019
  • Publisher: Schloss Dagstuhl - Leibniz-Zentrum fuer Informatik GmbH, Wadern/Saarbruecken, Germany
  • Country: Belgium
Abstract
One common approach for verifying safety properties of multithreaded programs is assigning appropriate permissions, such as ownership of a heap location, and obligations, such as an obligation to send a message on a channel, to each thread and making sure that each thread only performs the actions for which it has permissions and it also fulfills all of its obligations before it terminates. Although permissions can be transferred through synchronizations from a sender thread, where for example a message is sent or a condition variable is notified, to a receiver thread, where that message or that notification is received, in existing approaches obligations can on...
Persistent Identifiers
Subjects
free text keywords: Computer Science, 000 Computer science, knowledge, general works, Hoare logic, separation logic, modular program verification, synchronization, transferring obligations, deadlock-freedom
Related Organizations
Funded by
EC| VESSEDIA
Project
VESSEDIA
VERIFICATION ENGINEERING OF SAFETY AND SECURITY CRITICAL DYNAMIC INDUSTRIAL APPLICATIONS
  • Funder: European Commission (EC)
  • Project Code: 731453
  • Funding stream: H2020 | RIA
Any information missing or wrong?Report an Issue