Publications

Conference and Journal papers

2022

© 2022 IEEE. Personal use of this material is permitted. However, permission to reprint/republish this material for advertising or promotional purposes or for creating new collective works for resale or redistribution to servers or lists, or to reuse any copyrighted component of this work in other works must be obtained from the IEEE.

  • Mohammad Rahmani Fadiheh, Alex Wezel, Johannes Müller, Jorg Bormann, Sayak Ray, Jason M. Fung, Subhasish Mitra, Dominik Stoffel and Wolfgang Kunz: “An Exhaustive Approach to Detecting Transient Execution Side Channels in RTL Designs of Processors “, in IEEE Transactions on Computers, (early access) doi: 10.1109/TC.2022.3152666.

  • Lucas Deutschmann, Johannes Müller, Mohammad Rahmani Fadiheh, Dominik Stoffel and Wolfgang Kunz: “Towards a Formally Verified Hardware Root-of-Trust for Data-Oblivious Computing “, 59th ACM/IEEE Design Automation Conference (DAC), San Francisco, USA, 2022.

  • Christian Bartsch, Stephan Wilhelm, Daniel Kästner, Dominik Stoffel and Wolfgang Kunz: ”Combining Fault Effect Analysis and Fault Propagation Analysis to Determine Source-Level Effects of Hardware Faults”, Embedded World, 2022.

  • Stian Sorensen, Christian Bartsch, Dominik Stoffel and Wolfgang Kunz: “Generation of Formal CPU Profiles for Embedded Systems“, 30th IFIP/IEEE International Conference on Very Large Scale Integration (VLSI-SoC), Patras, Greece, 2022.

  • Wolfgang Kunz: “Spectres, Meltdowns, Zombies, Orcs: Can formal methods banish the ghosts that haunt your hardware?”, SeHAS Workshop at HiPEAC, Budapest, Hungary, 2022. (keynote)

  • Endri Kaja, Nicolas Gerlin, Monideep Bora, Keerthikumara Devarajegowda, Dominik Stoffel, Wolfgang Kunz and Wolfgang Ecker: “MetaFS: Model-driven Fault Simulation Framework“, IEEE International Symposium on Defect and Fault Tolerance in VLSI and Nanotechnology Systems (DFTS), Austin, TX, 2022.

  • Nicolas Gerlin, Endri Kaja, Monideep Bora, Keerthikumara Devarajegowda, Dominik Stoffel, Wolfgang Kunz and Wolfgang Ecker: “Design of a Tightly-Coupled RISC-V Physical Memory Protection Unit for Online Error Detection“, 30th IFIP/IEEE International Conference on Very Large Scale Integration (VLSI-SoC), Patras, Greece, 2022.

  • Endri Kaja, Nicolas Gerlin, Monideep Bora, Gabriel Rutsch, Keerthikumara Devarajegowda, Dominik Stoffel, Wolfgang Kunz and Wolfgang Ecker: “Fast and accurate Model-Driven FPGA-based System-Level Fault Emulation“, 30th IFIP/IEEE International Conference on Very Large Scale Integration (VLSI-SoC), Patras, Greece, 2022.

  • Wolfgang Ecker, Peer Adelt, Wolfgang Müller, Reinhold Heckmann, Milos Krstic, Vladimir Herdt, Rolf Drechsler, Gerhard Angst, Ralf Wimmer, Andreas Mauderer, Rafael Stahl, Karsten Emrich, Daniel Mueller-Gritschneder, Bernd Becker, Philipp Scholl, Eyck Jentzsch, Jan Schlamelcher, Kim Grüttner, Paul Palomero Bernardo, Oliver Bringmann, Mihaela Damian, Julian Oppermann, Andreas Koch, Jörg Bormann, Johannes Partzsch, Christian Mayr, Wolfgang Kunz: “The Scale4Edge RISC-V Ecosystem“, Design and Test in Europe (DATE), 2022.

     

2021

