Wolfgang Kunz

Orcid: 0000-0002-6612-2946

Affiliations:
  • University of Kaiserslautern


According to our database1, Wolfgang Kunz authored at least 127 papers between 1992 and 2024.

Collaborative distances:

Awards

IEEE Fellow

IEEE Fellow 2006, "For contributions to hardware verification, very large scale integrated (VLSI) circuit testing and logic synthesis.".

Timeline

Legend:

Book 
In proceedings 
Article 
PhD thesis 
Dataset
Other 

Links

Online presence:

On csauthors.net:

Bibliography

2024
A Scalable Formal Verification Methodology for Data-Oblivious Hardware.
IEEE Trans. Comput. Aided Des. Integr. Circuits Syst., September, 2024

VeriCHERI: Exhaustive Formal Security Verification of CHERI at the RTL.
CoRR, 2024

Efficient Stimuli Generation using Reinforcement Learning in Design Verification.
CoRR, 2024

Data-Oblivious and Performant: On Designing Security-Conscious Hardware.
Proceedings of the 25th IEEE Latin American Test Symposium, 2024

An Automated Exhaustive Fault Analysis Technique guided by Processor Formal Verification Methods.
Proceedings of the 25th International Symposium on Quality Electronic Design, 2024

A Golden-Free Formal Method for Trojan Detection in Non-Interfering Accelerators.
Proceedings of the Design, Automation & Test in Europe Conference & Exhibition, 2024

MCU-Wide Timing Side Channels and Their Detection.
Proceedings of the 61st ACM/IEEE Design Automation Conference, 2024

2023
An Exhaustive Approach to Detecting Transient Execution Side Channels in RTL Designs of Processors.
IEEE Trans. Computers, 2023

Okapi: A Lightweight Architecture for Secure Speculation Exploiting Locality of Memory Accesses.
CoRR, 2023

A New Security Threat in MCUs - SoC-wide timing side channels and how to find them.
CoRR, 2023

Fault Attacks on Access Control in Processors: Threat, Formal Analysis and Microarchitectural Mitigation.
IEEE Access, 2023

Design of Access Control Mechanisms in Systems-on-Chip with Formal Integrity Guarantees.
Proceedings of the 32nd USENIX Security Symposium, 2023

UPEC-PN: Exhaustive constant time verification of low-level software using property checking.
Proceedings of the Methods and Description Languages for Modelling and Verification of Circuits and Systems, 2023

Secure-by-Construction Design Methodology for CPUs: Implementing Secure Speculation on the RTL.
Proceedings of the IEEE/ACM International Conference on Computer Aided Design, 2023

2022
Generation of Formal CPU Profiles for Embedded Systems.
Proceedings of the 30th IFIP/IEEE 30th International Conference on Very Large Scale Integration, 2022

Fast and Accurate Model-Driven FPGA-based System-Level Fault Emulation.
Proceedings of the 30th IFIP/IEEE 30th International Conference on Very Large Scale Integration, 2022

Design of a Tightly-Coupled RISC-V Physical Memory Protection Unit for Online Error Detection.
Proceedings of the 30th IFIP/IEEE 30th International Conference on Very Large Scale Integration, 2022

Compositional Fault Propagation Analysis in Embedded Systems using Abstract Interpretation.
Proceedings of the Methods and Description Languages for Modelling and Verification of Circuits and Systems, 2022

MetaFS: Model-driven Fault Simulation Framework.
Proceedings of the IEEE International Symposium on Defect and Fault Tolerance in VLSI and Nanotechnology Systems, 2022


Towards a formally verified hardware root-of-trust for data-oblivious computing.
Proceedings of the DAC '22: 59th ACM/IEEE Design Automation Conference, San Francisco, California, USA, July 10, 2022

2021
Effective Pre-Silicon Verification of Processor Cores by Breaking the Bounds of Symbolic Quick Error Detection.
CoRR, 2021


A Formal Approach to Confidentiality Verification in SoCs at the Register Transfer Level.
Proceedings of the 58th ACM/IEEE Design Automation Conference, 2021

2020
Generation of Abstract Driver Models for IP Integration Verification.
IEEE Trans. Emerg. Top. Comput., 2020

