Communication based multilevel synthesis for multi-output Boolean functions. - Paul Molitor; Christoph Scholl 001 (Great Lakes Symposium on VLSI, 1994)

Communication based FPGA synthesis for multi-output Boolean functions. - Christoph Scholl 001; Paul Molitor (ASP-DAC, 1995)

Minimizing ROBDD sizes of incompletely specified Boolean functionsby exploiting strong symmetries. - Christoph Scholl 001; S. Melchior; Günter Hotz; Paul Molitor (ED&TC, 1997)

Functional simulation using binary decision diagrams. - Christoph Scholl 001; Rolf Drechsler; Bernd Becker 001 (ICCAD, 1997)

Mehrstufige Logiksynthese unter Ausnutzung funktionaler Eigenschaften. - Christoph Scholl 001 (1997)

Multi-output Functional Decomposition with Exploitation of Don't Cares. - Christoph Scholl 001 (DATE, 1998)

Word-level decision diagrams, WLCDs and division. - Christoph Scholl 001; Bernd Becker 001; Thomas M. Weis (ICCAD, 1998)

Datenstrukturen und effiziente Algorithmen für die Logiksynthese kombinatorischer Schaltungen. - Paul Molitor; Christoph Scholl 001 (Teubner, 1999)

BDD minimization using symmetries. - Christoph Scholl 001; Dirk Möller; Paul Molitor; Rolf Drechsler (IEEE Trans. Comput. Aided Des. Integr. Circuits Syst., 1999)

Distance driven finite state machine traversal. - Andreas Hett; Christoph Scholl 001; Bernd Becker 001 (DAC, 2000)

On the Generation of Multiplexer Circuits for Pass Transistor Logic. - Christoph Scholl 001; Bernd Becker 001 (DATE, 2000)

State Traversal guided by Hamming Distance Profiles. - Andreas Hett; Christoph Scholl 001; Bernd Becker 001 (MBMV, 2000)

Functional decomposition with applications to FPGA synthesis. - Christoph Scholl 001 (Kluwer, 2001)

The multiple variable order problem for binary decision diagrams: theory and practical application. - Christoph Scholl 001; Bernd Becker 001; Andreas Brogle (ASP-DAC, 2001)

Exploiting don't cares to minimize *BMDs. - Christoph Scholl 001; Marc Herbstritt; Bernd Becker 001 (ISCAS (5), 2001)

Checking Equivalence for Partial Implementations. - Christoph Scholl 001; Bernd Becker 001 (MBMV (1), 2001)

Don't Care Minimization of BMDs: Complexity and Algorithms. - Christoph Scholl 001; Marc Herbstritt; Bernd Becker 001 (MBMV (1), 2001)

Checking Equivalence for Circuits Containing Incompletely Specified Boxes. - Christoph Scholl 001; Bernd Becker 001 (ICCD, 2002)

Equivalence Checking in the Presence of Incompletely Specified Boxes. - Christoph Scholl 001; Bernd Becker 001 (MBMV, 2002)

On WLCDs and the Complexity of Word-Level Decision Diagrams-A Lower Bound for Division. - Christoph Scholl 001; Bernd Becker 001; Thomas M. Weis (Formal Methods Syst. Des., 2002)

Approximate Symbolic Model Checking for Incomplete Designs. - Tobias Nopper; Christoph Scholl 001 (FMCAD, 2004)

Filter Based Diagnosis for Multiple Design Errors. - Christoph Scholl 001; Matthias Büche (MBMV, 2004)

Automatic Verification of Hybrid Systems with Large Discrete State Space. - Werner Damm; Stefan Disch; Hardi Hungar; Jun Pang 001; Florian Pigorsch; Christoph Scholl 001; Uwe Waldmann; Boris Wirtz (ATVA, 2006)

Advanced Unbounded Model Checking Based on AIGs, BDD Sweeping, And Quantifier Scheduling. - Florian Pigorsch; Christoph Scholl 001; Stefan Disch (FMCAD, 2006)

Advanced Unbounded CTL Model Checking By Using AIGs, BDD Sweeping, and Quantifier Scheduling. - Florian Pigorsch; Christoph Scholl 001; Stefan Disch (MBMV, 2006)

Advanced SAT-Techniques for Bounded Model Checking of Blackbox Designs. - Marc Herbstritt; Bernd Becker 001; Christoph Scholl 001 (MTV, 2006)

