The Paths to Choreography Extraction

    Research output: Chapter in Book/Report/Conference proceedingArticle in proceedingsResearchpeer-review

    131 Downloads (Pure)


    Choreographies are global descriptions of interactions among concurrent components, most notably used in the settings of verification and synthesis of correct-by-construction software. They require a top-down approach: programmers first write choreographies, and then use them to verify or synthesize their programs. However, most software does not come with choreographies yet, which prevents their application. To attack this problem, previous work investigated choreography extraction, which automatically constructs a choreography that describes the behavior of a given set of programs or protocol specifications.

    We propose a new extraction methodology that improves on the state of the art: we can deal with programs that are equipped with state and internal computation; time complexity is dramatically better; and we capture programs that work by exploiting asynchronous communication.
    Original languageEnglish
    Title of host publicationFoundations of Software Science and Computation Structures : Proceedings of the 20th International Conference, FOSSACS 2017, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2017
    EditorsJavier Esparza, Andrzej S. Murawski
    Publication date2017
    ISBN (Print)978-3-662-54457-0
    ISBN (Electronic)978-3-662-54458-7
    Publication statusPublished - 2017
    Event20th International Conference on Foundations of Software Science and Computation Structures - Uppsala, Sweden
    Duration: 22. Apr 201729. Apr 2017
    Conference number: 20


    Conference20th International Conference on Foundations of Software Science and Computation Structures
    SeriesLecture Notes in Computer Science


    Dive into the research topics of 'The Paths to Choreography Extraction'. Together they form a unique fingerprint.

    Cite this