Improving Structural FSM Traversal by Constraint-Satisfying Logic Simulation. - Markus Wedler; Dominik Stoffel; Wolfgang Kunz (ISVLSI, 2002)

Using RTL Statespace Information and State Encoding for Induction Based Property Checking. - Markus Wedler; Dominik Stoffel; Wolfgang Kunz (DATE, 2003)

Towards the impact of state encoding on induction-based property checking. - Markus Wedler; Dominik Stoffel; Wolfgang Kunz (MBMV, 2003)

Exploiting state encoding for invariant generation in induction-based property checking. - Markus Wedler; Dominik Stoffel; Wolfgang Kunz (ASP-DAC, 2004)

Arithmetic Reasoning in DPLL-Based SAT Solving. - Markus Wedler; Dominik Stoffel; Wolfgang Kunz (DATE, 2004)

Structural FSM traversal. - Dominik Stoffel; Markus Wedler; Peter Warkentin; Wolfgang Kunz (IEEE Trans. Comput. Aided Des. Integr. Circuits Syst., 2004)

Normalization at the arithmetic bit level. - Markus Wedler; Dominik Stoffel; Wolfgang Kunz (DAC, 2005)

Transition-by-transition FSM traversal for reachability analysis in bounded model checking. - Minh D. Nguyen; Dominik Stoffel; Markus Wedler; Wolfgang Kunz (ICCAD, 2005)

A case study on applying bounded model checking to analog circuit verification. - Alexander Jesser; Markus Wedler; Lars Hedrich; Wolfgang Kunz (MBMV, 2006)

Arithmetic Constraints in SAT-based Property Checking. - Evgeny Pavlenko; Markus Wedler; Dominik Stoffel; Wolfgang Kunz (MBMV, 2007)

A Normalization Method for Arithmetic Data-Path Verification. - Markus Wedler; Dominik Stoffel; Raik Brinkmann; Wolfgang Kunz (IEEE Trans. Comput. Aided Des. Integr. Circuits Syst., 2007)

Verifying full-custom multipliers by Boolean equivalence checking and an arithmetic bit level proof. - Udo Krautz; Markus Wedler; Wolfgang Kunz; Kai Weber 001; Christian Jacobi 002; Matthias Pflanz (ASP-DAC, 2008)

An Algebraic Approach for Proving Data Correctness in Arithmetic Data Paths. - Oliver Wienand; Markus Wedler; Dominik Stoffel; Wolfgang Kunz; Gert-Martin Greuel (CAV, 2008)

A New Verification Technique for Custom-Designed Components at the Arithmetic Bit Level. - Evgeny Pavlenko; Markus Wedler; Dominik Stoffel; Wolfgang Kunz; Oliver Wienand; Evgeny Karibaev (FDL (Selected Papers), 2008)

Modeling of Custom-Designed Arithmetic Components for ABL Normalization. - Evgeny Pavlenko; Markus Wedler; Dominik Stoffel; Wolfgang Kunz; Oliver Wienand; Evgeny Karibaev (MBMV, 2008)

Formale Verifikation einer Hardware-Implementierung des LIN-Protokoll Kontrollers. - Bernard Schmidt; Slava Bulach; Katharina Weinberger; Markus Wedler (MBMV, 2008)

Proving Functional Correctness of Weakly Programmable IPs - A Case Study with Formal Property Checking. - Sacha Loitz; Markus Wedler; Christian Brehm; Timo Vogt; Norbert Wehn; Wolfgang Kunz (SASP, 2008)

Unbounded Protocol Compliance Verification Using Interval Property Checking With Invariants. - Minh D. Nguyen; Max Thalmaier; Markus Wedler; Jörg Bormann; Dominik Stoffel; Wolfgang Kunz (IEEE Trans. Comput. Aided Des. Integr. Circuits Syst., 2008)

Solving hard instances in QF-BV combining Boolean reasoning with computer algebra. - Markus Wedler; Evgeny Pavlenko; Alexander Dreyer; Frank Seelisch; Dominik Stoffel; Gert-Martin Greuel; Wolfgang Kunz (Algorithms and Applications for Next Generation SAT Solvers, 2009)