Properties First - Correct-By-Construction RTL Design in System-Level Design Flows.
IEEE Trans. Comput. Aided Des. Integr. Circuits Syst., 2020

Efficient binary-level coverage analysis.
Proceedings of the ESEC/FSE '20: 28th ACM Joint European Software Engineering Conference and Symposium on the Foundations of Software Engineering, 2020

Area Estimation Framework for Digital Hardware Design using Machine Learning.
Proceedings of the 23rd GMM/ITG/GI Workshop on Methods and Description Languages for Modelling and Verification of Circuits and Systems, 2020

Automatic State Space Analysis for Modeling Untrusted Embedded Device Drivers.
Proceedings of the 23rd Euromicro Conference on Digital System Design, 2020

Gap-free Processor Verification by S<sup>2</sup>QED and Property Generation.
Proceedings of the 2020 Design, Automation & Test in Europe Conference & Exhibition, 2020

A Formal Approach for Detecting Vulnerabilities to Transient Execution Attacks in Out-of-Order Processors.
Proceedings of the 57th ACM/IEEE Design Automation Conference, 2020

2019
Exploiting Hardware Unobservability for Low-Power Design and Safety Analysis in Formal Verification-Driven Design Flows.
IEEE Trans. Very Large Scale Integr. Syst., 2019

ACCESS: HW/SW-Co-Equivalence Checking for Firmware Optimization.
Proceedings of the 22nd Workshop Methods and Description Languages for Modelling and Verification of Circuits and Systems, 2019

How to Keep 4-Eyes Principle in a Design and Property Generation Flow.
Proceedings of the 22nd Workshop Methods and Description Languages for Modelling and Verification of Circuits and Systems, 2019

Systematic RISC-V based Firmware Design<sup>⋆</sup>.
Proceedings of the 2019 Forum for Specification and Design Languages, 2019

Symbolic QED Pre-silicon Verification for Automotive Microcontroller Cores: Industrial Case Study.
Proceedings of the Design, Automation & Test in Europe Conference & Exhibition, 2019

Processor Hardware Security Vulnerabilities and their Detection by Unique Program Execution Checking.
Proceedings of the Design, Automation & Test in Europe Conference & Exhibition, 2019

ACCESS: HW/SW Co-Equivalence Checking for Firmware Optimization.
Proceedings of the 56th Annual Design Automation Conference 2019, 2019

2018
Symbolic quick error detection using symbolic initial state for pre-silicon verification.
Proceedings of the 2018 Design, Automation & Test in Europe Conference & Exhibition, 2018

2017
A HW/SW Cross-Layer Approach for Determining Application-Redundant Hardware Faults in Embedded Systems.
J. Electron. Test., 2017

Special session on early life failures.
Proceedings of the 35th IEEE VLSI Test Symposium, 2017

Dynamic Power Optimization Based on Formal Property Checking of Operations.
Proceedings of the 30th International Conference on VLSI Design and 16th International Conference on Embedded Systems, 2017

Speculative disassembly of binary code.
Proceedings of the Methoden und Beschreibungssprachen zur Modellierung und Verifikation von Schaltungen und Systemen, 2017

goSAT: Floating-point satisfiability as global optimization.
Proceedings of the 2017 Formal Methods in Computer Aided Design, 2017

Cycle-accurate software modeling for RTL verification of embedded systems.
Proceedings of the 20th IEEE International Symposium on Design and Diagnostics of Electronic Circuits & Systems, 2017

2016
A computer-algebraic approach to formal verification of data-centric low-level software.
Proceedings of the 2016 ACM/IEEE International Conference on Formal Methods and Models for System Design, 2016

A HW-dependent Software Model for Cross-Layer Fault Analysis in Embedded Systems.
Proceedings of the 19th GI/ITG/GMM Workshop Methoden und Beschreibungssprachen zur Modellierung und Verifikation von Schaltungen und Systemen, 2016

Safety across the HW/SW interface - Can formal methods meet the challenge?
Proceedings of the International Symposium on Integrated Circuits, 2016

Properties first? a new design methodology for hardware, and its perspectives in safety analysis.
Proceedings of the 35th International Conference on Computer-Aided Design, 2016

The European Masters in Embedded Computing Systems (EMECS).
Proceedings of the 11th European Workshop on Microelectronics Education, 2016