Combinational Equivalence Checking Using Incremental SAT Solving, Output Ordering, and Resets. - Stefan Disch; Christoph Scholl 001 (ASP-DAC, 2007)

Exact State Set Representations in the Verification of Linear Hybrid Systems with Large Discrete State Space. - Werner Damm; Stefan Disch; Hardi Hungar; Swen Jacobs; Jun Pang 001; Florian Pigorsch; Christoph Scholl 001; Uwe Waldmann; Boris Wirtz (ATVA, 2007)

Towards an Experimental Autonomous Blimp Platform. - Axel Rottmann; Matthias Sippel; Thorsten Zitterell; Wolfram Burgard; Leonhard M. Reindl; Christoph Scholl 001 (EMCR, 2007)

Computation of minimal counterexamples by using black box techniques and symbolic methods. - Tobias Nopper; Christoph Scholl 001; Bernd Becker 001 (ICCAD, 2007)

Counterexample Generation for Incomplete Designs. - Tobias Nopper; Christoph Scholl 001 (MBMV, 2007)

Improving energy-efficient real-time scheduling by exploiting code instrumentation. - Thorsten Zitterell; Christoph Scholl 001 (IMCSIT, 2008)

Dynamische Verwaltung Virtuellen Speichers für Echtzeitsysteme. - Martin Böhnert; Thorsten Zitterell; Christoph Scholl 001 (Echtzeit, 2008)

Exploiting structure in an AIG based QBF solver. - Florian Pigorsch; Christoph Scholl 001 (DATE, 2009)

Symbolic CTL Model Checking for Incomplete Designs by Selecting Property-Specific Subsets of Local Component Assumptions. - Christian Miller; Tobias Nopper; Christoph Scholl 001 (MBMV, 2009)

Using Implications for Optimizing State Set Representations of Linear Hybrid Systems. - Florian Pigorsch; Christoph Scholl 001 (MBMV, 2009)

Computing Optimized Representations for Non-convex Polyhedra by Detection and Removal of Redundant Linear Constraints. - Christoph Scholl 001; Stefan Disch; Florian Pigorsch; Stefan Kupferschmid (TACAS, 2009)

An AIG-Based QBF-solver using SAT for preprocessing. - Florian Pigorsch; Christoph Scholl 001 (DAC, 2010)

A probabilistic and energy-efficient scheduling approach for online application in real-time systems. - Thorsten Zitterell; Christoph Scholl 001 (DAC, 2010)

SAT Modulo BDD – A Combined Verification Approach for Incomplete Designs. - Tobias Nopper; Christian Miller; Matthew Lewis 004; Bernd Becker 001; Christoph Scholl 001 (MBMV, 2010)

Bounded Model Checking of Incomplete Networks of Timed Automata. - Christian Miller; Karina Gitina; Christoph Scholl 001; Bernd Becker 001 (MTV, 2010)

Fully Symbolic Model Checking for Timed Automata. - Georges Morbé; Florian Pigorsch; Christoph Scholl 001 (CAV, 2011)

Integration of orthogonal QBF solving techniques. - Sven Reimer; Florian Pigorsch; Christoph Scholl 001; Bernd Becker 001 (DATE, 2011)

Verifying Incomplete Networks of Timed Automata. - Christian Miller; Christoph Scholl 001; Bernd Becker 001 (MBMV, 2011)

Fully Symbolic Model Checking for Timed Automata. - Georges Morbé; Christoph Scholl 001 (MBMV, 2011)

Fully Symbolic Model Checking for Incomplete Systems of Timed Automata. - Georges Morbé; Christoph Scholl 001 (MBMV, 2012)

Enhanced Integration of QBF Solving Techniques. - Sven Reimer; Florian Pigorsch; Christoph Scholl 001; Bernd Becker 001 (MBMV, 2012)

Guaranteeing Termination of Fully Symbolic Timed Forward Model Checking. - Georges Morbé; Christoph Scholl 001 (MTV, 2012)

Exact and fully symbolic verification of linear hybrid automata with large discrete state spaces. - Werner Damm; Henning Dierks; Stefan Disch; Willem Hagemann; Florian Pigorsch; Christoph Scholl 001; Uwe Waldmann; Boris Wirtz (Sci. Comput. Program., 2012)

Lemma localization: a practical method for downsizing SMT-interpolants. - Florian Pigorsch; Christoph Scholl 001 (DATE, 2013)

