Every Component Matters: Generating Parallel Verification Benchmarks with Hardness Guarantees
Jasper M, Schlüter M, Schmidt D, Steffen B (2021)
In: Leveraging Applications of Formal Methods, Verification and Validation: Tools and Trends. 9th International Symposium on Leveraging Applications of Formal Methods, ISoLA 2020, Rhodes, Greece, October 20–30, 2020, Proceedings, Part IV. Margaria T, Steffen B (Eds); Lecture Notes in Computer Science. Cham: Springer International Publishing: 242-263.
Sammelwerksbeitrag
| Veröffentlicht | Englisch
Download
Es wurden keine Dateien hochgeladen. Nur Publikationsnachweis!
Autor*in
Jasper, Marc;
Schlüter, Maximilian;
Schmidt, DavidUniBi 
;
Steffen, Bernhard
;
Steffen, BernhardHerausgeber*in
Margaria, Tiziana;
Steffen, Bernhard
Einrichtung
Abstract / Bemerkung
In this paper, we show how to automatically generate hard verification tasks in order to support events like the Model Checking Contest or the Rigorous Examination of Reactive Systems Challenge with tailored benchmark problems for analyzing the validity of linear-time properties in parallel systems. Characteristic of the generated benchmarks are two hardness guarantees: (i) every parallel component is relevant and (ii) the state space of the analyzed system is exponential in the number of its parallel components. Generated benchmarks can be made available, e.g., as Promela code or Petri nets.
Erscheinungsjahr
2021
Buchtitel
Leveraging Applications of Formal Methods, Verification and Validation: Tools and Trends. 9th International Symposium on Leveraging Applications of Formal Methods, ISoLA 2020, Rhodes, Greece, October 20–30, 2020, Proceedings, Part IV
Serientitel
Lecture Notes in Computer Science
Seite(n)
242-263
Konferenz
9th International Symposium on Leveraging Applications of Formal Methods, ISoLA 2020
Konferenzort
Rhodes, Greece
Konferenzdatum
2020-10-20 – 2020-10-30
ISBN
978-3-030-83722-8
eISBN
978-3-030-83723-5
ISSN
0302-9743
eISSN
1611-3349
Page URI
https://pub.uni-bielefeld.de/record/2989314
Zitieren
Jasper M, Schlüter M, Schmidt D, Steffen B. Every Component Matters: Generating Parallel Verification Benchmarks with Hardness Guarantees. In: Margaria T, Steffen B, eds. Leveraging Applications of Formal Methods, Verification and Validation: Tools and Trends. 9th International Symposium on Leveraging Applications of Formal Methods, ISoLA 2020, Rhodes, Greece, October 20–30, 2020, Proceedings, Part IV. Lecture Notes in Computer Science. Cham: Springer International Publishing; 2021: 242-263.
Jasper, M., Schlüter, M., Schmidt, D., & Steffen, B. (2021). Every Component Matters: Generating Parallel Verification Benchmarks with Hardness Guarantees. In T. Margaria & B. Steffen (Eds.), Lecture Notes in Computer Science. Leveraging Applications of Formal Methods, Verification and Validation: Tools and Trends. 9th International Symposium on Leveraging Applications of Formal Methods, ISoLA 2020, Rhodes, Greece, October 20–30, 2020, Proceedings, Part IV (pp. 242-263). Cham: Springer International Publishing. https://doi.org/10.1007/978-3-030-83723-5_16
Jasper, Marc, Schlüter, Maximilian, Schmidt, David, and Steffen, Bernhard. 2021. “Every Component Matters: Generating Parallel Verification Benchmarks with Hardness Guarantees”. In Leveraging Applications of Formal Methods, Verification and Validation: Tools and Trends. 9th International Symposium on Leveraging Applications of Formal Methods, ISoLA 2020, Rhodes, Greece, October 20–30, 2020, Proceedings, Part IV, ed. Tiziana Margaria and Bernhard Steffen, 242-263. Lecture Notes in Computer Science. Cham: Springer International Publishing.
Jasper, M., Schlüter, M., Schmidt, D., and Steffen, B. (2021). “Every Component Matters: Generating Parallel Verification Benchmarks with Hardness Guarantees” in Leveraging Applications of Formal Methods, Verification and Validation: Tools and Trends. 9th International Symposium on Leveraging Applications of Formal Methods, ISoLA 2020, Rhodes, Greece, October 20–30, 2020, Proceedings, Part IV, Margaria, T., and Steffen, B. eds. Lecture Notes in Computer Science (Cham: Springer International Publishing), 242-263.
Jasper, M., et al., 2021. Every Component Matters: Generating Parallel Verification Benchmarks with Hardness Guarantees. In T. Margaria & B. Steffen, eds. Leveraging Applications of Formal Methods, Verification and Validation: Tools and Trends. 9th International Symposium on Leveraging Applications of Formal Methods, ISoLA 2020, Rhodes, Greece, October 20–30, 2020, Proceedings, Part IV. Lecture Notes in Computer Science. Cham: Springer International Publishing, pp. 242-263.
M. Jasper, et al., “Every Component Matters: Generating Parallel Verification Benchmarks with Hardness Guarantees”, Leveraging Applications of Formal Methods, Verification and Validation: Tools and Trends. 9th International Symposium on Leveraging Applications of Formal Methods, ISoLA 2020, Rhodes, Greece, October 20–30, 2020, Proceedings, Part IV, T. Margaria and B. Steffen, eds., Lecture Notes in Computer Science, Cham: Springer International Publishing, 2021, pp.242-263.
Jasper, M., Schlüter, M., Schmidt, D., Steffen, B.: Every Component Matters: Generating Parallel Verification Benchmarks with Hardness Guarantees. In: Margaria, T. and Steffen, B. (eds.) Leveraging Applications of Formal Methods, Verification and Validation: Tools and Trends. 9th International Symposium on Leveraging Applications of Formal Methods, ISoLA 2020, Rhodes, Greece, October 20–30, 2020, Proceedings, Part IV. Lecture Notes in Computer Science. p. 242-263. Springer International Publishing, Cham (2021).
Jasper, Marc, Schlüter, Maximilian, Schmidt, David, and Steffen, Bernhard. “Every Component Matters: Generating Parallel Verification Benchmarks with Hardness Guarantees”. Leveraging Applications of Formal Methods, Verification and Validation: Tools and Trends. 9th International Symposium on Leveraging Applications of Formal Methods, ISoLA 2020, Rhodes, Greece, October 20–30, 2020, Proceedings, Part IV. Ed. Tiziana Margaria and Bernhard Steffen. Cham: Springer International Publishing, 2021. Lecture Notes in Computer Science. 242-263.
Google Scholar
ISBN Suche