Zur Hauptnavigation / To main navigation

Zur Sekundärnavigation / To secondary navigation

Zum Inhalt dieser Seite / To the content of this page

Sekundärnavigation / Secondary navigation

Inhaltsbereich / Content

Publications

Conference and Journal papers

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