2015
Architectural System Modeling for Correct-by-Construction RTL Design.
Proceedings of the Methoden und Beschreibungssprachen zur Modellierung und Verifikation von Schaltungen und Systemen, 2015

2014
Path Predicate Abstraction for Sound System-Level Models of RT-Level Circuit Designs.
IEEE Trans. Comput. Aided Des. Integr. Circuits Syst., 2014

T4B: Formal verification in system-on-chip design: Scientific foundations and practical methodology.
Proceedings of the 27th IEEE International System-on-Chip Conference, 2014

Efficient SAT/simulation-based model generation for low-level embedded software.
Proceedings of the Methoden und Beschreibungssprachen zur Modellierung und Verifikation von Schaltungen und Systemen, 2014

Software in a hardware view: New models for HW-dependent software in SoC verification and test.
Proceedings of the 2014 International Test Conference, 2014

Coverage of compositional property sets under reactive constraints.
Proceedings of the Fifteenth International Symposium on Quality Electronic Design, 2014

A property language for the specification of hardware-dependent embedded system software.
Proceedings of the 2014 Forum on Specification and Design Languages, 2014

2013
A New Formal Verification Approach for Hardware-dependent Embedded System Software.
IPSJ Trans. Syst. LSI Des. Methodol., 2013

Formal system-on-chip verification: An operation-based methodology and its perspectives in low power design.
Proceedings of the 2013 23rd International Workshop on Power and Timing Modeling, 2013

An equivalence checker for hardware-dependent embedded system software.
Proceedings of the 11th ACM/IEEE International Conference on Formal Methods and Models for Codesign, 2013

A Hardware-Dependent Model for SAT-based Verification of Interrupt-Driven Low-level Embedded System Software.
Proceedings of the Methoden und Beschreibungssprachen zur Modellierung und Verifikation von Schaltungen und Systemen (MBMV), 2013

Compositional Completeness over reactive Constraints.
Proceedings of the Methoden und Beschreibungssprachen zur Modellierung und Verifikation von Schaltungen und Systemen (MBMV), 2013

Proof logging for computer algebra based SMT solving.
Proceedings of the IEEE/ACM International Conference on Computer-Aided Design, 2013

Environmental Information System and Odour Monitoring based on Citizen and Technology Innovative Sensors.
Proceedings of the 27th International Conference on Environmental Informatics for Environmental Protection, 2013

A computational model for SAT-based verification of hardware-dependent low-level embedded system software.
Proceedings of the 18th Asia and South Pacific Design Automation Conference, 2013

2012
Formal plausibility checks for environment constraints.
Proceedings of the Proceeding of the 2012 Forum on Specification and Design Languages, 2012

System verification of concurrent RTL modules by compositional path predicate abstraction.
Proceedings of the 49th Annual Design Automation Conference 2012, 2012

2011
Validation of channel decoding ASIPs a case study.
Proceedings of the 22nd IEEE International Symposium on Rapid System Prototyping, 2011

STABLE: A new QF-BV SMT Solver for hard Verification Problems combining Boolean Reasoning with Computer Algebra.
Proceedings of the Methoden und Beschreibungssprachen zur Modellierung und Verifikation von Schaltungen und Systemen (MBMV), 2011

Formal Hardware/Software Co-Verification by Interval Property Checking with Abstraction.
Proceedings of the Methoden und Beschreibungssprachen zur Modellierung und Verifikation von Schaltungen und Systemen (MBMV), 2011

Formal hardware/software co-verification by interval property checking with abstraction.
Proceedings of the 48th Design Automation Conference, 2011

2010
Analyzing k-step induction to compute invariants for SAT-based property checking.
Proceedings of the Methoden und Beschreibungssprachen zur Modellierung und Verifikation von Schaltungen und Systemen (MBMV), 2010

Path predicate abstraction by complete interval property checking.
Proceedings of 10th International Conference on Formal Methods in Computer-Aided Design, 2010

Complete Verification of Weakly Programmable IPs against Their Operational ISA Model.
Proceedings of the 2010 Forum on specification & Design Languages, 2010

Analyzing <i>k</i>-step induction to compute invariants for SAT-based property checking.
Proceedings of the 47th Design Automation Conference, 2010

