Wolfgang Kunz
Orcid: 0000-0002-6612-2946Affiliations:
- University of Kaiserslautern
According to our database1,
Wolfgang Kunz
authored at least 122 papers
between 1992 and 2023.
Collaborative distances:
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 OtherLinks
Online presence:
-
on orcid.org
On csauthors.net:
Bibliography
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
CoRR, 2023
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
Proceedings of the 30th IFIP/IEEE 30th International Conference on Very Large Scale Integration, 2022
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
Proceedings of the IEEE International Symposium on Defect and Fault Tolerance in VLSI and Nanotechnology Systems, 2022
Proceedings of the 2022 Design, Automation & Test in Europe Conference & Exhibition, 2022
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
Proceedings of the Design, Automation & Test in Europe Conference & Exhibition, 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
IEEE Trans. Emerg. Top. Comput., 2020
IEEE Trans. Comput. Aided Des. Integr. Circuits Syst., 2020
Proceedings of the ESEC/FSE '20: 28th ACM Joint European Software Engineering Conference and Symposium on the Foundations of Software Engineering, 2020
Proceedings of the 23rd GMM/ITG/GI Workshop on Methods and Description Languages for Modelling and Verification of Circuits and Systems, 2020
Proceedings of the 23rd Euromicro Conference on Digital System Design, 2020
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
Proceedings of the 22nd Workshop Methods and Description Languages for Modelling and Verification of Circuits and Systems, 2019
Proceedings of the 22nd Workshop Methods and Description Languages for Modelling and Verification of Circuits and Systems, 2019
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
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
Proceedings of the 35th IEEE VLSI Test Symposium, 2017
Dynamic Power Optimization based on Formal Property Checking of Operations.
Proceedings of the Methoden und Beschreibungssprachen zur Modellierung und Verifikation von Schaltungen und Systemen, 2017
Speculative disassembly of binary code.
Proceedings of the Methoden und Beschreibungssprachen zur Modellierung und Verifikation von Schaltungen und Systemen, 2017
Proceedings of the 2017 Formal Methods in Computer Aided Design, 2017
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
Proceedings of the 19th GI/ITG/GMM Workshop Methoden und Beschreibungssprachen zur Modellierung und Verifikation von Schaltungen und Systemen, 2016
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
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
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
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
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
Proof Logging for Computer Algebra based SMT Solving.
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
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
Proceedings of the Models, Methods, and Tools for Complex Chip Design, 2012
System verification of concurrent RTL modules by compositional path predicate abstraction.
Proceedings of the 49th Annual Design Automation Conference 2012, 2012
2011
Proceedings of the 22nd IEEE International Symposium on Rapid System Prototyping, 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
STABLE: A new QF-BV SMT solver for hard verification problems combining Boolean reasoning with computer algebra.
Proceedings of the Design, Automation and Test in Europe, 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
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
Proceedings of the Forum on specification and Design Languages, 2009
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
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
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
Proceedings of the 42nd Design Automation Conference, 2005
2004
IEEE Trans. Comput. Aided Des. Integr. Circuits Syst., 2004
IEEE Trans. Comput. Aided Des. Integr. Circuits Syst., 2004
Layout Driven Optimization of Datapath Circuits using Arithmetic Reasoning.
Proceedings of the Methoden und Beschreibungssprachen zur Modellierung und Verifikation von Schaltungen und Systemen (MBMV), 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
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
Proceedings of the 2002 IEEE Computer Society Annual Symposium on VLSI (ISVLSI 2002), 2002
Proceedings of the 2002 IEEE Computer Society Annual Symposium on VLSI (ISVLSI 2002), 2002
Proceedings of the 2002 IEEE/ACM International Conference on Computer-aided Design, 2002
Proceedings of the 2002 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
Proceedings of the 2001 International Symposium on Physical Design, 2001
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
Proceedings of the 2001 IEEE/ACM International Conference on Computer-Aided Design, 2001
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
Proceedings of the Field-Programmable Logic and Applications, 9th International Workshop, 1999
1998
IEEE Trans. Comput. Aided Des. Integr. Circuits Syst., 1998
1997
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
IEEE Trans. Comput. Aided Des. Integr. Circuits Syst., 1996
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
Proceedings of the 1994 IEEE/ACM International Conference on Computer-Aided Design, 1994
1993
IEEE Trans. Comput. Aided Des. Integr. Circuits Syst., 1993
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