Publications Search Tool

@inproceedings{Dingel1997b,

title = {Approximating Unity},

author = {Juergen Dingel},

editor = {David Garlan and Daniel Le Métayer},

url = {http://dx.doi.org/10.1007/3-540-63383-9_89},

doi = {10.1007/3-540-63383-9_89},

isbn = {978-3-540-69527-1},

year  = {1997},

date = {1997-01-01},

booktitle = {Second International Conference on Coordination Languages and Models (COORDINATION'97)},

pages = {320-337},

publisher = {Springer},

address = {Berlin, Germany. September 1-3, 1997},

abstract = {A framework for the stepwise refinement of UNITY programs with local variables is proposed. It is centered around two preorders. The first one compares program components with respect to a given context. Aside from being context-sensitive, this order also allows the introduction of local variables. The second preorder compares program contexts with respect to their discriminating power. Using these two relations, program refinement arises as a form of assumption/commitment reasoning. An example illustrates the use of the framework and presents some proof rules.},

keywords = {},

pubstate = {published},

tppubtype = {inproceedings}

}

@inproceedings{Baldamus1997b,

title = {Modal characterization of weak bisimulation for higher-order processes},

author = {Michael Baldamus and Juergen Dingel},

editor = {Michel Bidoit and Max Dauchet},

url = {http://dx.doi.org/10.1007/BFb0030604},

doi = {10.1007/BFb0030604},

isbn = {978-3-540-68517-3},

year  = {1997},

date = {1997-01-01},

booktitle = {7th International Joint Conference CAAP/FASE on Theory and Practice of Software Development (TAPSOFT'97)},

pages = {285-296},

publisher = {Springer},

address = {Lille, France. April 14-18, 1997},

abstract = {Context bisimulation [12, 1] has become an important notion of behavioural equivalence for higher-order processes. Weak forms of context bisimulation are particularly interesting, because of their high level of abstraction. We present a modal logic for this setting and provide a characterization of a variant of weak context bisimulation on second-order processes. We show how the logic permits compositional reasoning. In comparison to previous work by Amadio and Dam [2] on the strong case, our modal logic supports derived operators through a complete duality and thus constitutes an appealing extension of Hennessy-Milner logic.},

keywords = {},

pubstate = {published},

tppubtype = {inproceedings}

}

@inproceedings{Dingel1997,

title = {Approximating Unity},

author = {Juergen Dingel},

editor = {David Garlan and Daniel Le Métayer},

url = {http://dx.doi.org/10.1007/3-540-63383-9_89},

doi = {10.1007/3-540-63383-9_89},

isbn = {978-3-540-69527-1},

year  = {1997},

date = {1997-01-01},

booktitle = {Second International Conference on Coordination Languages and Models (COORDINATION'97)},

pages = {320-337},

publisher = {Springer},

address = {Berlin, Germany. September 1-3, 1997},

abstract = {A framework for the stepwise refinement of UNITY programs with local variables is proposed. It is centered around two preorders. The first one compares program components with respect to a given context. Aside from being context-sensitive, this order also allows the introduction of local variables. The second preorder compares program contexts with respect to their discriminating power. Using these two relations, program refinement arises as a form of assumption/commitment reasoning. An example illustrates the use of the framework and presents some proof rules.},

keywords = {},

pubstate = {published},

tppubtype = {inproceedings}

}

@inproceedings{Baldamus1997,

title = {Modal characterization of weak bisimulation for higher-order processes},

author = {Michael Baldamus and Juergen Dingel},

editor = {Michel Bidoit and Max Dauchet},

url = {http://dx.doi.org/10.1007/BFb0030604},

doi = {10.1007/BFb0030604},

isbn = {978-3-540-68517-3},

year  = {1997},

date = {1997-01-01},

booktitle = {7th International Joint Conference CAAP/FASE on Theory and Practice of Software Development (TAPSOFT'97)},

pages = {285-296},

publisher = {Springer},

address = {Lille, France. April 14-18, 1997},

abstract = {Context bisimulation [12, 1] has become an important notion of behavioural equivalence for higher-order processes. Weak forms of context bisimulation are particularly interesting, because of their high level of abstraction. We present a modal logic for this setting and provide a characterization of a variant of weak context bisimulation on second-order processes. We show how the logic permits compositional reasoning. In comparison to previous work by Amadio and Dam [2] on the strong case, our modal logic supports derived operators through a complete duality and thus constitutes an appealing extension of Hennessy-Milner logic.},

keywords = {},

pubstate = {published},

tppubtype = {inproceedings}

}

@inproceedings{Dingel:1996:MVS:646731.703856b,

title = {Modular Verification for Shared-Variable Concurrent Programs},

author = {Juergen Dingel},

url = {http://dl.acm.org/citation.cfm?id=646731.703856},

isbn = {3-540-61604-7},

year  = {1996},

date = {1996-01-01},

booktitle = {7th International Conference on Concurrency Theory (CONCUR'96)},

pages = {703-718},

publisher = {Springer},

address = {Pisa, Italy. August 26-29, 1996},

series = {CONCUR'96},

keywords = {},

pubstate = {published},

tppubtype = {inproceedings}

}

@inproceedings{Dingel:1996:MVS:646731.703856,

title = {Modular Verification for Shared-Variable Concurrent Programs},

author = {Juergen Dingel},

url = {http://dl.acm.org/citation.cfm?id=646731.703856},

isbn = {3-540-61604-7},

year  = {1996},

date = {1996-01-01},

booktitle = {7th International Conference on Concurrency Theory (CONCUR'96)},

pages = {703-718},

publisher = {Springer},

address = {Pisa, Italy. August 26-29, 1996},

series = {CONCUR'96},

keywords = {},

pubstate = {published},

tppubtype = {inproceedings}

}

@inproceedings{Dingel1995c,

title = {Model checking for infinite state systems using data abstraction, assumption-commitment style reasoning and theorem proving},

author = {Juergen Dingel and Thomas Filkorn},

editor = {Pierre Wolper},

url = {http://dx.doi.org/10.1007/3-540-60045-0_40},

doi = {10.1007/3-540-60045-0_40},

isbn = {978-3-540-49413-3},

year  = {1995},

date = {1995-01-01},

booktitle = {7th International Conference on Computer Aided Verification (CAV'95)},

pages = {54-69},

publisher = {Springer},

address = {Liège, Belgium. July 3-5, 1995},

abstract = {A method combining data abstraction, model checking and theorem proving is presented. It provides a semi-automatic, formal framework for proving arbitrary linear time temporal logic properties of infinite state reactive systems. The paper contains a complete case study to prove safety and liveness of an implementation of a scheduler for the readers/writers problem which uses unbounded queues and sets. We argue that the proposed framework could be automated to a very large extent making this approach feasible in an industrial environment.},

keywords = {},

pubstate = {published},

tppubtype = {inproceedings}

}

@inproceedings{Dingel1995bb,

title = {Canonical Derivations for the Single-Pushout Approach for Graph Transformation},

author = {Michael Loewe and Juergen Dingel},

year  = {1995},

date = {1995-01-01},

booktitle = {Dagstuhl Seminar on Graph Transformations in Computer Science},

pages = {54-69},

publisher = {Springer},

address = {Schloss Dagstuhl, Germany. January 1993},

keywords = {},

pubstate = {published},

tppubtype = {inproceedings}

}

@inproceedings{Dingel1995,

title = {Model checking for infinite state systems using data abstraction, assumption-commitment style reasoning and theorem proving},

author = {Juergen Dingel and Thomas Filkorn},

editor = {Pierre Wolper},

url = {http://dx.doi.org/10.1007/3-540-60045-0_40},

doi = {10.1007/3-540-60045-0_40},

isbn = {978-3-540-49413-3},

year  = {1995},

date = {1995-01-01},

booktitle = {7th International Conference on Computer Aided Verification (CAV'95)},

pages = {54-69},

publisher = {Springer},

address = {Liège, Belgium. July 3-5, 1995},

abstract = {A method combining data abstraction, model checking and theorem proving is presented. It provides a semi-automatic, formal framework for proving arbitrary linear time temporal logic properties of infinite state reactive systems. The paper contains a complete case study to prove safety and liveness of an implementation of a scheduler for the readers/writers problem which uses unbounded queues and sets. We argue that the proposed framework could be automated to a very large extent making this approach feasible in an industrial environment.},

keywords = {},

pubstate = {published},

tppubtype = {inproceedings}

}

@inproceedings{Dingel1995b,

title = {Canonical Derivations for the Single-Pushout Approach for Graph Transformation},

author = {Michael Loewe and Juergen Dingel},

year  = {1995},

date = {1995-01-01},

booktitle = {Dagstuhl Seminar on Graph Transformations in Computer Science},

pages = {54-69},

publisher = {Springer},

address = {Schloss Dagstuhl, Germany. January 1993},

keywords = {},

pubstate = {published},

tppubtype = {inproceedings}

}