2009
A Re-Use Methodology for SoC Protocol Compliance Verification.
Proceedings of the Methoden und Beschreibungssprachen zur Modellierung und Verifikation von Schaltungen und Systemen (MBMV), 2009

A re-use methodology for formal SoC protocol compliance verification.
Proceedings of the Forum on specification and Design Languages, 2009

Solving hard instances in QF-BV combining Boolean reasoning with computer algebra.
Proceedings of the Algorithms and Applications for Next Generation SAT Solvers, 08.11., 2009

2008
Unbounded Protocol Compliance Verification Using Interval Property Checking With Invariants.
IEEE Trans. Comput. Aided Des. Integr. Circuits Syst., 2008

Proving Functional Correctness of Weakly Programmable IPs - A Case Study with Formal Property Checking.
Proceedings of the IEEE Symposium on Application Specific Processors, 2008

Modeling of Custom-Designed Arithmetic Components for ABL Normalization.
Proceedings of the Methoden und Beschreibungssprachen zur Modellierung und Verifikation von Schaltungen und Systemen (MBMV), 2008

A New Verification Technique for Custom-Designed Components at the Arithmetic Bit Level.
Proceedings of the Languages for Embedded Systems and their Applications, 2008

An Algebraic Approach for Proving Data Correctness in Arithmetic Data Paths.
Proceedings of the Computer Aided Verification, 20th International Conference, 2008

Verifying full-custom multipliers by Boolean equivalence checking and an arithmetic bit level proof.
Proceedings of the 13th Asia South Pacific Design Automation Conference, 2008

2007
A Normalization Method for Arithmetic Data-Path Verification.
IEEE Trans. Comput. Aided Des. Integr. Circuits Syst., 2007

Arithmetic Constraints in SAT-based Property Checking.
Proceedings of the Methoden und Beschreibungssprachen zur Modellierung und Verifikation von Schaltungen und Systemen (MBMV), 2007

Methoden zur Verifikation von Kommunikationsstrukturen.
Proceedings of the Methoden und Beschreibungssprachen zur Modellierung und Verifikation von Schaltungen und Systemen (MBMV), 2007

2006
A case study on applying bounded model checking to analog circuit verification.
Proceedings of the Methoden und Beschreibungssprachen zur Modellierung und Verifikation von Schaltungen und Systemen (MBMV), 2006

2005
Transition-by-transition FSM traversal for reachability analysis in bounded model checking.
Proceedings of the 2005 International Conference on Computer-Aided Design, 2005

Enhancing BMC-based Protocol Verification Using Transition-By-Transition FSM Traversal.
Proceedings of the 35. Jahrestagung der Gesellschaft für Informatik, 2005

Normalization at the arithmetic bit level.
Proceedings of the 42nd Design Automation Conference, 2005

2004
Structural FSM traversal.
IEEE Trans. Comput. Aided Des. Integr. Circuits Syst., 2004

Equivalence checking of arithmetic circuits on the arithmetic bit level.
IEEE Trans. Comput. Aided Des. Integr. Circuits Syst., 2004

Layout Driven Optimization of Datapath Circuits using Arithmetic Reasoning.
Proceedings of the 22nd IEEE International Conference on Computer Design: VLSI in Computers & Processors (ICCD 2004), 2004

Arithmetic Reasoning in DPLL-Based SAT Solving.
Proceedings of the 2004 Design, 2004

Exploiting state encoding for invariant generation in induction-based property checking.
Proceedings of the 2004 Conference on Asia South Pacific Design Automation: Electronic Design and Solution Fair 2004, 2004

2003
Layout driven retiming using the coupled edge timing model.
IEEE Trans. Comput. Aided Des. Integr. Circuits Syst., 2003

Towards the impact of state encoding on induction-based property checking.
Proceedings of the Methoden und Beschreibungssprachen zur Modellierung und Verifikation von Schaltungen und Systemen (MBMV), 2003

Using RTL Statespace Information and State Encoding for Induction Based Property Checking.
Proceedings of the 2003 Design, 2003

2002
Improving Placement under the Constant Delay Model.
Proceedings of the Methoden und Beschreibungssprachen zur Modellierung und Verifikation von Schaltungen und Systemen (MBMV), 2002

Improving Structural FSM Traversal by Constraint-Satisfying Logic Simulation.
Proceedings of the 2002 IEEE Computer Society Annual Symposium on VLSI (ISVLSI 2002), 2002