A re-use methodology for formal SoC protocol compliance verification. - Minh D. Nguyen; Max Thalmaier; Markus Wedler; Dominik Stoffel; Wolfgang Kunz; Jörg Bormann (FDL, 2009)

A Re-Use Methodology for SoC Protocol Compliance Verification. - Minh D. Nguyen; Max Thalmaier; Markus Wedler; Dominik Stoffel; Wolfgang Kunz (MBMV, 2009)

Analyzing k-step induction to compute invariants for SAT-based property checking. - Max Thalmaier; Minh D. Nguyen; Markus Wedler; Dominik Stoffel; Jörg Bormann; Wolfgang Kunz (DAC, 2010)

Complete Verification of Weakly Programmable IPs against Their Operational ISA Model. - Sacha Loitz; Markus Wedler; Dominik Stoffel; Christian Brehm; Norbert Wehn; Wolfgang Kunz (FDL, 2010)

Path predicate abstraction by complete interval property checking. - Joakim Urdahl; Dominik Stoffel; Jörg Bormann; Markus Wedler; Wolfgang Kunz (FMCAD, 2010)

Analyzing k-step induction to compute invariants for SAT-based property checking. - Max Thalmaier; Minh D. Nguyen; Markus Wedler; Dominik Stoffel; Wolfgang Kunz (MBMV, 2010)

Formal hardware/software co-verification by interval property checking with abstraction. - Minh D. Nguyen; Markus Wedler; Dominik Stoffel; Wolfgang Kunz (DAC, 2011)

Formal Hardware/Software Co-Verification by Interval Property Checking with Abstraction. - Minh D. Nguyen; Markus Wedler; Bernard Schmidt; Dominik Stoffel; Wolfgang Kunz (MBMV, 2011)

STABLE: A new QF-BV SMT Solver for hard Verification Problems combining Boolean Reasoning with Computer Algebra. - Evgeny Pavlenko; Markus Wedler; Dominik Stoffel; Wolfgang Kunz; Alexander Dreyer; Frank Seelisch; Gert-Martin Greuel (MBMV, 2011)

System verification of concurrent RTL modules by compositional path predicate abstraction. - Joakim Urdahl; Dominik Stoffel; Markus Wedler; Wolfgang Kunz (DAC, 2012)

Formal plausibility checks for environment constraints. - Binghao Bao; Jörg Bormann; Markus Wedler; Dominik Stoffel; Wolfgang Kunz (FDL, 2012)

A computational model for SAT-based verification of hardware-dependent low-level embedded system software. - Bernard Schmidt; Carlos Villarraga; Jörg Bormann; Dominik Stoffel; Markus Wedler; Wolfgang Kunz (ASP-DAC, 2013)

Proof logging for computer algebra based SMT solving. - Oliver Marx; Markus Wedler; Dominik Stoffel; Wolfgang Kunz; Alexander Dreyer (ICCAD, 2013)

Compositional Completeness over reactive Constraints. - Binghao Bao; Jörg Bormann; Markus Wedler; Dominik Stoffel; Wolfgang Kunz (MBMV, 2013)

A New Formal Verification Approach for Hardware-dependent Embedded System Software. - Bernard Schmidt; Carlos Villarraga; Thomas Fehmel; Jörg Bormann; Markus Wedler; Minh D. Nguyen; Dominik Stoffel; Wolfgang Kunz (IPSJ Trans. Syst. LSI Des. Methodol., 2013)

Coverage of compositional property sets under reactive constraints. - Binghao Bao; Jörg Bormann; Markus Wedler; Dominik Stoffel; Wolfgang Kunz (ISQED, 2014)

Virtual hardware-in-the-loop co-simulation for multi-domain automotive systems via the functional mock-up interface. - Robert Lajos Bücs; Luis Gabriel Murillo; Ekaterina Korotcenko; Gaurav Dugge; Rainer Leupers; Gerd Ascheid; Andreas Ropers; Markus Wedler; Andreas Hoffmann 002 (FDL, 2015)