---
_id: '517'
abstract:
- lang: eng
text: In the Semantic (Web) Services area, services are considered black boxes with
a semantic description of their interfaces as to allow for precise service selection
and configuration. The semantic description is usually grounded on domain-specific
concepts as modeled in ontologies. This accounts for types used in service signatures,
but also predicates occurring in preconditions and effects of services. Ontologies,
in particular those enhanced with rules, capture the knowledge of domain experts
on properties of and relations between domain concepts. In this paper, we present
a verification technique for service compositions which makes use of this domain
knowledge. We consider a service composition to be an assembly of services of
which we just know signatures, preconditions, and effects. We aim at proving that
a composition satisfies a (user-defined) requirement, specified in terms of guaranteed
preconditions and required postconditions. As an underlying verification engine
we use an SMT solver. To take advantage of the domain knowledge (and often, to
enable verification at all), the knowledge is fed into the solver in the form of
sorts, uninterpreted functions and in particular assertions as to enhance the
solver’s reasoning capabilities. Thereby, we allow for deductions within a domain
previously unknown to the solver. We exemplify our technique on a case study from
the area of water network optimization software.
author:
- first_name: Sven
full_name: Walther, Sven
last_name: Walther
- first_name: Heike
full_name: Wehrheim, Heike
id: '573'
last_name: Wehrheim
citation:
ama: 'Walther S, Wehrheim H. Knowledge-Based Verification of Service Compositions
- An SMT approach. In: Proceedings of the 18th IEEE International Conference
on Engineering of Complex Computer Systems (ICECCS). ; 2013:24-32. doi:10.1109/ICECCS.2013.14'
apa: Walther, S., & Wehrheim, H. (2013). Knowledge-Based Verification of Service
Compositions - An SMT approach. In Proceedings of the 18th IEEE International
Conference on Engineering of Complex Computer Systems (ICECCS) (pp. 24–32).
https://doi.org/10.1109/ICECCS.2013.14
bibtex: '@inproceedings{Walther_Wehrheim_2013, title={Knowledge-Based Verification
of Service Compositions - An SMT approach}, DOI={10.1109/ICECCS.2013.14},
booktitle={Proceedings of the 18th IEEE International Conference on Engineering
of Complex Computer Systems (ICECCS)}, author={Walther, Sven and Wehrheim, Heike},
year={2013}, pages={24–32} }'
chicago: Walther, Sven, and Heike Wehrheim. “Knowledge-Based Verification of Service
Compositions - An SMT Approach.” In Proceedings of the 18th IEEE International
Conference on Engineering of Complex Computer Systems (ICECCS), 24–32, 2013.
https://doi.org/10.1109/ICECCS.2013.14.
ieee: S. Walther and H. Wehrheim, “Knowledge-Based Verification of Service Compositions
- An SMT approach,” in Proceedings of the 18th IEEE International Conference
on Engineering of Complex Computer Systems (ICECCS), 2013, pp. 24–32.
mla: Walther, Sven, and Heike Wehrheim. “Knowledge-Based Verification of Service
Compositions - An SMT Approach.” Proceedings of the 18th IEEE International
Conference on Engineering of Complex Computer Systems (ICECCS), 2013, pp.
24–32, doi:10.1109/ICECCS.2013.14.
short: 'S. Walther, H. Wehrheim, in: Proceedings of the 18th IEEE International
Conference on Engineering of Complex Computer Systems (ICECCS), 2013, pp. 24–32.'
date_created: 2017-10-17T12:42:33Z
date_updated: 2022-01-06T07:01:41Z
ddc:
- '000'
department:
- _id: '77'
doi: 10.1109/ICECCS.2013.14
file:
- access_level: closed
content_type: application/pdf
creator: ups
date_created: 2018-11-02T13:26:08Z
date_updated: 2018-11-02T13:26:08Z
file_id: '5248'
file_name: 06601801.pdf
file_size: 217085
relation: main_file
file_date_updated: 2018-11-02T13:26:08Z
has_accepted_license: '1'
language:
- iso: eng
page: '24 - 32 '
project:
- _id: '1'
name: SFB 901
- _id: '11'
name: SFB 901 - Subprojekt B3
- _id: '3'
name: SFB 901 - Project Area B
publication: Proceedings of the 18th IEEE International Conference on Engineering
of Complex Computer Systems (ICECCS)
status: public
title: Knowledge-Based Verification of Service Compositions - An SMT approach
type: conference
user_id: '477'
year: '2013'
...
---
_id: '3180'
author:
- first_name: Oleg
full_name: Travkin, Oleg
last_name: Travkin
- first_name: Heike
full_name: Wehrheim, Heike
id: '573'
last_name: Wehrheim
- first_name: Gerhard
full_name: Schellhorn, Gerhard
last_name: Schellhorn
citation:
ama: Travkin O, Wehrheim H, Schellhorn G. Proving Linearizability of Multiset with
Local Proof Obligations. {ECEASST}. 2012.
apa: Travkin, O., Wehrheim, H., & Schellhorn, G. (2012). Proving Linearizability
of Multiset with Local Proof Obligations. {ECEASST}.
bibtex: '@article{Travkin_Wehrheim_Schellhorn_2012, title={Proving Linearizability
of Multiset with Local Proof Obligations}, journal={{ECEASST}}, author={Travkin,
Oleg and Wehrheim, Heike and Schellhorn, Gerhard}, year={2012} }'
chicago: Travkin, Oleg, Heike Wehrheim, and Gerhard Schellhorn. “Proving Linearizability
of Multiset with Local Proof Obligations.” {ECEASST}, 2012.
ieee: O. Travkin, H. Wehrheim, and G. Schellhorn, “Proving Linearizability of Multiset
with Local Proof Obligations,” {ECEASST}, 2012.
mla: Travkin, Oleg, et al. “Proving Linearizability of Multiset with Local Proof
Obligations.” {ECEASST}, 2012.
short: O. Travkin, H. Wehrheim, G. Schellhorn, {ECEASST} (2012).
date_created: 2018-06-13T08:16:49Z
date_updated: 2022-01-06T06:59:03Z
department:
- _id: '77'
publication: '{ECEASST}'
status: public
title: Proving Linearizability of Multiset with Local Proof Obligations
type: journal_article
user_id: '29719'
year: '2012'
...
---
_id: '3181'
author:
- first_name: Thomas
full_name: Ruhroth, Thomas
last_name: Ruhroth
- first_name: Heike
full_name: Wehrheim, Heike
id: '573'
last_name: Wehrheim
citation:
ama: Ruhroth T, Wehrheim H. Model evolution and refinement. Sci Comput Program.
2012;(3):270--289. doi:10.1016/j.scico.2011.04.007
apa: Ruhroth, T., & Wehrheim, H. (2012). Model evolution and refinement. Sci.
Comput. Program., (3), 270--289. https://doi.org/10.1016/j.scico.2011.04.007
bibtex: '@article{Ruhroth_Wehrheim_2012, title={Model evolution and refinement},
DOI={10.1016/j.scico.2011.04.007},
number={3}, journal={Sci. Comput. Program.}, author={Ruhroth, Thomas and Wehrheim,
Heike}, year={2012}, pages={270--289} }'
chicago: 'Ruhroth, Thomas, and Heike Wehrheim. “Model Evolution and Refinement.”
Sci. Comput. Program., no. 3 (2012): 270--289. https://doi.org/10.1016/j.scico.2011.04.007.'
ieee: T. Ruhroth and H. Wehrheim, “Model evolution and refinement,” Sci. Comput.
Program., no. 3, pp. 270--289, 2012.
mla: Ruhroth, Thomas, and Heike Wehrheim. “Model Evolution and Refinement.” Sci.
Comput. Program., no. 3, 2012, pp. 270--289, doi:10.1016/j.scico.2011.04.007.
short: T. Ruhroth, H. Wehrheim, Sci. Comput. Program. (2012) 270--289.
date_created: 2018-06-13T08:17:58Z
date_updated: 2022-01-06T06:59:03Z
department:
- _id: '77'
doi: 10.1016/j.scico.2011.04.007
issue: '3'
page: 270--289
publication: Sci. Comput. Program.
status: public
title: Model evolution and refinement
type: journal_article
user_id: '29719'
year: '2012'
...
---
_id: '3182'
author:
- first_name: Gerhard
full_name: Schellhorn, Gerhard
last_name: Schellhorn
- first_name: Heike
full_name: Wehrheim, Heike
id: '573'
last_name: Wehrheim
- first_name: John
full_name: Derrick, John
last_name: Derrick
citation:
ama: 'Schellhorn G, Wehrheim H, Derrick J. How to Prove Algorithms Linearisable.
In: Madhusudan P, A. Seshia S, eds. Computer Aided Verification - 24th International
Conference, {CAV} 2012, Berkeley, CA, USA, July 7-13, 2012 Proceedings. Lecture
Notes in Computer Science. ; 2012:243--259. doi:10.1007/978-3-642-31424-7_21'
apa: Schellhorn, G., Wehrheim, H., & Derrick, J. (2012). How to Prove Algorithms
Linearisable. In P. Madhusudan & S. A. Seshia (Eds.), Computer Aided Verification
- 24th International Conference, {CAV} 2012, Berkeley, CA, USA, July 7-13, 2012
Proceedings (pp. 243--259). https://doi.org/10.1007/978-3-642-31424-7_21
bibtex: '@inproceedings{Schellhorn_Wehrheim_Derrick_2012, series={Lecture Notes
in Computer Science}, title={How to Prove Algorithms Linearisable}, DOI={10.1007/978-3-642-31424-7_21},
booktitle={Computer Aided Verification - 24th International Conference, {CAV}
2012, Berkeley, CA, USA, July 7-13, 2012 Proceedings}, author={Schellhorn, Gerhard
and Wehrheim, Heike and Derrick, John}, editor={Madhusudan, P. and A. Seshia,
SanjitEditors}, year={2012}, pages={243--259}, collection={Lecture Notes in Computer
Science} }'
chicago: Schellhorn, Gerhard, Heike Wehrheim, and John Derrick. “How to Prove Algorithms
Linearisable.” In Computer Aided Verification - 24th International Conference,
{CAV} 2012, Berkeley, CA, USA, July 7-13, 2012 Proceedings, edited by P. Madhusudan
and Sanjit A. Seshia, 243--259. Lecture Notes in Computer Science, 2012. https://doi.org/10.1007/978-3-642-31424-7_21.
ieee: G. Schellhorn, H. Wehrheim, and J. Derrick, “How to Prove Algorithms Linearisable,”
in Computer Aided Verification - 24th International Conference, {CAV} 2012,
Berkeley, CA, USA, July 7-13, 2012 Proceedings, 2012, pp. 243--259.
mla: Schellhorn, Gerhard, et al. “How to Prove Algorithms Linearisable.” Computer
Aided Verification - 24th International Conference, {CAV} 2012, Berkeley, CA,
USA, July 7-13, 2012 Proceedings, edited by P. Madhusudan and Sanjit A. Seshia,
2012, pp. 243--259, doi:10.1007/978-3-642-31424-7_21.
short: 'G. Schellhorn, H. Wehrheim, J. Derrick, in: P. Madhusudan, S. A. Seshia
(Eds.), Computer Aided Verification - 24th International Conference, {CAV} 2012,
Berkeley, CA, USA, July 7-13, 2012 Proceedings, 2012, pp. 243--259.'
date_created: 2018-06-13T08:19:33Z
date_updated: 2022-01-06T06:59:03Z
department:
- _id: '77'
doi: 10.1007/978-3-642-31424-7_21
editor:
- first_name: P.
full_name: Madhusudan, P.
last_name: Madhusudan
- first_name: Sanjit
full_name: A. Seshia, Sanjit
last_name: A. Seshia
page: 243--259
publication: Computer Aided Verification - 24th International Conference, {CAV} 2012,
Berkeley, CA, USA, July 7-13, 2012 Proceedings
series_title: Lecture Notes in Computer Science
status: public
title: How to Prove Algorithms Linearisable
type: conference
user_id: '29719'
year: '2012'
...
---
_id: '590'
abstract:
- lang: eng
text: 'Predicate abstraction is an established technique for reducing the size of
the state space during verification. In this paper, we extend predication abstraction
with block-abstraction memoization (BAM), which exploits the fact that blocks
are often executed several times in a program. The verification can thus benefit
from caching the values of previous block analyses and reusing them upon next
entry into a block. In addition to function bodies, BAM also performs well for
nested loops. To further increase effectiveness, block memoization has been integrated
with lazy abstraction adopting a lazy strategy for cache refinement. Together,
this achieves significant performance increases: our tool (an implementation within
the configurable program analysis framework CPAchecker) has won the Competition
on Software Verification 2012 in the category “Overall”.'
author:
- first_name: Daniel
full_name: Wonisch, Daniel
last_name: Wonisch
- first_name: Heike
full_name: Wehrheim, Heike
id: '573'
last_name: Wehrheim
citation:
ama: 'Wonisch D, Wehrheim H. Predicate Analysis with Block-Abstraction Memoization.
In: Proceedings of the 14th International Conference on Formal Engineering
Methods (ICFEM). LNCS. ; 2012:332-347. doi:10.1007/978-3-642-34281-3_24'
apa: Wonisch, D., & Wehrheim, H. (2012). Predicate Analysis with Block-Abstraction
Memoization. In Proceedings of the 14th International Conference on Formal
Engineering Methods (ICFEM) (pp. 332–347). https://doi.org/10.1007/978-3-642-34281-3_24
bibtex: '@inproceedings{Wonisch_Wehrheim_2012, series={LNCS}, title={Predicate Analysis
with Block-Abstraction Memoization}, DOI={10.1007/978-3-642-34281-3_24},
booktitle={Proceedings of the 14th International Conference on Formal Engineering
Methods (ICFEM)}, author={Wonisch, Daniel and Wehrheim, Heike}, year={2012}, pages={332–347},
collection={LNCS} }'
chicago: Wonisch, Daniel, and Heike Wehrheim. “Predicate Analysis with Block-Abstraction
Memoization.” In Proceedings of the 14th International Conference on Formal
Engineering Methods (ICFEM), 332–47. LNCS, 2012. https://doi.org/10.1007/978-3-642-34281-3_24.
ieee: D. Wonisch and H. Wehrheim, “Predicate Analysis with Block-Abstraction Memoization,”
in Proceedings of the 14th International Conference on Formal Engineering Methods
(ICFEM), 2012, pp. 332–347.
mla: Wonisch, Daniel, and Heike Wehrheim. “Predicate Analysis with Block-Abstraction
Memoization.” Proceedings of the 14th International Conference on Formal Engineering
Methods (ICFEM), 2012, pp. 332–47, doi:10.1007/978-3-642-34281-3_24.
short: 'D. Wonisch, H. Wehrheim, in: Proceedings of the 14th International Conference
on Formal Engineering Methods (ICFEM), 2012, pp. 332–347.'
date_created: 2017-10-17T12:42:47Z
date_updated: 2022-01-06T07:02:46Z
ddc:
- '040'
department:
- _id: '77'
doi: 10.1007/978-3-642-34281-3_24
file:
- access_level: closed
content_type: application/pdf
creator: florida
date_created: 2018-03-15T08:33:56Z
date_updated: 2018-03-15T08:33:56Z
file_id: '1258'
file_name: 590-WonischWehrheim2012.pdf
file_size: 320901
relation: main_file
success: 1
file_date_updated: 2018-03-15T08:33:56Z
has_accepted_license: '1'
language:
- iso: eng
page: 332-347
project:
- _id: '1'
name: SFB 901
- _id: '12'
name: SFB 901 - Subprojekt B4
- _id: '3'
name: SFB 901 - Project Area B
publication: Proceedings of the 14th International Conference on Formal Engineering
Methods (ICFEM)
series_title: LNCS
status: public
title: Predicate Analysis with Block-Abstraction Memoization
type: conference
user_id: '477'
year: '2012'
...
---
_id: '608'
abstract:
- lang: eng
text: 'Predicate abstraction is an established technique in software verification.
It inherently includes an abstraction refinement loop successively adding predicates
until the right level of abstraction is found. For concurrent systems, predicate
abstraction can be combined with spotlight abstraction, further reducing the state
space by abstracting away certain processes. Refinement then has to decide whether
to add a new predicate or a new process. Selecting the right predicates and processes
is a crucial task: The positive effect of abstraction may be compromised by unfavourable
refinement decisions. Here we present a heuristic approach to abstraction refinement.
The basis for a decision is a set of refinement candidates, derived by multiple
counterexample-generation. Candidates are evaluated with respect to their influence
on other components in the system. Experimental results show that our technique
can significantly speed up verification as compared to a naive abstraction refinement.'
author:
- first_name: Nils
full_name: Timm, Nils
last_name: Timm
- first_name: Heike
full_name: Wehrheim, Heike
id: '573'
last_name: Wehrheim
- first_name: Mike
full_name: Czech, Mike
last_name: Czech
citation:
ama: 'Timm N, Wehrheim H, Czech M. Heuristic-Guided Abstraction Refinement for Concurrent
Systems. In: Proceedings of the 14th International Conference on Formal Engineering
Methods (ICFEM). LNCS. ; 2012:348-363. doi:10.1007/978-3-642-34281-3_25'
apa: Timm, N., Wehrheim, H., & Czech, M. (2012). Heuristic-Guided Abstraction
Refinement for Concurrent Systems. In Proceedings of the 14th International
Conference on Formal Engineering Methods (ICFEM) (pp. 348–363). https://doi.org/10.1007/978-3-642-34281-3_25
bibtex: '@inproceedings{Timm_Wehrheim_Czech_2012, series={LNCS}, title={Heuristic-Guided
Abstraction Refinement for Concurrent Systems}, DOI={10.1007/978-3-642-34281-3_25},
booktitle={Proceedings of the 14th International Conference on Formal Engineering
Methods (ICFEM)}, author={Timm, Nils and Wehrheim, Heike and Czech, Mike}, year={2012},
pages={348–363}, collection={LNCS} }'
chicago: Timm, Nils, Heike Wehrheim, and Mike Czech. “Heuristic-Guided Abstraction
Refinement for Concurrent Systems.” In Proceedings of the 14th International
Conference on Formal Engineering Methods (ICFEM), 348–63. LNCS, 2012. https://doi.org/10.1007/978-3-642-34281-3_25.
ieee: N. Timm, H. Wehrheim, and M. Czech, “Heuristic-Guided Abstraction Refinement
for Concurrent Systems,” in Proceedings of the 14th International Conference
on Formal Engineering Methods (ICFEM), 2012, pp. 348–363.
mla: Timm, Nils, et al. “Heuristic-Guided Abstraction Refinement for Concurrent
Systems.” Proceedings of the 14th International Conference on Formal Engineering
Methods (ICFEM), 2012, pp. 348–63, doi:10.1007/978-3-642-34281-3_25.
short: 'N. Timm, H. Wehrheim, M. Czech, in: Proceedings of the 14th International
Conference on Formal Engineering Methods (ICFEM), 2012, pp. 348–363.'
date_created: 2017-10-17T12:42:50Z
date_updated: 2022-01-06T07:02:52Z
ddc:
- '040'
department:
- _id: '77'
doi: 10.1007/978-3-642-34281-3_25
file:
- access_level: closed
content_type: application/pdf
creator: florida
date_created: 2018-03-15T08:15:33Z
date_updated: 2018-03-15T08:15:33Z
file_id: '1250'
file_name: 608-Timm2013-0main.pdf
file_size: 396337
relation: main_file
success: 1
file_date_updated: 2018-03-15T08:15:33Z
has_accepted_license: '1'
language:
- iso: eng
page: 348-363
project:
- _id: '1'
name: SFB 901
- _id: '12'
name: SFB 901 - Subprojekt B4
- _id: '3'
name: SFB 901 - Project Area B
publication: Proceedings of the 14th International Conference on Formal Engineering
Methods (ICFEM)
series_title: LNCS
status: public
title: Heuristic-Guided Abstraction Refinement for Concurrent Systems
type: conference
user_id: '477'
year: '2012'
...
---
_id: '627'
abstract:
- lang: eng
text: Block Abstraction Memoization (ABM) is a technique in software model checking
that exploits the modularity of programs during verification by caching. To this
end, ABM records the results of block analyses and reuses them if possible when
revisiting the same block again. In this paper we present an implementation of
ABM into the predicate-analysis component of the software-verification framework
CPAchecker. With our participation at the Competition on Software Verification
we aim at providing evidence that ABM can not only substantially increase the
efficiency of predicate analysis but also enables verification of a wider range
of programs.
author:
- first_name: Daniel
full_name: Wonisch, Daniel
last_name: Wonisch
citation:
ama: 'Wonisch D. Block Abstraction Memoization for CPAchecker. In: Proceedings
of the 18th International Conference on Tools and Algorithms for the Construction
and Analysis of Systems (TACAS). LNCS. ; 2012:531-533. doi:10.1007/978-3-642-28756-5_41'
apa: Wonisch, D. (2012). Block Abstraction Memoization for CPAchecker. In Proceedings
of the 18th International Conference on Tools and Algorithms for the Construction
and Analysis of Systems (TACAS) (pp. 531–533). https://doi.org/10.1007/978-3-642-28756-5_41
bibtex: '@inproceedings{Wonisch_2012, series={LNCS}, title={Block Abstraction Memoization
for CPAchecker}, DOI={10.1007/978-3-642-28756-5_41},
booktitle={Proceedings of the 18th International Conference on Tools and Algorithms
for the Construction and Analysis of Systems (TACAS)}, author={Wonisch, Daniel},
year={2012}, pages={531–533}, collection={LNCS} }'
chicago: Wonisch, Daniel. “Block Abstraction Memoization for CPAchecker.” In Proceedings
of the 18th International Conference on Tools and Algorithms for the Construction
and Analysis of Systems (TACAS), 531–33. LNCS, 2012. https://doi.org/10.1007/978-3-642-28756-5_41.
ieee: D. Wonisch, “Block Abstraction Memoization for CPAchecker,” in Proceedings
of the 18th International Conference on Tools and Algorithms for the Construction
and Analysis of Systems (TACAS), 2012, pp. 531–533.
mla: Wonisch, Daniel. “Block Abstraction Memoization for CPAchecker.” Proceedings
of the 18th International Conference on Tools and Algorithms for the Construction
and Analysis of Systems (TACAS), 2012, pp. 531–33, doi:10.1007/978-3-642-28756-5_41.
short: 'D. Wonisch, in: Proceedings of the 18th International Conference on Tools
and Algorithms for the Construction and Analysis of Systems (TACAS), 2012, pp.
531–533.'
date_created: 2017-10-17T12:42:54Z
date_updated: 2022-01-06T07:02:59Z
ddc:
- '040'
department:
- _id: '77'
doi: 10.1007/978-3-642-28756-5_41
file:
- access_level: closed
content_type: application/pdf
creator: florida
date_created: 2018-03-15T06:46:05Z
date_updated: 2018-03-15T06:46:05Z
file_id: '1242'
file_name: 627-WonischSV-Comp2012_01.pdf
file_size: 184000
relation: main_file
success: 1
file_date_updated: 2018-03-15T06:46:05Z
has_accepted_license: '1'
language:
- iso: eng
page: 531-533
project:
- _id: '1'
name: SFB 901
- _id: '12'
name: SFB 901 - Subprojekt B4
- _id: '3'
name: SFB 901 - Project Area B
publication: Proceedings of the 18th International Conference on Tools and Algorithms
for the Construction and Analysis of Systems (TACAS)
series_title: LNCS
status: public
title: Block Abstraction Memoization for CPAchecker
type: conference
user_id: '477'
year: '2012'
...
---
_id: '565'
abstract:
- lang: eng
text: 'In model-driven development of multi-layer systems (e.g. application, platform
and infrastructure), each layer is usually described by separate models. When
generating analysis models or code, these separate models rst of all need to be
linked. Hence, existing model transformations for single layers cannot be simply
re-used. In this paper, we present a modular approach to the transformation of
multi-layer systems. It employs model weaving to dene the interconnections between
models of dierent layers. The weaving models themselves are subject to model transformations:
The result of transforming a weaving model constitutes a conguration for the models
obtained by transforming single layers, thereby allowing for a re-use of existing
model transformations. We exemplify our approach by the generation of analysis
models for component-based software.'
author:
- first_name: Galina
full_name: Besova, Galina
last_name: Besova
- first_name: Sven
full_name: Walther, Sven
last_name: Walther
- first_name: Heike
full_name: Wehrheim, Heike
id: '573'
last_name: Wehrheim
- first_name: Steffen
full_name: Becker, Steffen
last_name: Becker
citation:
ama: 'Besova G, Walther S, Wehrheim H, Becker S. Weaving-based configuration and
modular transformation of multi-layer systems. In: Proceedings of the 15th
International Conference on Model Driven Engineering Languages & Systems (MoDELS).
LNCS. ; 2012:776-792. doi:10.1007/978-3-642-33666-9_49'
apa: Besova, G., Walther, S., Wehrheim, H., & Becker, S. (2012). Weaving-based
configuration and modular transformation of multi-layer systems. In Proceedings
of the 15th International Conference on Model Driven Engineering Languages &
Systems (MoDELS) (pp. 776–792). https://doi.org/10.1007/978-3-642-33666-9_49
bibtex: '@inproceedings{Besova_Walther_Wehrheim_Becker_2012, series={LNCS}, title={Weaving-based
configuration and modular transformation of multi-layer systems}, DOI={10.1007/978-3-642-33666-9_49},
booktitle={Proceedings of the 15th International Conference on Model Driven Engineering
Languages & Systems (MoDELS)}, author={Besova, Galina and Walther, Sven and
Wehrheim, Heike and Becker, Steffen}, year={2012}, pages={776–792}, collection={LNCS}
}'
chicago: Besova, Galina, Sven Walther, Heike Wehrheim, and Steffen Becker. “Weaving-Based
Configuration and Modular Transformation of Multi-Layer Systems.” In Proceedings
of the 15th International Conference on Model Driven Engineering Languages &
Systems (MoDELS), 776–92. LNCS, 2012. https://doi.org/10.1007/978-3-642-33666-9_49.
ieee: G. Besova, S. Walther, H. Wehrheim, and S. Becker, “Weaving-based configuration
and modular transformation of multi-layer systems,” in Proceedings of the 15th
International Conference on Model Driven Engineering Languages & Systems (MoDELS),
2012, pp. 776–792.
mla: Besova, Galina, et al. “Weaving-Based Configuration and Modular Transformation
of Multi-Layer Systems.” Proceedings of the 15th International Conference on
Model Driven Engineering Languages & Systems (MoDELS), 2012, pp. 776–92,
doi:10.1007/978-3-642-33666-9_49.
short: 'G. Besova, S. Walther, H. Wehrheim, S. Becker, in: Proceedings of the 15th
International Conference on Model Driven Engineering Languages & Systems (MoDELS),
2012, pp. 776–792.'
date_created: 2017-10-17T12:42:42Z
date_updated: 2022-01-06T07:02:20Z
ddc:
- '040'
department:
- _id: '77'
doi: 10.1007/978-3-642-33666-9_49
file:
- access_level: closed
content_type: application/pdf
creator: florida
date_created: 2018-03-15T10:24:06Z
date_updated: 2018-03-15T10:24:06Z
file_id: '1276'
file_name: 565-Besova_et_al._-_2012_-_Weaving-Based_Configuration_and_Modular_Transformation_of_Multi-layer_Systems_01.pdf
file_size: 589972
relation: main_file
success: 1
file_date_updated: 2018-03-15T10:24:06Z
has_accepted_license: '1'
language:
- iso: eng
page: 776-792
project:
- _id: '1'
name: SFB 901
- _id: '11'
name: SFB 901 - Subprojekt B3
- _id: '3'
name: SFB 901 - Project Area B
publication: Proceedings of the 15th International Conference on Model Driven Engineering
Languages & Systems (MoDELS)
series_title: LNCS
status: public
title: Weaving-based configuration and modular transformation of multi-layer systems
type: conference
user_id: '477'
year: '2012'
...
---
_id: '3183'
author:
- first_name: Steve
full_name: Schneider, Steve
last_name: Schneider
- first_name: Helen
full_name: Treharne, Helen
last_name: Treharne
- first_name: Heike
full_name: Wehrheim, Heike
id: '573'
last_name: Wehrheim
citation:
ama: 'Schneider S, Treharne H, Wehrheim H. Bounded Retransmission in Event-B{\(\parallel\)}CSP:
a Case Study. Electr Notes Theor Comput Sci. 2011:69--80. doi:10.1016/j.entcs.2011.11.019'
apa: 'Schneider, S., Treharne, H., & Wehrheim, H. (2011). Bounded Retransmission
in Event-B{\(\parallel\)}CSP: a Case Study. Electr. Notes Theor. Comput. Sci.,
69--80. https://doi.org/10.1016/j.entcs.2011.11.019'
bibtex: '@article{Schneider_Treharne_Wehrheim_2011, title={Bounded Retransmission
in Event-B{\(\parallel\)}CSP: a Case Study}, DOI={10.1016/j.entcs.2011.11.019},
journal={Electr. Notes Theor. Comput. Sci.}, author={Schneider, Steve and Treharne,
Helen and Wehrheim, Heike}, year={2011}, pages={69--80} }'
chicago: 'Schneider, Steve, Helen Treharne, and Heike Wehrheim. “Bounded Retransmission
in Event-B{\(\parallel\)}CSP: A Case Study.” Electr. Notes Theor. Comput. Sci.,
2011, 69--80. https://doi.org/10.1016/j.entcs.2011.11.019.'
ieee: 'S. Schneider, H. Treharne, and H. Wehrheim, “Bounded Retransmission in Event-B{\(\parallel\)}CSP:
a Case Study,” Electr. Notes Theor. Comput. Sci., pp. 69--80, 2011.'
mla: 'Schneider, Steve, et al. “Bounded Retransmission in Event-B{\(\parallel\)}CSP:
A Case Study.” Electr. Notes Theor. Comput. Sci., 2011, pp. 69--80, doi:10.1016/j.entcs.2011.11.019.'
short: S. Schneider, H. Treharne, H. Wehrheim, Electr. Notes Theor. Comput. Sci.
(2011) 69--80.
date_created: 2018-06-13T08:20:47Z
date_updated: 2022-01-06T06:59:03Z
department:
- _id: '77'
doi: 10.1016/j.entcs.2011.11.019
page: 69--80
publication: Electr. Notes Theor. Comput. Sci.
status: public
title: 'Bounded Retransmission in Event-B{\(\parallel\)}CSP: a Case Study'
type: journal_article
user_id: '29719'
year: '2011'
...
---
_id: '3184'
author:
- first_name: John
full_name: Derrick, John
last_name: Derrick
- first_name: Gerhard
full_name: Schellhorn, Gerhard
last_name: Schellhorn
- first_name: Heike
full_name: Wehrheim, Heike
id: '573'
last_name: Wehrheim
citation:
ama: Derrick J, Schellhorn G, Wehrheim H. Mechanically verified proof obligations
for linearizability. {ACM} Trans Program Lang Syst. 2011;(1):4:1--4:43.
doi:10.1145/1889997.1890001
apa: Derrick, J., Schellhorn, G., & Wehrheim, H. (2011). Mechanically verified
proof obligations for linearizability. {ACM} Trans. Program. Lang. Syst.,
(1), 4:1--4:43. https://doi.org/10.1145/1889997.1890001
bibtex: '@article{Derrick_Schellhorn_Wehrheim_2011, title={Mechanically verified
proof obligations for linearizability}, DOI={10.1145/1889997.1890001},
number={1}, journal={{ACM} Trans. Program. Lang. Syst.}, author={Derrick, John
and Schellhorn, Gerhard and Wehrheim, Heike}, year={2011}, pages={4:1--4:43} }'
chicago: 'Derrick, John, Gerhard Schellhorn, and Heike Wehrheim. “Mechanically Verified
Proof Obligations for Linearizability.” {ACM} Trans. Program. Lang. Syst.,
no. 1 (2011): 4:1--4:43. https://doi.org/10.1145/1889997.1890001.'
ieee: J. Derrick, G. Schellhorn, and H. Wehrheim, “Mechanically verified proof obligations
for linearizability,” {ACM} Trans. Program. Lang. Syst., no. 1, pp. 4:1--4:43,
2011.
mla: Derrick, John, et al. “Mechanically Verified Proof Obligations for Linearizability.”
{ACM} Trans. Program. Lang. Syst., no. 1, 2011, pp. 4:1--4:43, doi:10.1145/1889997.1890001.
short: J. Derrick, G. Schellhorn, H. Wehrheim, {ACM} Trans. Program. Lang. Syst.
(2011) 4:1--4:43.
date_created: 2018-06-13T08:22:02Z
date_updated: 2022-01-06T06:59:03Z
department:
- _id: '77'
doi: 10.1145/1889997.1890001
issue: '1'
page: 4:1--4:43
publication: '{ACM} Trans. Program. Lang. Syst.'
status: public
title: Mechanically verified proof obligations for linearizability
type: journal_article
user_id: '29719'
year: '2011'
...