Reachability Problems in Piecewise FIFO Systems

Autor: Naghmeh Ghafari, Arie Gurfinkel, Nils Klarlund, Richard J. Trefler

Publikováno v: ACM Transactions on Computational Logic. 13:1-33

Systems consisting of several finite components that communicate via unbounded perfect FIFO channels (i.e., FIFO systems) arise naturally in modeling distributed systems. Despite well-known difficulties in analyzing such systems, they are of signific

Externí odkaz: https://explore.openaire.eu/search/publication?articleId=doi_________::0e1c5131ea467246fcb155f4b2bf28b2
https://doi.org/10.1145/2071368.2071375

Regularity Results for FIFO Channels

Autor: Nils Klarlund, Richard J. Trefler

Publikováno v: Electronic Notes in Theoretical Computer Science. 128(6):21-36

FIFO channel systems, in which messages between processes are cached in queues, are fundamental to the modeling of concurrency. A great deal of effort has gone into identifying scenarios where reasoning about such systems is decidable, often through

Externí odkaz: https://explore.openaire.eu/search/publication?articleId=doi_dedup___::6f452fa8078c9aab45e0c020eab69fdf

A domain-specific language for regular sets of strings and trees

Autor: Nils Klarlund, Michael I. Schwartzbach

Publikováno v: DSL
Schwartzbach, M I & Klarlund, N 1999, ' A Domain-Specific Languane for Regular Sets of Strings and Trees ', I E E E Transactions on Software Engineering, vol. 25, no. 3, pp. 378-386 . https://doi.org/10.1109/32.798326

We propose a novel high level programming notation, called FIDO, that we have designed to concisely express regular sets of strings or trees. In particular, it can be viewed as a domain-specific language for the expression of finite state automata on

Externí odkaz: https://explore.openaire.eu/search/publication?articleId=doi_dedup___::7e802697c2e8dd176a80c9e1fc97f992
https://doi.org/10.1109/32.798326

Proving Nondeterministically Specified Safety Properties Using Progress Measures

Autor: Fred B. Schneider, Nils Klarlund

Publikováno v: Information and Computation. 107:151-170

Using the notion of progress measures, we discuss verification methods for proving that a program satisfies a property specified by an automaton having finite nondeterminism. Such automata can express any safety property. Previous methods, which can

Externí odkaz: https://explore.openaire.eu/search/publication?articleId=doi_dedup___::9b77ce87e864d8770ce4a72cad6d2923
https://doi.org/10.1006/inco.1993.1064

DART

Autor: Nils Klarlund, Patrice Godefroid, Koushik Sen

Publikováno v: PLDI

We present a new tool, named DART, for automatically testing software that combines three main techniques: (1) automated extraction of the interface of a program with its external environment using static source-code parsing; (2) automatic generation

Externí odkaz: https://explore.openaire.eu/search/publication?articleId=doi_dedup___::0566e471b02269be84f304799909682c
https://doi.org/10.1145/1065010.1065036