Publications

  • Herber Paula, Adelt Julius, Liebrenz Timm. . ‘Formal Verification of Intelligent Cyber-Physical Systems with the Interactive Theorem Prover KeYmaera X.’ In Proceedings of the Software Engineering 2021 Satellite Events, Braunschweig/Virtual, Germany, February 22 - 26, 2021, edited by Götz S, Linsbauer L, Schaefer I, Wortmann A, 1-4.: CEUR-WS.org.

  • Dilian Gurov, Paula Herber, Ina Schäfer. . ‘Automated Verification of Embedded Control Software - Track Introduction.’ In 9th International Symposium On Leveraging Applications of Formal Methods, Verification and Validation (ISoLA 2020).: Springer.
  • Herber Paula, Liebrenz Timm. . ‘Dependence Analysis and Automated Partitioning for Scalable Formal Analysis of SystemC Designs.’ In ACM/IEEE International Conference on Formal Methods and Models for System Design, (MEMOCODE 2020), 1-6.: IEEE. doi: 10.1109/MEMOCODE51338.2020.9314998.
  • Simon Schwan, Paula Herber. . ‘Optimized Hardware/Software Co-Verification using the UCLID Satisfiability Modulo Theory Solver.’ Contributed to the IEEE International Conference on Enabling Technologies: Infrastructure for Collaborative Enterprises (WETICE 2020), Virtual Conference.
  • Stefan Sydow, Mohannad Nabelsee, Sabine Glesner, Paula Herber. . ‘Towards Profile-Guided Optimisation for Safe and Efficient Parallel Stream Processing in Rust.’ Contributed to the Workshop on Applications for Multi-Core Architectures (WAMCA) at IEEE International Symposium on Computer Architecture and High Performance Computing (SBAC-PAD), Virtual Conference.
  • Timm Liebrenz, Paula Herber, Sabine Glesner. . ‘Towards Automated Service-oriented Verification of Embedded Control Software modeled in Simulink.’ In International Symposium On Leveraging Applications of Formal Methods, Verification and Validation (ISoLA 2020).: Springer.
  • Treus J, Herber P. . ‘Early Analysis of Security Threats by Modeling and Simulating Power Attacks in SystemC.’ In 91st IEEE Vehicular Technology Conference (VTC Spring 2020), Antwerp, Belgium, May 25-28, 2020, 1-5.: IEEE. doi: 10.1109/VTC2020-Spring48590.2020.9129426.
  • Ulrike Witteck, Denis Grie{ß}bach, Paula Herber. . ‘Equivalence Class Definition for Automated Testing of Satellite On-Board Image Processing.’ In Software Technologies, edited by Sinderen M, Maciaszek LA, 3-25.: Springer. doi: 10.1007/978-3-030-52991-8\_1.
  • Witteck U, Grie{ß}bach D, Herber P. . ‘A Genetic Algorithm for Automated Test Generation for Satellite On-board Image Processing Applications.’ In Proceedings of the 15th International Conference on Software Technologies (ICSOFT), Lieusaint, Paris, France, July 7-9, 2020, edited by Sinderen M, Fill H, Maciaszek LA, 128-135.: ScitePress. doi: 10.5220/0009821101280135.

  • Marcus Mikulcak, Paula Herber, Thomas Göthel, Sabine Glesner. . ‘Information Flow Analysis of Combined Simulink/Stateflow Models.’ Information Technology And Control 48, No. 2: 299-315. doi: 10.5755/j01.itc.48.2.21759.
  • Moesus Nikolai, Scholze Matthias, Schlesinger Sebastian, Herber, Paula. . ‘A Rating Tool for the Automated Selection of Software Refactorings that Remove Antipatterns to Improve Performance and Stability.’ In Software Technologies, edited by van Sinderen, Marten, Maciaszek, Leszek A., 28-54.
  • Timm Liebrenz, Paula Herber and Sabine Glesner. . ‘A Service-oriented Approach for Decomposing and Verifying Hybrid System Models.’ Contributed to the International Conference on Formal Aspects of Component Software, Amsterdam, Niederlande. doi: 10.1007/978-3-030-40914-2\_7.
  • Ulrike Witteck, Denis Griessbach, Paula Herber. . ‘Test Input Partitioning for Automated Testing of Satellite On-board Image Processing Algorithms.’ Contributed to the International Conference on Software Technologies (ICSOFT 2019), Prague, Czech Republic.

  • Feldner B, Herber P. . ‘A Qualitative Evaluation of IPv6 for the Industrial Internet of Things.’ International Workshop on the Future of the Internet of Things (FIT 2018) 138. doi: 10.1016/j.procs.2018.07.195.
  • Liebrenz T, Herber P, Glesner S. . ‘Deductive Verification of Hybrid Control Systems modeled in Simulink with KeYmaera X.’ In International Conference on Formal Engineering Methods (ICFEM 2018, to appear).: Springer. doi: 10.1007/978-3-030-02450-5_6.
  • Mikulcak M, Herber P, Göthel T, Glesner S. . ‘Information Flow Analysis of Combined Simulink/Stateflow Models.’ In VSC Track on Validation of Safety critical Collaboration systems at the IEEE International Conference on Enabling Technologies: Infrastructure for Collaborative Enterprises (WETICE 2018), 223-228.: IEEE Computer Society. doi: 10.1109/WETICE.2018.00050.
  • Moesus N, Scholze M, Schlesinger S, Herber P. . ‘Automated Selection of Software Refactorings that Improve Performance.’ In 13th International Conference on Software Technologies (ICSOFT'18), 67-78.: SCITEPRESS.
  • Pfeffer T, Herber P, Druschke L, Glesner S. . ‘Efficient and Safe Control Flow Recovery Using a Restricted Intermediate Language.’ In Proceedings - 2018 IEEE 27th International Conference on Enabling Technologies: Infrastructure for Collaborative Enterprises (WETICE 2018), Paris, France, 27-29 June 2018, 235-240.: IEEE Computer Society. doi: 10.1109/WETICE.2018.00052.
  • Schlesinger S, Herber P, Göthel T, Glesner S. . ‘Equivalence Checking for Hybrid Control Systems Modelled in Simulink.’ In 2018 IEEE International Conference on Software Quality, Reliability and Security Companion (QRS-C), 572-579.: IEEE. doi: 10.1109/QRS-C.2018.00101.
  • Sydow S, Nabelsee M, Parzyjegla H, Herber P. . ‘A Safe and User-Friendly Graphical Programming Model for Parallel Stream Processing.’ In Parallel, Distributed and Network-based Processing (PDP), 2018 26th Euromicro International Conference on, 239-243.: Conference Publishing Services (CPS). doi: 10.1109/PDP2018.2018.00040.

  • Fellmuth J, Herber P, Pfeffer TF, Glesner S. . ‘Securing Real-Time Cyber-Physical Systems Using WCET-Aware Artificial Diversity.’ In Dependable, Autonomic and Secure Computing, 15th Intl Conf on Pervasive Intelligence & Computing, 3rd Intl Conf on Big Data Intelligence and Computing and Cyber Science and Technology Congress (DASC/PiCom/DataCom/CyberSciTech), 2017 IEEE 15th Intl, 454-461.: IEEE. doi: 10.1109/DASC-PICom-DataCom-CyberSciTec.2017.88.
  • Jaß L, Herber P. . ‘Bit-Precise Formal Verification for SystemC Using Satisfiability Modulo Theories Solving.’ In System Level Design from HW/SW to Memory for Embedded Systems, 51-63.: Springer.
  • Liebrenz T, Herber P, Göthel T, Glesner S. . ‘Towards Service-Oriented Design of Hybrid Systems Modeled in Simulink.’ In Computer Software and Applications Conference (COMPSAC), 2017 IEEE 41st Annual, 469-474.: IEEE. doi: 10.1109/COMPSAC.2017.251.
  • Liebrenz T, Klös V, Herber P. . ‘Automatic Analysis and Abstraction for Model Checking HW/SW Co-Designs modeled in SystemC.’ ACM SIGAda Ada Letters 36, No. 2: 9-17. doi: 10.1145/3092893.3092895.
  • Mikulcak M, Herber P, Göthel T, Glesner S. . ‘Timed Path Conditions in MATLAB/Simulink.’ In System Level Design from HW/SW to Memory for Embedded Systems. Springer., 64-76.: Springer.

  • Herber P, Klös V. . ‘A Multi-Robot Search Using LEGO Mindstorms -- An Embedded Software Design Project.’ ACM SIGBED Review, Special Issue on Embedded and Cyber-Physical Systems Education 14, No. 1.
  • Mikulcak M, Göthel T, Herber P, Glesner S. . ‘Towards Identifying Spurious Paths in Combined Simulink/Stateflow Models.’ Contributed to the Informatik 2016, Klagenfurt, Austria.
  • Pfeffer TF, Sydow S, Fellmuth J, Herber P. . ‘Protecting Legacy Code against Control Hijacking via Execution Location Equivalence Checking.’ In Software Quality, Reliability and Security (QRS), 2016 IEEE International Conference on, 230-241. doi: 10.1109/QRS.2016.35.
  • Schlesinger S, Herber P, Göthel T, Glesner S. . ‘Proving Transformation Correctness of Refactorings for Discrete and Continuous Simulink Models.’ In ICONS 2016, The Eleventh International Conference on Systems, EMBEDDED 2016, International Symposium on Advances in Embedded Systems and Applications., 45-50.
  • Schlesinger S, Herber P, Göthel T, Glesner S. . ‘Proving Correctness of Refactorings for Hybrid Simulink Models with Control Flow.’ In International Workshop on Design, Modeling, and Evaluation of Cyber Physical Systems, 71-86.: IARIA.

  • Herber P, Glesner S. . ‘Verification of Embedded Real-time Systems.’ In Formal Modeling and Verification of Cyber-Physical Systems, edited by Drechsler R., Kühne U., 1-25. Springer Vieweg, Wiesbaden. doi: 10.1007/978-3-658-09994-7_1.
  • Herber P, Pockrandt M, Glesner S. . ‘STATE--A SystemC to Timed Automata Transformation Engine.’ In High Performance Computing and Communications (HPCC), 2015 IEEE 7th International Symposium on Cyberspace Safety and Security (CSS), 2015 IEEE 12th International Conferen on Embedded Software and Systems (ICESS), 2015 IEEE 17th International Conference on, 1074-1077. doi: 10.1109/HPCC-CSS-ICESS.2015.188.
  • Schlesinger S, Herber P, Göthel T, Glesner S. . ‘Towards the verification of refactorings of hybrid Simulink models.’ In Proceedings of 3rd International Workshop on Verification and Program Transformation, EPTCS, 69.

  • Herber P. . ‘The RESCUE Approach-Towards Compositional Hardware/Software Co-verification.’ In High Performance Computing and Communications, 2014 IEEE 6th Intl Symp on Cyberspace Safety and Security, 2014 IEEE 11th Intl Conf on Embedded Software and Syst (HPCC, CSS, ICESS), 2014 IEEE Intl Conf on, 721-724. doi: 10.1109/HPCC.2014.109.
  • Herber P, Hünnemeyer B. . ‘Formal Verification of SystemC Designs using the BLAST Software Model Checker.’ In ACESMB@ MoDELS, 44-53.
  • Pfeffer TF, Herber P, Schneider J. . ‘Reverse engineering of ARM binaries using formal transformations.’ In Proceedings of the 7th International Conference on Security of Information and Networks, 345. doi: 10.1145/2659651.2659697.

  • Herber P, Glesner S. . ‘A HW/SW co-verification framework for SystemC.’ ACM Transactions on Embedded Computing Systems (TECS) 12, No. 1s: 61. doi: 10.1145/2435227.2435257.
  • Herber P, Reicherdt R, Bittner P. . ‘Bit-precise formal verification of discrete-time MATLAB/Simulink models using SMT solving.’ In Embedded Software (EMSOFT), 2013 Proceedings of the International Conference on, 1-10. doi: 10.1109/EMSOFT.2013.6658586.
  • Pockrandt M, Herber P, Klös V, Glesner S. . ‘Model checking memory-related properties of hardware/software co-designs.’ In International Embedded Systems Symposium, 92-103. doi: 10.1007/978-3-642-38853-8_9.

  • Herber P. . ‘Automated HW/SW Co-Verification of SystemC Designs using Timed Automata.’ it-Information Technology Methoden und innovative Anwendungen der Informatik und Informationstechnik 54, No. 6: 296-300.
  • Pockrandt M, Herber P, Gross H, Glesner S. . ‘Optimized Transformation and Verification of SystemC Methods.’ Electronic Communications of the EASST 53.

  • Herber P. . „Automatisierte HW/SW Co-Verifikation von SystemC Modellen mit Hilfe von Timed Automata.“ it - Information Technology. Ausgezeichnete Informatikdissertationen 54, No. 6: 296-300.
  • Herber P, Pockrandt M, Glesner S. . ‘Transforming SystemC transaction level models into UPPAAL timed automata.’ In Proceedings of the Ninth ACM/IEEE International Conference on Formal Methods and Models for Codesign, 161-170. doi: 10.1109/MEMCOD.2011.5970523.
  • Hänsel J, Rose D, Herber P, Glesner S. . ‘An evolutionary algorithm for the generation of timed test traces for embedded real-time systems.’ In Software Testing, Verification and Validation (ICST), 2011 IEEE Fourth International Conference on, 170-179.
  • Pockrandt M, Herber P, Glesner S. . ‘Model checking a SystemC/TLM design of the AMBA AHB protocol.’ In Embedded Systems for Real-Time Multimedia (ESTIMedia), 2011 9th IEEE Symposium on, 66-75. doi: 10.1109/ESTIMedia.2011.6088527.
  • Pockrandt M, Herber P, Glesner S. . ‘Towards a Formal Semantics of the SystemC-TLM Core Interfaces.’ In GI/GMM/ITG Workshop Testmethoden und Zuverlässigkeit von Schaltungen und Systemen (TUZ).

  • Herber P. . A Framework for Automated HW/SW Co-Verification of SystemC Designs using Timed Automata.: Logos Verlag Berlin GmbH.
  • Herber P, Pockrandt M, Glesner S. . ‘Automated conformance evaluation of SystemC designs using timed automata.’ In Test Symposium (ETS), 2010 15th IEEE European, 188-193. doi: 10.1109/ETSYM.2010.5512761.

  • Herber P, Friedemann F, Glesner S. . ‘Combining model checking and testing in a continuous hw/sw co-verification process.’ In International Conference on Tests and Proofs, 121-136. doi: 10.1007/978-3-642-02949-3_10.

  • Herber P, Fellmuth J, Glesner S. . ‘Model checking SystemC designs using timed automata.’ In Proceedings of the 6th IEEE/ACM/IFIP international conference on Hardware/Software codesign and system synthesis, 131-136. doi: 10.1145/1450135.1450166.