Equivalence checking of partial designs using dependency quantified Boolean formulae. - Karina Gitina; Sven Reimer; Matthias Sauer 002; Ralf Wimmer 001; Christoph Scholl 001; Bernd Becker 001 (ICCD, 2013)

Equivalence Checking for Partial Implementations Revisited. - Karina Gitina; Sven Reimer; Matthias Sauer 002; Ralf Wimmer 001; Christoph Scholl 001; Bernd Becker 001 (MBMV, 2013)

Proving QBF-hardness in Bounded Model Checking for Incomplete Designs. - Christian Miller; Christoph Scholl 001; Bernd Becker 001 (MTV, 2013)

Fully Symbolic TCTL Model Checking for Incomplete Timed Systems. - Georges Morbé; Christoph Scholl 001 (Electron. Commun. Eur. Assoc. Softw. Sci. Technol., 2013)

Symbolic Model Checking for Incomplete Designs with Flexible Modeling of Unknowns. - Tobias Nopper; Christoph Scholl 001 (IEEE Trans. Computers, 2013)

Simple interpolants for linear arithmetic. - Christoph Scholl 001; Florian Pigorsch; Stefan Disch; Ernst Althaus (DATE, 2014)

Combined Bounded and Symbolic Model Checking for Incomplete Timed Systems. - Georges Morbé; Christian Miller; Christoph Scholl 001; Bernd Becker 001 (Haifa Verification Conference, 2014)

A dynamic virtual memory management under real-time constraints. - Martin Böhnert; Christoph Scholl 001 (RTCSA, 2014)

Improving Interpolants for Linear Arithmetic. - Ernst Althaus; Björn Beber; Joschka Kupilas; Christoph Scholl 001 (ATVA, 2015)

Solving DQBF through quantifier elimination. - Karina Gitina; Ralf Wimmer 001; Sven Reimer; Matthias Sauer 002; Christoph Scholl 001; Bernd Becker 001 (DATE, 2015)

Preprocessing for DQBF. - Ralf Wimmer 001; Karina Gitina; Jennifer Nist; Christoph Scholl 001; Bernd Becker 001 (SAT, 2015)

Modeling Unknown Values in Test and Verification. - Bernd Becker 001; Matthias Sauer 002; Christoph Scholl 001; Ralf Wimmer 001 (SyDe Summer School, 2015)

Fully symbolic TCTL model checking for complete and incomplete real-time systems. - Georges Morbé; Christoph Scholl 001 (Sci. Comput. Program., 2015)

Clauses Versus Gates in CEGAR-Based 2QBF Solving. - Valeriy Balabanov; Jie-Hong Roland Jiang; Alan Mishchenko; Christoph Scholl 001 (AAAI Workshop: Beyond NP, 2016)

Task Variants with Different Scratchpad Memory Consumption in Multi-Task Environments. - Martin Böhnert; Christoph Scholl 001 (ARCS, 2016)

Skolem Functions for DQBF. - Karina Wimmer; Ralf Wimmer 001; Christoph Scholl 001; Bernd Becker 001 (ATVA, 2016)

2QBF: Challenges and Solutions. - Valeriy Balabanov; Jie-Hong Roland Jiang; Christoph Scholl 001; Alan Mishchenko; Robert K. Brayton (SAT, 2016)

The QBF Solver AIGSolve. - Christoph Scholl 001; Florian Pigorsch (QBF@SAT, 2016)

Dependency Schemes for DQBF. - Ralf Wimmer 001; Christoph Scholl 001; Karina Wimmer; Bernd Becker 001 (SAT, 2016)

Sequential Verification Using Reverse PDR. - Tobias Seufert; Christoph Scholl 001 (MBMV, 2017)

Verification of linear hybrid systems with large discrete state spaces using counterexample-guided abstraction refinement. - Ernst Althaus; Björn Beber; Werner Damm; Stefan Disch; Willem Hagemann; Astrid Rakow; Christoph Scholl 001; Uwe Waldmann; Boris Wirtz (Sci. Comput. Program., 2017)

Analysis of Incomplete Circuits Using Dependency Quantified Boolean Formulas. - Ralf Wimmer 001; Karina Wimmer; Christoph Scholl 001; Bernd Becker 001 (Advanced Logic Synthesis, 2018)

