---
res:
  bibo_abstract:
  - We present a computer-aided programming approach to concurrency. The approach
    allows programmers to program assuming a friendly, non-preemptive scheduler, and
    our synthesis procedure inserts synchronization to ensure that the final program
    works even with a preemptive scheduler. The correctness specification is implicit,
    inferred from the non-preemptive behavior. Let us consider sequences of calls
    that the program makes to an external interface. The specification requires that
    any such sequence produced under a preemptive scheduler should be included in
    the set of such sequences produced under a non-preemptive scheduler. The solution
    is based on a finitary abstraction, an algorithm for bounded language inclusion
    modulo an independence relation, and rules for inserting synchronization. We apply
    the approach to device-driver programming, where the driver threads call the software
    interface of the device and the API provided by the operating system. Our experiments
    demonstrate that our synthesis method is precise and efficient, and, since it
    does not require explicit specifications, is more practical than the conventional
    approach based on user-provided assertions.@eng
  bibo_authorlist:
  - foaf_Person:
      foaf_givenName: Pavol
      foaf_name: Cerny, Pavol
      foaf_surname: Cerny
      foaf_workInfoHomepage: http://www.librecat.org/personId=4DCBEFFE-F248-11E8-B48F-1D18A9856A87
  - foaf_Person:
      foaf_givenName: Edmund
      foaf_name: Clarke, Edmund
      foaf_surname: Clarke
  - foaf_Person:
      foaf_givenName: Thomas A
      foaf_name: Henzinger, Thomas A
      foaf_surname: Henzinger
      foaf_workInfoHomepage: http://www.librecat.org/personId=40876CD8-F248-11E8-B48F-1D18A9856A87
    orcid: 0000−0002−2985−7724
  - foaf_Person:
      foaf_givenName: Arjun
      foaf_name: Radhakrishna, Arjun
      foaf_surname: Radhakrishna
      foaf_workInfoHomepage: http://www.librecat.org/personId=3B51CAC4-F248-11E8-B48F-1D18A9856A87
  - foaf_Person:
      foaf_givenName: Leonid
      foaf_name: Ryzhyk, Leonid
      foaf_surname: Ryzhyk
  - foaf_Person:
      foaf_givenName: Roopsha
      foaf_name: Samanta, Roopsha
      foaf_surname: Samanta
      foaf_workInfoHomepage: http://www.librecat.org/personId=3D2AAC08-F248-11E8-B48F-1D18A9856A87
  - foaf_Person:
      foaf_givenName: Thorsten
      foaf_name: Tarrach, Thorsten
      foaf_surname: Tarrach
      foaf_workInfoHomepage: http://www.librecat.org/personId=3D6E8F2C-F248-11E8-B48F-1D18A9856A87
    orcid: 0000-0003-4409-8487
  bibo_doi: 10.1007/978-3-319-21668-3_11
  bibo_volume: 9207
  dct_date: 2015^xs_gYear
  dct_identifier:
  - UT:000491470400011
  dct_language: eng
  dct_publisher: Springer@
  dct_title: From non-preemptive to preemptive scheduling using synchronization synthesis@
...