© 2021 IEEE. Personal use of this material is permitted. However, permission to reprint/republish this material for advertising or promotional purposes or for creating new collective works for resale or redistribution to servers or lists, or to reuse any copyrighted component of this work in other works must be obtained from the IEEE.

  • J. Müller; Mo Fadiheh; A. Duque Anton; T. Eisenbarth; D. Stoffel and W. Kunz: “A Formal Approach to Confidentiality Verification in SoCs at the Register Transfer Level“, 58th IEEE/ACM Design Automation Conf. (DAC), Dec. 2021.
     
  • Christian Bartsch, Stephan Wilhelm, Daniel Kästner, Dominik Stoffel and Wolfgang Kunz: ”Compositional Fault Propagation Analysis in Embedded Systems Using Abstract Interpretation”, IEEE International Test Conference (ITC), October 2021.
     
  • T. Ludwig, M. Schwarz, P. Morkunas, S. Santana, D. Stoffel, W. Kunz : „Democratizing Formal Verification“, Design and Verification Conference Europe (DVCON EU), 2021.
     
  • K Devarajegowda, E. Kaja, S. Prebeck, W. Ecker: ISA modeling with trace notation for context free property generation. 58th Annual Design Automation Conference, (DAC'21), 2021.
     
  • Ilia Polian, Frank Altmann, Tolga Arul, Christian Boit, Ralf Brederlow, Lucas Davi, Rolf Drechsler, Nan Du, Thomas Eisenbarth, Tim Güneysu, Sascha Hermann, Matthias Hiller, Rainer Leupers, Farhad Merchant, Thomas Mussenbrock, Stefan Katzenbeisser, Akash Kumar, Wolfgang Kunz, Thomas Mikolajick, Vivek Pachauri, Jean-Pierre Seifert, Frank Sill Torres, Jens Trommer: „Nano Security: From Nano-Electronics to Secure Systems“ Design, Automation Test in Europe Conference Exhibition (DATE), 2021.
     
  • Lucas Deutschmann, Johannes Schauß, Tobias Ludwig, Dominik Stoffel, Wolfgang Kunz: „Operation Level Synthesis“, Methoden und Beschreibungssprachen zur Modellierung und Verifikation von Schaltungen und Systemen (MBMV), 2021.
     
  • Karthik Ganesan, Florian Lonsing, Srinivasa Shashank Nuthakki, Eshan Singh, Mohammad Rahmani Fadiheh, Wolfgang Kunz, Dominik Stoffel, Clark W. Barrett, Subhasish Mitra: „Effective Pre-Silicon Verification of Processor Cores by Breaking the Bounds of Symbolic Quick Error Detection“, CoRR abs/2106.10392, 2021.
     
  • Mohammad Rahmani Fadiheh, Alex Wezel, Johannes Müller, Jörg Bormann, Sayak Ray, Jason M. Fung, Subhasish Mitra, Dominik Stoffel, Wolfgang Kunz: „An Exhaustive Approach to Detecting Transient Execution Side Channels in RTL Designs of Processors“. CoRR abs/2108.01979, 2021.

2020

© 2020 IEEE. Personal use of this material is permitted. However, permission to reprint/republish this material for advertising or promotional purposes or for creating new collective works for resale or redistribution to servers or lists, or to reuse any copyrighted component of this work in other works must be obtained from the IEEE.

  • M.R. Fadiheh, J. Müller, R. Brinkmann, S. Mitra, D. Stoffel, W. Kunz: A formal approach for detecting vulnerabilities to transient execution attacks in out-of-order processors. 57th Annual Design Automation Conference, (DAC'20), 2020
     
  • M.R. Fadiheh, J. Müller, A. Duque-Anton, S. Mitra, J. Fung, D. Stoffel, W. Kunz: A Systematic Approach to Detecting Microarchitectural Security Vulnerabilities by RTL Hardware Verification, Intel Side-Channel Academic Program (SCAP) Workshop 2020, (recording)
     
  • M.R. Fadiheh, J. Müller, A. Duque-Anton, S. Mitra, D. Stoffel, W. Kunz: A Formal Approach for Detecting Vulnerabilities to Transient Execution Attacks in Out-of-order Processors, Intel Side-Channel Academic Program Workshop (SCAP) 2020, (recording)
     
  • K. Devarajegowda, M.R. Fadiheh, E. Singh, C. Barrett, S. Mitra, W. Ecker, D. Stoffel, W. Kunz: "Gap-free Processor Verification by S²QED and Property Generation", Design, Automation Test in Europe Conference Exhibition (DATE), Grenoble, March 2020
     
  • K. Devarajegowda, V. Hiltl, T. Rabenalt, D. Stoffel, W. Kunz, W. Ecker: "Formal Verification by the Book: Error Detection and Correction Codes", Design and Verification Conference US (DVCON US), San Jose, CA, March. 2020.
     
  • K. Devarajegowda, M.R. Fadiheh:"C-S²QED: Gap-Free Formal Verification of Processor Cores",Design and Verification Conference Europe (DVCON EU), Virtual Conference, October. 2020.
     
  • M. A. Ben Khadra, D. Stoffel, and W. Kunz, “Efficient Binary-Level Coverage Analysis,” in ACM Joint European Software Engineering Conference and Symposium on the Foundations of Software Engineering - ESEC/FSE’20, Virtual Event, USA, November 2020. (recording)

2019

© 2019 IEEE. Personal use of this material is permitted. However, permission to reprint/republish this material for advertising or promotional purposes or for creating new collective works for resale or redistribution to servers or lists, or to reuse any copyrighted component of this work in other works must be obtained from the IEEE.

  • T. Ludwig, J. Urdahl, D. Stoffel, W. Kunz: Properties First – Correct-By-Construction RTL Design in System-Level Design Flows, IEEE Transactions on Computer-Aided Design of Circuits and Systems (TCAD), accepted for publication, 2019.
     
  • S. Udupi, J. Urdahl, D. Stoffel, W. Kunz: Exploiting Hardware Unobservability for Low-Power Design and Safety Analysis, IEEE Transactions on Very Large Scale Integration (TVLSI), Vol. 27, no. 6, pp. 1262 – 1275, June 2019.
     
  • T. Ludwig, M. Schwarz, J. Urdahl, L. Deutschmann, S. Hetalani, D. Stoffel, W. Kunz: Property-Driven Development of a RISC-V CPU, Design and Verification Conference US (DVCON US), San Jose, CA, Feb. 2019.
     
  • M.R. Fadiheh, D. Stoffel, S. Mitra, C. Barrett, W. Kunz: ”Processor hardware security vulnerabilities and their detection by unique program execution checking”. Design, Automation Test in Europe Conference Exhibition (DATE), Florence, March 2019.
     
  • E. Singh, K. Devarajegowda, S. Simon, R. Schnieder, K. Ganesan, M. Fadiheh, D. Stoffel, W. Kunz, C. Barrett, W. Ecker, S. Mitra: „Symbolic QED Pre-silicon Verification for Automotive Microcontroller Cores: Industrial Case Study” Design, Automation Test in Europe Conference Exhibition (DATE), Florence, March  2019.
     
  • M. Schwarz, D. Stoffel, W. Kunz: ACCESS: HW/SW-Co-Equivalence Checking for Firmware Optimization, Methoden und Beschreibungssprachen zur Modellierung und Verifikation von Schaltungen und Systemen" (MBMV), 2019, (WiP Paper)
     
  • M. Schwarz, R. Stahl, D. Müller-Gritschneder, U. Schlichtmann, D. Stoffel, W. Kunz: ACCESS: HW/SW Co-Equivalence Checking for Firmware Optimization, 56th Annual Design Automation Conference, (DAC'19), Las Vegas, NV, USA, 2019.

2018

© 2018 IEEE. Personal use of this material is permitted. However, permission to reprint/republish this material for advertising or promotional purposes or for creating new collective works for resale or redistribution to servers or lists, or to reuse any copyrighted component of this work in other works must be obtained from the IEEE.

  • C. Villarraga, D. Stoffel, W. Kunz. Software in a Hardware View. In: Drechsler R. (eds) Formal System Verification. Pages 123-154. ISBN 978-3-319-57685-5 Springer, Cham. 2018
     
  • T. Fehmel, D. Stoffel, W. Kunz: “Generation of Abstract Driver Models for IP Integration Verification”, IEEE Transactions on Emerging Topics in Computing, 2018.
     
  • M.R. Fadiheh, S.S. Nuthakki, S. Mitra, C. Barrett, D. Stoffel, W. Kunz: ”Symbolic quick error detection using symbolic initial state for pre-silicon verification.” In Design, Automation Test in Europe Conference Exhibition (DATE), 2018 (pp. 55-60).
     
  • M. Schwarz, D. Stoffel, W. Kunz:  “HW/SW Co-Equivalence Checking for Firmware Optimization” Proceedings of Embedded Software for Industrial IoTs (ESIIT), March 2018.
     
  • M. Schwarz, D. Stoffel, W. Kunz:  “HW/SW Co-Equivalence Checking for Firmware Optimization; Forum on specification & Design Language (FDL), September 2018, (Invited Talk).
     
  • T. Ludwig: Properties-First Design: “A New Design Methodology for SoC Hardware and Low-Level Software” Design and Verification Conference Europe (DVVCON Europe), 2018 (Invited Tutorial)
     

2017

© 2017 IEEE. Personal use of this material is permitted. However, permission to reprint/republish this material for advertising or promotional purposes or for creating new collective works for resale or redistribution to servers or lists, or to reuse any copyrighted component of this work in other works must be obtained from the IEEE.

  • M. A. Ben Khadra: E3Solver: Decision tree unification by enumeration, in 6th Workshop on Synthesis (SYNT'17), 2017. [pdf] (Competition Contribution)
     
  • M. A. Ben Khadra, D. Stoffel, W. Kunz: goSAT: Floating-point Satisfiability as Global Optimization, in Formal Methods in Computer-Aided Design (FMCAD'17), 2017. [pdf] (Accepted)
     
  • M. A. Ben Khadra, D. Stoffel, W. Kunz: Speculative Disassembly of Binary Code, in 20. Workshop Methoden und Beschreibungssprachen zur Modellierung und Verifikation von Schaltungen und Systemen (MBMV’17), 2017. (Abstract)
     
  • C. Bartsch, C. Villarraga, D. Stoffel, and W. Kunz, “A HW/SW Cross-Layer Approach for Determining Application-Redundant Hardware Faults in Embedded Systems,” Journal of Electronic Testing (JETTA), vol. 33, no. 1, pp. 77 – 92, Feb 2017. [link]
     
  • W. Kunz: “A HW/SW Cross-Layer Approach for Determining Application-Critical HW Faults in Embedded Systems”, IEEE VLSI Test Symposium (VTS’17),, Las Vegas, April 2017 (invited).
     
  • W. Kunz: “Safety across the HW/SW interface – can Formal Methods meet the challenge?” 26th International Workshop on Logic & Synthesis (IWLS’17), Austin, TX, June 2017 (invited).
     
  • W. Kunz: Rethinking Design in the IoT Era - How Formal Methods Help to Meet theChallenges, 12th VDEC D2T Symposium, Tokyo, September 2017 (invited)
     
  • D. Stoffel: Software in a Hardware View: New Models for Firmware Development and Safety Analysis in IoT Systems, 12th VDEC D2T Symposium, Tokyo, September 2017 (invited)
     
  • S. Udupi, J. Urdahl, D. Stoffel and W. Kunz, "Dynamic Power Optimization Based on Formal Property Checking of Operations," 30th International Conference on VLSI Design and 16th International Conference on Embedded Systems (VLSID), Hyderabad, 2017. [link]
     
  • M. Schwarz, C. Villarraga, D. Stoffel, W. Kunz: "Cycle-Accurate Software Modeling for RTL Verification of Embedded Systems", IEEE Design and Diagnostics of Electronic Circuits and Systems (DDECS), Dresden, 2017.
     
  • S. Udupi, J. Urdahl, D. Stoffel, W. Kunz. "Dynamic Power Optimization based on Formal Property Checking of Operations" 20. Workshop Methoden und Beschreibungssprachen zur Modellierung und Verifikation von Schaltungen und Systemen MBMV), 2017, Bremen, Germany.
     
  • Villarraga C., Stoffel D., Kunz W. Software in a Hardware View. In: Drechsler R. (eds) Formal System Verification. Pages 123-154. ISBN 978-3-319-57685-5 Springer, Cham. 2018

 

2016 

© 2016 IEEE. Personal use of this material is permitted. However, permission to reprint/republish this material for advertising or promotional purposes or for creating new collective works for resale or redistribution to servers or lists, or to reuse any copyrighted component of this work in other works must be obtained from the IEEE.

  • C. Bartsch, C. Villarraga, D. Stoffel, W. Kunz: A HW-dependent Software Model for Cross-Layer Fault Analysis in Embedded Systems, IEEE Latin-American Test Symposium (LATS-2016), Brazil, 2016.
     
  • M. A. Ben Khadra, D. Stoffel, W. Kunz: Speculative Disassembly of Binary Code, International Conference on Compilers, Architectures and Synthesis for Embedded Systems (CASES), Embedded Systems Week 2016, Pittsburgh, USA, 2016.
     
  • M. A. Ben Khadra, D. Stoffel, W. Kunz: Approximate Computing: Facing the Control Flow, Embedded Systems Week Workshop on Approximate Computing, Poster, Pittsburgh, USA, 2016
     
  • C. Bartsch, C. Villarraga, D. Stoffel, W. Kunz: A HW-dependent Software Model for Cross-Layer Fault Analysis in Embedded Systems, 9. Workshop Methoden und Beschreibungssprachen zur Modellierung und Verifikation von Schaltungen und Systemen (MBMV), Freiburg, 2016.
     
  • S. Udupi, J. Urdahl, D. Stoffel, W. Kunz: Dynamic Power Optimization based on Formal Property Checking of Operations, IEEE/ACM Design Automation Conference (DAC-2016), WIP Session, Austin, USA, 2016
     
  • J. Urdahl, S. Udupi, T. Ludwig, D. Stoffel, W. Kunz: Properties First? A New Design Methodology for Hardware, and its Perspectives in Safety Analysis, IEEE/ACM International Conference on Computer Aided Design (ICCAD), Austin, USA, 2016.
     
  • S. Udupi, J. Urdahl, D. Stoffel, W. Kunz: Dynamic Power Optimization based on Formal Property Checking of Operations, VLSI Design 2017, Hyderabad, India, 2017.
     
  • M. Zwolinski, W. Kunz, K. Svarstad, A. Brown: The European Masters in Embedded Computing Systems (EMECS), European Workshop on Microelectronics Education (EWME), Southampton, UK, 2016.
     
  • C. Bartsch, C Villarraga, D. Stoffel, W. Kunz: Safety Across the HW/SW Interface – Can Formal Methods Meet the Challenge? International Symposium on Integrated Circuits (ISIC-2016), Singapore, 2016.
     
  • W. Kunz: Prototype or Golden Model – what if Formal Methods took the lead in ESL-based design flows?, IEEE International Conference on Communications and Electronics (ICCE 2016), Halong Bay, Vietnam, 2016. (invited)
     
  • O. Marx, C. Villarraga, D. Stoffel, W. Kunz: A Computer-Algebraic Approach to Formal Verification of Data-Centric Low-Level Software, ACM-IEEE International Conference on Formal Methods and Models for System Design, 2016
     
  • Villarraga C., Stoffel D., Kunz W. Software in a Hardware View: New Models for HW-dependent Software in SoC Verification. In: Formal System Verification (Edited by R. Drechsler), Springer to appear.

     

2015 

© 2015 IEEE. Personal use of this material is permitted. However, permission to reprint/republish this material for advertising or promotional purposes or for creating new collective works for resale or redistribution to servers or lists, or to reuse any copyrighted component of this work in other works must be obtained from the IEEE.

  • W. Kunz: „Korrekte Chips mit formalen Methoden: 
    Beweis erbracht  –  aber wo bleibt der Durchbruch am Markt?“ anlässlich des 80. Geburtstages von Prof. Kurt Antreich, TU München, 26.02.2015

  • J. Urdahl, D. Stoffel, W. Kunz: "Architectural System Modeling for Correct-by-Construction RTL Design", Proc. Methoden und Beschreibungssprachen zur Modellierung und Verifikation von Schaltungen und Systemen (MBMV), Chemnitz, Germany, March 2015.

  • W. Kunz: „Hardware/Firmware Verification in System-Level Design  Flows –  Can Formal Methods Meet the Challenge?” IEEE European Conference on Circuit Theory and Design (ECCTD), August 2015

  • J. Urdahl, D. Stoffel, W. Kunz: "Architectural System Modeling for Correct-by-Construction RTL Design", Proc. Forum on Specification and Design Languages (FDL), Barcelona, Spain, September 2015. 

  • M. Schwarz, M. Chaari, B. Tabacaru, W. Ecker: "A Meta-Model-Based Approach for Semantic Fault Modeling on Multiple Abstraction Levels", Proc. Design and Verification Conference & Exhibition Europe 2015 (DVCon), Munich, Germany, November 2015.

  • C. Bartsch, N. Roedel, C. Villarraga, D. Stoffel, and W. Kunz, “A hw-dependent software model for cross-layer fault analysis in embedded systems,” in International Workshop on Resiliency in Embedded Electronic Systems, November  2015.
           
  • B. Bao, C. Villarraga, B. Schmidt, D. Stoffel, W. Kunz: "A New Property Language for the Specification of Hardware-Dependent Embedded System Software" in F. Oppenheimer (Ed.), Languages, Design Methods, and Tools for Electronic Systems Design, Springer (to appear).


2014 

© 2014 IEEE. Personal use of this material is permitted. However, permission to reprint/republish this material for advertising or promotional purposes or for creating new collective works for resale or redistribution to servers or lists, or to reuse any copyrighted component of this work in other works must be obtained from the IEEE.

  • C. Villarraga, B. Schmidt, B. Bao, R. Raman, C. Bartsch, T. Fehmel, D. Stoffel, W. Kunz. "Software in a Hardware View: New Models for HW-dependent Software in SoC Verification and Test" (Invited Paper) Proc. International Test Conference (ITC'14), 2014. Seattle, USA.

  • B. Bao, C. Villarraga, B. Schmidt, D. Stoffel, W. Kunz. "A New Property Language for the Specification of Hardware-Dependent Embedded System Software". Proc. Forum on Specification And Design Languages (FDL), 2014. Munich, Germany.

  • C. Bartsch, C. Villarraga, B. Schmidt, D. Stoffel, W. Kunz. "Efficient SAT/Simulation-based model generation for low-level embedded software" 17. GI/ITG/GMM Workshop Methoden und Beschreibungssprachen zur Modellierung und Verifikation von Schaltungen und Systemen MBMV), 2014, 147-157. Boeblingen, Germany.

  • J. Urdahl, D. Stoffel, W. Kunz: "Path Predicate Abstraction for Sound System-Level Models of RT-Level Circuit Designs", IEEE Transactions on Computer-Aided Design of Integrated Circuits and Systems, Vol. 33, No. 2, Feb. 2014, pp. 291-304

  • B. Bao, J. Bormann, M. Wedler, D. Stoffel, W. Kunz: "Formal Plausibility Checks for Environment Constraints" in J. Haase (Ed.), Models, Methods, and Tools for Complex Chip Design, Springer, 2014, ISBN 978-3-319-01417-3.

  • W. Kunz, D. Stoffel, J. Urdahl: Formal Verification in System-on-Chip Design: Scientific Foundations and Practical Methodology, IEEE System-on-Chip Conference, Las Vegas, 2014.

  • W. Kunz: “The big hurdles for FV tools in industrial practice – can we overcome them insystem-level design flows? International Workshop on Design and Implementation of Formal Tools and Systems (DIFTS), co-located with FMCAD and MEMOCODE, Lausanne, Switzerland October 20, 2014.

  • B. Bao, J. Bormann, M. Wedler, D. Stoffel, W. Kunz: "Formal Plausibility Checks for Environment Constraints" in J. Haase (Ed.), Models, Methods, and Tools for Complex Chip Design, Springer, 2014, ISBN 978-3-319-01417-3

2013 

© 2013 IEEE. Personal use of this material is permitted. However, permission to reprint/republish this material for advertising or promotional purposes or for creating new collective works for resale or redistribution to servers or lists, or to reuse any copyrighted component of this work in other works must be obtained from the IEEE.

  • B. Schmidt, C. Villarraga, J. Bormann, D. Stoffel, M. Wedler, W. Kunz: "A Computational Model for SAT-based Verification of Hardware-Dependent Low-Level Embedded System Software", The 18th Asia and South Pacific Design Automation Conference(ASP-DAC), Yokohama, Japan, January 2013 

  • B. Schmidt, C. Villarraga, T. Fehmel, J. Bormann, D. Stoffel, W. Kunz: "A Hardware-Dependent Model for SAT-based Verification of Interrupt-Driven Low-level Embedded System Software" 16. Workshop Methoden und Beschreibungssprachen zur Modellierung und Verifikation von Schaltungen und Systemen (MBMV), Rostock, Germany, March 2013 

  • B. Bao, J. Bormann, M. Wedler, D. Stoffel, W. Kunz: "Compositional Completeness over reactive Constraints" 16. Workshop Methoden und Beschreibungssprachen zur Modellierung und Verifikation von Schaltungen und Systemen (MBMV), Rostock, Germany, March 2013 

  • O. Marx, M. Wedler, A. Dreyer, D. Stoffel, W. Kunz: "Proof Logging for Computer Algebra based SMT Solving" 16. Workshop Methoden und Beschreibungssprachen zur Modellierung und Verifikation von Schaltungen und Systemen (MBMV), Rostock, Germany, March 2013 

  • C. Villarraga, B. Schmidt, J. Bormann, D. Stoffel, W. Kunz: "A New SAT-Based Approach for Equivalence Checking of Hardware-Dependent Low-Level Embedded System Software"  edaWorkshop13, Dresden, Germany, May 2013 

  • C. Villarraga, B. Schmidt, C. Bartsch, J. Bormann, D. Stoffel, and W. Kunz: "A New SAT-Based Approach for Equivalence Checking of Hardware-Dependent Low-Level Embedded System Software". 50th Design Automation Conference (DAC 2013) Work-In-Progress (WIP), Austin (Texas), June 2013.

  • B. Bao, J. Bormann, M. Wedler, D. Stoffel, W. Kunz: „Coverage of Compositional Property Sets under Reactive Constraints“, Work in Progress DAC 2013, Austin (Texas), June 2013

  • B. Schmidt, C. Villarraga, T. Fehmel, J. Bormann, M. Wedler, M. Nguyen, D. Stoffel, W. Kunz: "A New Formal Verification Approach for Hardware-dependent Embedded System Software"  Special Issue on ASP-DAC 2013, IPSJ Transactions on System LSI Design Methodology Vol. 6(2013), August 2013 

  • C. Villarraga, B. Schmidt, C. Bartsch, J. Bormann, D. Stoffel, and W. Kunz: "An Equivalence Checker for Hardware-Dependent Embedded System Software",  Eleventh ACM-IEEE International Conference on  Formal Methods and Models for Codesign (MEMOCODE), Portland (Oregon), USA, October 2013

  • J. Urdahl, S. Udupi, D. Stoffel, W. Kunz: "Formal System-on-Chip Verification: An Operation-Based Methodology and its Perspectives in Low Power Design", Proc. 23th International Workshop on Power and Timing Modeling, Optimization and Simulation (PATMOS'13), September 2013

  • J. Urdahl, D. Stoffel, W. Kunz: "Path Predicate Abstraction for Sound System-Level Models of RT-Level Circuit Designs", Accepted for IEEE Transactions on Computer Aided Design (TCAD), Oktober 2013.

  • O. Marx, M. Wedler, A. Dreyer, D. Stoffel, W. Kunz: "Proof Logging for Computer Algebra based SMT Solving", Proc. of the ACM/IEEE  International Conference on Computer-Aided Design (ICCAD) , San Jose (California), USA, November 2013

  • B. Bao, J. Bormann, M. Wedler, D. Stoffel, W. Kunz: "Formal Plausibility Checks for Environment Constraints" in J. Haase (Ed.), Models, Methods, and Tools for Complex Chip Design, Springer, 2014, ISBN 978-3-319-01417-3

2012 

© 2012 IEEE. Personal use of this material is permitted. However, permission to reprint/republish this material for advertising or promotional purposes or for creating new collective works for resale or redistribution to servers or lists, or to reuse any copyrighted component of this work in other works must be obtained from the IEEE.

  • M. Wedler, E. Crabill, G. Schelle, P. Lysaght: “Using Formal Verification for HW/SW Co-verification of an FPGA IP Core”, The XCell Journal – Solutions for a Programmable World, Issue 79, Second Quarter, 2012.

  • J. Urdahl, D. Stoffel, M. Wedler, W. Kunz: "System Verification of Concurrent RTL Modules by Compositional Path Predicate Abstraction", Proc. Design Automation Conference (DAC), San Francisco CA, USA, June 3-7, 2012

  • Minh D. Nguyen, W. Kunz: “Hardware/Software Formal Co-Verification Using Hardware Verification Techniques” Proc. of the 4th International Conference on Communications and Electronics (ICCE'12), Hue, Vietnam, 01-03 July, 2012

  • W. Kunz: “System-level models for System-on-Chip implementations: Can we close the semantic gap with formal property checking?” Proc. of the 4th International Conference on Communications and Electronics (ICCE'12), Hue, Vietnam, 01-03 July, 2012 (invited presentation)

  • Binghao Bao, Joerg Bormann, Markus Wedler, Dominik Stoffel, Wolfgang Kunz: "Formal Plausibility Checks for Environment Constraints", Proc. Forum on Specification & Design Languages (FDL), September 2012, Vienna, Austria

2011 

© 2011 IEEE. Personal use of this material is permitted. However, permission to reprint/republish this material for advertising or promotional purposes or for creating new collective works for resale or redistribution to servers or lists, or to reuse any copyrighted component of this work in other works must be obtained from the IEEE.

 

2010 

© 2010 IEEE. Personal use of this material is permitted. However, permission to reprint/republish this material for advertising or promotional purposes or for creating new collective works for resale or redistribution to servers or lists, or to reuse any copyrighted component of this work in other works must be obtained from the IEEE.

  • J. Urdahl, D. Stoffel, J. Bormann, M. Wedler, W. Kunz: "Path Predicate Abstraction by Complete Interval Property Checking",Proc. Formal Methods in Computer-Aided Design (FMCAD), Lugano, CH, Oktober, 2010
     
  • S. Loitz, M. Wedler, D. Stoffel, C. Brehm, W. Kunz, N. Wehn: "Complete Verification of Weakly Programmable IPs against their Operational ISA Model", 4.GMM/GI/ITG-Fachtagung Zuverlässigkeit und Entwurf, Wildbad Kreuth, Germany, September, 2010
     
  • S. Loitz, M. Wedler, D. Stoffel, C. Brehm, W. Kunz, N. Wehn: "Complete Verification of Weakly Programmable IPs against their Operational ISA Model", Proc. Forum on Specification & Design Languages, Southampton, UK, September, 2010
     
  • M. Thalmaier, M. Nguyen , M. Wedler, D. Stoffel, J. Bormann, W. Kunz: “Analyzing k-Step Induction to Compute Invariants for SAT-Based Property Checking” , Proc. Design Automation Conference (DAC), Anaheim CA, USA, June 13-19, 2010
     
  • M. Wedler, E. Pavlenko, A. Dreyer, F. Seelisch, D. Stoffel, G.-M. Greuel, W. Kunz, “Solving hard instances in QF-BV combining Boolean reasoning with computer algebra", Dagstuhl Seminar Proceedings 09461, Algorithms and Applications for Next Generation SAT Solvers, Schloss Dagstuhl - Leibniz-Zentrum fuer Informatik, Germany, 2010
     
  • M. Wedler, S. Loitz, W. Kunz: “Gap-Free verification of weakly programmable IPs against their operational ISA model ”, Proc. International Workshop on Designing Correct Circuits (DCC), Paphos, Cyprus, Mar. 2010
     
  • M. Thalmaier, M. Nguyen, M. Wedler, D. Stoffel, W. Kunz: "Analyzing k-step induction to compute invariants for SAT-based property checking", 13. GI/ITG/GMM Workshop Modellierung und Verifikation, Dresden, Feb. 2010

  • M. Nguyen, M. Thalmaier, M. Wedler, D. Stoffel, W. Kunz, J. Bormann: "A Re-Use Methodology for Formal SoC Protocol Compliance Verification”, in D. Borrione (Ed.), Advances in Design Methods from Modeling Languages for Embedded Systems and SoC's, Springer, 2010, ISBN 978-90-481-9303-5.

2009

© 2009 IEEE. Personal use of this material is permitted. However, permission to reprint/republish this material for advertising or promotional purposes or for creating new collective works for resale or redistribution to servers or lists, or to reuse any copyrighted component of this work in other works must be obtained from the IEEE.

  • M. Nguyen, M. Thalmaier, D. Stoffel, M. Wedler, W. Kunz: “A Re-Use Methodology for Formal SoC Protocol Compliance Verification”, Proc. Forum on Specification & Design Languages, Sophia Antipolis, France, September 2009.
     
  • M. Nguyen, M. Thalmaier, M. Wedler, D. Stoffel, W. Kunz: “Recorder-based SoC Protocol Compliance Verification”, 12. GI/ITG/GMM Workshop Modellierung und Verifikation, Berlin, S.57 -66, ISBN 978-3-7983-2118-2, März 2009.
     
  • Jan Zutter, Max Thalmaier, Martin Klein, Karsten-Olaf Laux, "Acceleration of RSA Cryptographic Operations using FPGA Technology"IEEE EDACS Conference at DEXA 2009
     
    , Sept. 1, Linz, Austria.
     
  • J. Bormann: “Complete Functional Verification”, Formal Methods in Computer Aided Design (FMCAD) 2009, Austin, Texas, USA, November 15 – 18.
     
  • M. Brickenstein, A. Dreyer, G.-M. Greuel, M. Wedler, O. Wienand: "New developments in the theory of Groebner bases and applications to formal verification"Journal of Pure and Applied Algebra, Vol. 213 (2009), 1612-1635.

  • E. Pavlenko, M. Wedler, D. Stoffel, W. Kunz, O. Wienand, E. Karibaev: "A New Verification Technique for Custom-Designed Components at the Arithmetic Bit Level”, in M. Radetzki (Ed.), Languages for Embedded Systems and their Applications, Springer, 2009, ISBN 1-4020-9713-3.

2008

© 2008 IEEE. Personal use of this material is permitted. However, permission to reprint/republish this material for advertising or promotional purposes or for creating new collective works for resale or redistribution to servers or lists, or to reuse any copyrighted component of this work in other works must be obtained from the IEEE.

2007 

© 2007 IEEE. Personal use of this material is permitted. However, permission to reprint/republish this material for advertising or promotional purposes or for creating new collective works for resale or redistribution to servers or lists, or to reuse any copyrighted component of this work in other works must be obtained from the IEEE.

  • D. Eberhard: "Kapselung sicherheitskritischer Funktionen in automobilen Steuergeräten", Tagungsband GI Fachtagung Mobilität und Echtzeit, December 2007, Boppard, Germany
     
  • E. Pavlenko, M. Wedler, D. Stoffel, W. Kunz: "Arithmetic Constraints in SAT-based Property Checking", TagungsbandGI/ITG/GMM-Workshop Methoden und Beschreibungssprachen zur Modellierung und Verifikation von Schaltungen und Systemen, März 2007, Erlangen
     
  • M. Braun, H. Eveking, M. Schickel, M. Nguyen, W. Kunz: "Methoden > zur Verifikation von Kommunikationsstrukturen", Tagungsband GI/ITG/GMM-Workshop Methoden und Beschreibungssprachen zur Modellierung und Verifikation von Schaltungen und Systemen, März 2007, Erlangen
     
  • M. Thalmaier, M. D. Nguyen, M. Wedler, D. Stoffel, W. Kunz: "Formale Verifikation von SoC Protokollimplementierungen", Tagungsband 1.GMM/GI/ITG-Fachtagung Zuverlässigkeit und Entwurf, Mar. 26-28 2007, Munich, Germany
     
  • M. Wedler, D. Stoffel, R. Brinkmann, W. Kunz: "A Normalization Method for Arithmetic Data Path Verification", IEEE Transactions on Computer-Aided Design of Circuits and Systems, Vol. 26, pp. 1909-1922, November 2007
     

2006

© 2006 IEEE. Personal use of this material is permitted. However, permission to reprint/republish this material for advertising or promotional purposes or for creating new collective works for resale or redistribution to servers or lists, or to reuse any copyrighted component of this work in other works must be obtained from the IEEE.

  • W. Kunz: "Formale Verifikation von System-on-Chip-Entwürfen", Proc. VDE - Kongress, October 2006, Aachen, Germany
     
  • U. Krautz, M. Pflanz, C. Jacobi, H. W. Tast, K. Weber, H. T. Vierhaus: "Evaluating coverage of error detection logic for soft errors using formal methods", Proc. Design, Automation and Test in Europe, (DATE) Mar. 6-10 2006, Munich, Germany
     
  • I. Neumann: " Modelling Synchronous Multi-Clock Circuits for Retiming", Tagungsband GI/ITG/GMM-Workshop Methoden und Beschreibungssprachen zur Modellierung und Verifikation von Schaltungen und Systemen, Feb. 20-22 2006, Dresden
     
  • A. Jesser, M. Wedler, L. Hedrich, W. Kunz: " A case study on applying bounded model checking to analog circuit verification", Tagungsband GI/ITG/GMM-Workshop Methoden und Beschreibungssprachen zur Modellierung und Verifikation von Schaltungen und Systemen, Feb. 20-22 2006, Dresden 
     

2005

© 2005 IEEE. Personal use of this material is permitted. However, permission to reprint/republish this material for advertising or promotional purposes or for creating new collective works for resale or redistribution to servers or lists, or to reuse any copyrighted component of this work in other works must be obtained from the IEEE.

  • M. D. Nguyen, D. Stoffel, M. Wedler, W. Kunz: " Transition-by-Transition FSM Traversal for Reachability Analysis in Bounded Model Checking", Proc. International Conference on Computer Aided Design, Nov. 6-10 2005, San Jose, USA

  • M. D. Nguyen, D. Stoffel, W. Kunz: "Enhancing BMC-based Protocol Verification Using Transition-By-Transition FSM Traversal", 303-307, INFORMATIK 2005 - Informatik LIVE! Band 1, Beiträge der 35. Jahrestagung der Gesellschaft für Informatik e.V. (GI), Bonn, Sep. 19-22 2005, Bonn, Germany

  • M. Wedler, D. Stoffel, W. Kunz: " Frontend Model Generation for SAT-Based Property Checking", Proc. 6th Int. Conference On ASIC, Oct. 24-27, 2005, Shanghai, China

  • M. Wedler, D. Stoffel, W. Kunz: " Normalization at the Arithmetic Bit Level", Proc. Design Automation Conference (DAC), June 13-17, 2005, Anaheim CA, USA

  • M. Wedler, D. Stoffel, W. Kunz: "Verification of arithmetic processor units by ABL normalization", Tagungsband GI/ITG/GMM-Workshop Methoden und Beschreibungssprachen zur Modellierung und Verifikation von Schaltungen und Systemen, April 6-7 2005 München.

 

2004

© 2004 IEEE. Personal use of this material is permitted. However, permission to reprint/republish this material for advertising or promotional purposes or for creating new collective works for resale or redistribution to servers or lists, or to reuse any copyrighted component of this work in other works must be obtained from the IEEE.

2003

© 2003 IEEE. Personal use of this material is permitted. However, permission to reprint/republish this material for advertising or promotional purposes or for creating new collective works for resale or redistribution to servers or lists, or to reuse any copyrighted component of this work in other works must be obtained from the IEEE.

  • I. Neumann, W. Kunz: "Layout Driven Retiming Using the Coupled Edge Timing Model", IEEE Transactions on Computer Aided Design, vol. 22, no. 7, pp. 825-835, July 2003.
     
  • I. Neumann, D. Stoffel, M. Berkelaar, W. Kunz: "Layout Driven Synthesis of Datapath Circuits using Arithmetic Reasoning", Proc. of the International Workshop on Logic & Synthesis, (IWLS) May 28-30 2003, Laguna Beach CA, USA.
     
  • M. Wedler, D. Stoffel, W. Kunz: "Using RTL statespace information and state encoding for induction based property checking", Proc. Design, Automation and Test in Europe, (DATE) March 2003, München.
     
  • K. Winkelmann, J. Trylus, D. Stoffel, G. Fey: "Cost-efficient Formal Block Verification for ASIC Design", TagungsbandGI/ITG/GMM-Workshop Methoden und Beschreibungssprachen zur Modellierung und Verifikation von Schaltungen und Systemen, Feb. 2003.
     
  • M. Wedler, D. Stoffel, W. Kunz: "The impact of state encoding on induction based property checking", TagungsbandGI/ITG/GMM-Workshop Methoden und Beschreibungssprachen zur Modellierung und Verifikation von Schaltungen und Systemen, Feb. 2003.

  • D. Stoffel, E. Karibaev, I. Kufareva, W. Kunz: "Equivalence Checking of Arithmetic Circuits”, in R. Drechsler (Ed.), Advanced Formal Verification, Kluwer Academic Publishers, Boston, MA, USA, 2003, ISBN 1-4020-7721-1.

2002

© 2002 IEEE. Personal use of this material is permitted. However, permission to reprint/republish this material for advertising or promotional purposes or for creating new collective works for resale or redistribution to servers or lists, or to reuse any copyrighted component of this work in other works must be obtained from the IEEE.

  • D. Stoffel, M. Wedler, W. Kunz: "Structural FSM traversal for sequential equivalence checking and property checking", Tagungsband Dagstuhl Seminar Formal Circuit Equivalence Verification, Aug. 2002.

  • M. Wedler, D. Stoffel, W. Kunz: "Using RTL statespace information and state encoding for induction based propert", Tagungsband Dagstuhl Seminar Formal Circuit Equivalence Verification, Aug. 2002.

  • I. Neumann, K. Sulimma, W. Kunz: "Accelerating Retiming Under the Coupled-Edge Timing Model", Proc. of the IEEE Annual Symposum on VLSI, (ISVLSI) Apr. 25-26 2002, Pittsburgh Pennsylvania, USA

  • M. Wedler, D. Stoffel, W. Kunz: "Improving structural FSM traversal by constraint-satisfying simulation", Proc. of the IEEE Annual Symposum on VLSI, (ISVLSI) Apr. 25-26 2002, Pittsburgh Pennsylvania, USA

  • K. Sulimma, I. Neumann, L. Van Ginneken, W. Kunz: "Improving Placement under the Constant Delay Model", Proc. Design, Automation and Test in Europe, (DATE) March 2002, Paris, France

  • T.Kutzschebauch, L.Stok: " Layout Driven Decomposition with Congestion Consideration ", Proc. Design, Automation and Test in Europe, (DATE) March 2002, Paris, France

  • W. Kunz, J. Marques-Silva, S. Malik: "SAT and ATPG: Algorithms for Boolean Decision Problems", in S. Hassoun and T. Sasao (Ed.), Logic Synthesis and Verification, Kluwer Academic Publishers, Boston, MA 2002, ISBN 0-7923-7606-4.


2001

© 2001 IEEE. Personal use of this material is permitted. However, permission to reprint/republish this material for advertising or promotional purposes or for creating new collective works for resale or redistribution to servers or lists, or to reuse any copyrighted component of this work in other works must be obtained from the IEEE.


Selected older papers

© 1994 - 2000 IEEE. Personal use of this material is permitted. However, permission to reprint/republish this material for advertising or promotional purposes or for creating new collective works for resale or redistribution to servers or lists, or to reuse any copyrighted component of this work in other works must be obtained from the IEEE.


Technical Reports


 

Dissertations and Habilitations