Combining PDR and reverse PDR for hardware model checking. - Tobias Seufert; Christoph Scholl 001 (DATE, 2018)

From DQBF to QBF by Dependency Elimination. - Ralf Wimmer 001; Andreas Karrenbauer; Ruben Becker; Christoph Scholl 001; Bernd Becker 001 (MBMV, 2018)

Dependency Quantified Boolean Formulas: An Overview of Solution Methods and Applications - Extended Abstract. - Christoph Scholl 001; Ralf Wimmer 001 (SAT, 2018)

A PSPACE Subclass of Dependency Quantified Boolean Formulas and Its Effective Solving. - Christoph Scholl 001; Jie-Hong Roland Jiang; Ralf Wimmer 001; Aile Ge-Ernst (AAAI, 2019)

fbPDR: In-depth combination of forward and backward analysis in Property Directed Reachability. - Tobias Seufert; Christoph Scholl 001 (DATE, 2019)

Localizing Quantifiers for DQBF. - Aile Ge-Ernst; Christoph Scholl 001; Ralf Wimmer 001 (FMCAD, 2019)

Incremental Inprocessing in SAT Solving. - Katalin Fazekas; Armin Biere; Christoph Scholl 001 (SAT, 2019)

Quantifier Localization for DQBF. - Aile Ge-Ernst; Christoph Scholl 001; Ralf Wimmer 001 (CoRR, 2019)

The (D)QBF Preprocessor HQSpre - Underlying Theory and Its Implementation. - Ralf Wimmer 001; Christoph Scholl 001; Bernd Becker 001 (J. Satisf. Boolean Model. Comput., 2019)

Symbolic Computer Algebra and SAT Based Information Forwarding for Fully Automatic Divider Verification. - Christoph Scholl 001; Alexander Konrad (DAC, 2020)

Towards Formal Verification of Optimized and Industrial Multipliers. - Alireza Mahzoon; Daniel Große; Christoph Scholl 001; Rolf Drechsler (DATE, 2020)

ICP and IC3. - Karsten Scheibler; Felix Winterer; Tobias Seufert; Tino Teige; Christoph Scholl 001; Bernd Becker 001 (DATE, 2021)

Verifying Dividers Using Symbolic Computer Algebra and Don't Care Optimization. - Christoph Scholl 001; Alexander Konrad; Alireza Mahzoon; Daniel Große; Rolf Drechsler (DATE, 2021)

Formal verification of modular multipliers using symbolic computer algebra and boolean satisfiability. - Alireza Mahzoon; Daniel Große; Christoph Scholl 001; Alexander Konrad; Rolf Drechsler (DAC, 2022)

Divider Verification Using Symbolic Computer Algebra and Delayed Don't Care Optimization. - Alexander Konrad; Christoph Scholl 001; Alireza Mahzoon; Daniel Große; Rolf Drechsler (FMCAD, 2022)

Quantifier Elimination in Stochastic Boolean Satisfiability. - Hao-Ren Wang; Kuan-Hua Tu; Jie-Hong Roland Jiang; Christoph Scholl 001 (SAT, 2022)

Making PROGRESS in Property Directed Reachability. - Tobias Seufert; Christoph Scholl 001; Arun Chandrasekharan; Sven Reimer; Tobias Welp (VMCAI, 2022)

Solving dependency quantified Boolean formulas using quantifier localization. - Aile Ge-Ernst; Christoph Scholl 001; Juraj Síc; Ralf Wimmer 001 (Theor. Comput. Sci., 2022)

Everything You Always Wanted to Know About Generalization of Proof Obligations in PDR. - Tobias Seufert; Felix Winterer; Christoph Scholl 001; Karsten Scheibler; Tobias Paxian; Bernd Becker 001 (IEEE Trans. Comput. Aided Des. Integr. Circuits Syst., 2023)

Symbolic Computer Algebra for Multipliers Revisited - It's All About Orders and Phases. - Alexander Konrad; Christoph Scholl 001 (FMCAD, 2024)

Hierarchical Stochastic SAT and Quality Assessment of Logic Locking. - Christoph Scholl 001; Tobias Seufert; Fabian Siegwolf (SAT, 2024)

Divider verification using symbolic computer algebra and delayed don't care optimization: theory and practical implementation. - Alexander Konrad; Christoph Scholl 001; Alireza Mahzoon; Daniel Große; Rolf Drechsler (Formal Methods Syst. Des., 2025)