Accelerating Retiming Under the Coupled-Edge Timing Model.
Proceedings of the 2002 IEEE Computer Society Annual Symposium on VLSI (ISVLSI 2002), 2002

SAT and ATPG: Boolean engines for formal hardware verification.
Proceedings of the 2002 IEEE/ACM International Conference on Computer-aided Design, 2002

2001
Äquivalenzvergleich mit strukturellen Methoden (Equivalence Checking using Structural Methods).
Informationstechnik Tech. Inform., 2001

Performance Optimization during Placement by Retiming.
Proceedings of the Methoden und Beschreibungssprachen zur Modellierung und Verifikation von Schaltungen und Systemen (MBMV), 2001

An exact algorithm for solving difficult detailed routing problems.
Proceedings of the 2001 International Symposium on Physical Design, 2001

Tight coupling of timing-driven placement and retiming.
Proceedings of the 2001 International Symposium on Circuits and Systems, 2001

Cycle time optimization by timing driven placement with simultaneous netlist transformations.
Proceedings of the 2001 International Symposium on Circuits and Systems, 2001

Verification of Integer Multipliers on the Arithmetic Bit Level.
Proceedings of the 2001 IEEE/ACM International Conference on Computer-Aided Design, 2001

Placement Driven Retiming with a Coupled Edge Timing Model.
Proceedings of the 2001 IEEE/ACM International Conference on Computer-Aided Design, 2001

1999
Cell replication and redundancy elimination during placement for cycle time optimization.
Proceedings of the 1999 IEEE/ACM International Conference on Computer-Aided Design, 1999

Accelerating Boolean Implications with FPGAs.
Proceedings of the Field-Programmable Logic and Applications, 9th International Workshop, 1999

1998
LOT: Logic Optimization with Testability. New transformations for logic synthesis.
IEEE Trans. Comput. Aided Des. Integr. Circuits Syst., 1998

1997
Logic optimization and equivalence checking by implication analysis.
IEEE Trans. Comput. Aided Des. Integr. Circuits Syst., 1997

Record & play: a structural fixed point iteration for sequential circuit verification.
Proceedings of the 1997 IEEE/ACM International Conference on Computer-Aided Design, 1997

AND/OR reasoning graphs for determining prime implicants in multi-level combinational networks.
Proceedings of the ASP-DAC '97 Asia and South Pacific Design Automation Conference, 1997

Reasoning in Boolean Networks - Logic Synthesis and Verification Using Testing Techniques.
Frontiers in electronic testing, Springer, ISBN: 978-0-7923-9921-6, 1997

1996
A novel framework for logic verification in a synthesis environment.
IEEE Trans. Comput. Aided Des. Integr. Circuits Syst., 1996

Gate-level synthesis for low-power using new transformations.
Proceedings of the 1996 International Symposium on Low Power Electronics and Design, 1996

1995
LOT: logic optimization with testability-new transformations using recursive learning.
Proceedings of the 1995 IEEE/ACM International Conference on Computer-Aided Design, 1995

Novel Verification Framework Combining Structural and OBDD Methods in a Synthesis Environment.
Proceedings of the 32st Conference on Design Automation, 1995

1994
Recursive learning: a new implication technique for efficient solutions to CAD problems-test, verification, and optimization.
IEEE Trans. Comput. Aided Des. Integr. Circuits Syst., 1994

Multi-level logic optimization by implication analysis.
Proceedings of the 1994 IEEE/ACM International Conference on Computer-Aided Design, 1994

1993
Accelerated dynamic learning for test pattern generation in combinational circuits.
IEEE Trans. Comput. Aided Des. Integr. Circuits Syst., 1993

HANNIBAL: an efficient tool for logic verification based on recursive learning.
Proceedings of the 1993 IEEE/ACM International Conference on Computer-Aided Design, 1993

1992
Rekursives Lernen: eine präzise Implikationsprozedur und ihre Anwendung auf die Testmustergenerierung in digitalen Schaltungen.
PhD thesis, 1992

Recursive Learning: An Attractive Alternative to the Decision Tree for Test Genration in Digital Circuits.
Proceedings of the Proceedings IEEE International Test Conference 1992, 1992


  Loading...