- The Paths to Choreography Extraction.
- Luís Cruz-Filipe, Kim S. Larsen, and Fabrizio Montesi.
In 20th International Conference on Foundations of Software Science and Computation Structures (FoSSaCS), volume 10203 of Lecture Notes in Computer Science, pages 424-440. Springer, 2017.
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
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.
- Link to the publication at the publisher's site - subscription may be required.
Text required by the publisher (if any):
The final publication is available at link.springer.com.
open access (398 KB)
The same as the publisher's version, when the publisher permits. Otherwise, the author's last version before the publisher's copyright; this is often exactly the same, but sometimes fonts, page numbers, figure numbers, etc. are different. It may also be a full version. However, it is safe to read this version, and at the same time cite the official version, as long as references to concrete locations, numbered theorems, etc. inside the article are avoided.
Other publications by the author.