Jana (Philipp) Berger

Email
berger at cs.rwth-aachen.de
Address
Room 4203
Ahornstraße 55
D-52074 Aachen
Phone
+49 241 80 21206

I am a PhD student at the Software Modeling and Verification Group (MOVES) headed by Professor J.-P. Katoen.

I am primarily interested in software model-checking of C code. I worked on a project with Ford Motor Company (feasibility analysis on two case studies based on software component prototypes).

Together with my master student Jan Švejda we participated in SV-COMP 2020 with our Violation Witness Validator NITWIT!

 

2022
DOI [bibtex]
@conference{CBCMC2022,
title = {Configurable Benchmarks for C Model Checkers},
author = {Xaver Fink and Philipp Berger and Joost-Pieter Katoen},
publisher = {Springer},
booktitle = {LNCS},
volume = {13260},
pages = {338-354},
type = {Conference Paper},
year = {2022},
doi = {10.1007/978-3-031-06773-0_18},
url = { https://publications.rwth-aachen.de/record/848928},
}×
[issue] 		Xaver Fink, Philipp Berger, Joost-Pieter Katoen. Configurable Benchmarks for C Model Checkers, NASA Formal Methods Symposium 2022 (NFM), Volume 13260 of LNCS, 338-354, Springer, 2022.
2020
DOI fulltext PDF [bibtex]
@conference{IBVWVCN2020,
title = {Interpretation-Based Violation Witness Validation for C: NITWIT},
author = {Jan Švejda and Philipp Berger and Joost-Pieter Katoen},
publisher = {Springer},
booktitle = {LNCS},
volume = {12078},
pages = {40-57},
type = {Conference Paper},
year = {2020},
doi = {10.1007/978-3-030-45190-5_3},
url = { https://publications.rwth-aachen.de/record/814598},
}×
[issue] 		Jan Švejda, Philipp Berger, Joost-Pieter Katoen. Interpretation-Based Violation Witness Validation for C: NITWIT, 26th International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS 2020), Volume 12078 of LNCS, 40-57, Springer, 2020.
DOI [bibtex]
@conference{BSMCAC2020,
title = {Benchmarking Software Model Checkers on Automotive Code},
author = {Lukas Westhofen and Philipp Berger and Joost-Pieter Katoen},
publisher = {Springer},
booktitle = {LNCS},
volume = {12229},
pages = {133-150},
type = {Conference Paper},
year = {2020},
doi = {10.1007/978-3-030-55754-6_8},
url = { https://publications.rwth-aachen.de/record/814599},
}×
[issue] 		Lukas Westhofen, Philipp Berger, Joost-Pieter Katoen. Benchmarking Software Model Checkers on Automotive Code, 12th NASA Formal Methods Symposium (NFM 2020), Volume 12229 of LNCS, 133-150, Springer, 2020.
2019
DOI [bibtex]
@conference{MAROSTVAMBD2019,
title = {Multiple Analyses, Requirements Once: Simplifying Testing and Verification in Automotive Model-Based Development},
author = {Philipp Berger and Johanna Nellen and Joost-Pieter Katoen and Erika Ábrahám and Md Tawhid Bin Waez and Thomas Rambow},
publisher = {Springer},
booktitle = {LNCS},
volume = {11687},
pages = {59-75},
type = {Conference Paper},
year = {2019},
doi = {10.1007/978-3-030-27008-7_4},
url = { https://publications.rwth-aachen.de/record/767285},
}×
[issue] 		Philipp Berger, Johanna Nellen, Joost-Pieter Katoen, Erika Ábrahám, Md Tawhid Bin Waez, Thomas Rambow. Multiple Analyses, Requirements Once: Simplifying Testing and Verification in Automotive Model-Based Development, 24th International Conference on Formal Methods for Industrial Critical Systems (FMICS 2019), Volume 11687 of LNCS, 59-75, Springer, 2019.
2018
DOI [bibtex]
@conference{VACCSAERAD2018,
title = {Verifying Auto-generated C Code from Simulink: An Experience Report in the Automotive Domain},
author = {Philipp Berger and Joost-Pieter Katoen and Erika Ábrahám and Md Tawhid Bin Waez and Thomas Rambow},
publisher = {Springer},
booktitle = {LNCS},
volume = {10951},
type = {Conference Paper},
year = {2018},
doi = {10.1007/978-3-319-95582-7_18},
url = { https://publications.rwth-aachen.de/record/753075},
}×
[issue] 		Philipp Berger, Joost-Pieter Katoen, Erika Ábrahám, Md Tawhid Bin Waez, Thomas Rambow. Verifying Auto-generated C Code from Simulink: An Experience Report in the Automotive Domain, 22nd International Symposium of Formal Methods (FM 2018), Volume 10951 of LNCS, Springer, 2018.