Christoph Scholl

101 papers A* 8A 24B 12C 2Journal 14Unranked 36

Year	Rank	Type	Title / Venue / Authors
2026	J	`jnl`	Symbolic computer algebra for multipliers revisited - demonstrating the significance of order and phase optimization. Formal Methods Syst. Des. Alexander Konrad, Christoph Scholl
2025	J	`jnl`	Divider verification using symbolic computer algebra and delayed don't care optimization: theory and practical implementation. Formal Methods Syst. Des. Alexander Konrad, Christoph Scholl, Alireza Mahzoon, Daniel Große, Rolf Drechsler
2025	B	`conf`	FastPoly: An Efficient Polynomial Package for the Verification of Integer Arithmetic Circuits. FMCAD Alexander Konrad, Christoph Scholl
2024	A	`conf`	Hierarchical Stochastic SAT and Quality Assessment of Logic Locking. SAT Christoph Scholl, Tobias Seufert, Fabian Siegwolf
2024	B	`conf`	Symbolic Computer Algebra for Multipliers Revisited - It's All About Orders and Phases. FMCAD Alexander Konrad, Christoph Scholl
2023	J	`jnl`	Everything You Always Wanted to Know About Generalization of Proof Obligations in PDR. IEEE Trans. Comput. Aided Des. Integr. Circuits Syst. Tobias Seufert, Felix Winterer, Christoph Scholl, Karsten Scheibler, Tobias Paxian, Bernd Becker
2022	B	`conf`	Divider Verification Using Symbolic Computer Algebra and Delayed Don't Care Optimization. FMCAD Alexander Konrad, Christoph Scholl, Alireza Mahzoon, Daniel Große, Rolf Drechsler
2022	A*	`conf`	Formal verification of modular multipliers using symbolic computer algebra and boolean satisfiability. DAC Alireza Mahzoon, Daniel Große, Christoph Scholl, Alexander Konrad, Rolf Drechsler
2022	—	`conf`	Making PROGRESS in Property Directed Reachability. MBMV Tobias Seufert, Christoph Scholl, Arun Chandrasekharan, Sven Reimer, Tobias Welp
2022	B	`conf`	Making PROGRESS in Property Directed Reachability. VMCAI Tobias Seufert, Christoph Scholl, Arun Chandrasekharan, Sven Reimer, Tobias Welp
2022	A	`conf`	Quantifier Elimination in Stochastic Boolean Satisfiability. SAT Hao-Ren Wang, Kuan-Hua Tu, Jie-Hong Roland Jiang, Christoph Scholl
2022	J	`jnl`	Solving dependency quantified Boolean formulas using quantifier localization. Theor. Comput. Sci. Aile Ge-Ernst, Christoph Scholl, Juraj Síc, Ralf Wimmer
2021	J	`jnl`	Everything You Always Wanted to Know About Generalization of Proof Obligations in PDR. CoRR Tobias Seufert, Felix Winterer, Christoph Scholl, Karsten Scheibler, Tobias Paxian, Bernd Becker
2021	A	`conf`	ICP and IC3. DATE Karsten Scheibler, Felix Winterer, Tobias Seufert, Tino Teige, Christoph Scholl, Bernd Becker
2021	A	`conf`	Verifying Dividers Using Symbolic Computer Algebra and Don't Care Optimization. DATE Christoph Scholl, Alexander Konrad, Alireza Mahzoon, Daniel Große, Rolf Drechsler
2020	A*	`conf`	Symbolic Computer Algebra and SAT Based Information Forwarding for Fully Automatic Divider Verification. DAC Christoph Scholl, Alexander Konrad
2020	A	`conf`	Towards Formal Verification of Optimized and Industrial Multipliers. DATE Alireza Mahzoon, Daniel Große, Christoph Scholl, Rolf Drechsler
2019	A*	`conf`	A PSPACE Subclass of Dependency Quantified Boolean Formulas and Its Effective Solving. AAAI Christoph Scholl, Jie-Hong Roland Jiang, Ralf Wimmer, Aile Ge-Ernst
2019	A	`conf`	Incremental Inprocessing in SAT Solving. SAT Katalin Fazekas, Armin Biere, Christoph Scholl
2019	B	`conf`	Localizing Quantifiers for DQBF. FMCAD Aile Ge-Ernst, Christoph Scholl, Ralf Wimmer
2019	J	`jnl`	Quantifier Localization for DQBF. CoRR Aile Ge-Ernst, Christoph Scholl, Ralf Wimmer
2019	J	`jnl`	The (D)QBF Preprocessor HQSpre - Underlying Theory and Its Implementation. J. Satisf. Boolean Model. Comput. Ralf Wimmer, Christoph Scholl, Bernd Becker
2019	A	`conf`	fbPDR: In-depth combination of forward and backward analysis in Property Directed Reachability. DATE Tobias Seufert, Christoph Scholl
2018	—	`ch.`	Analysis of Incomplete Circuits Using Dependency Quantified Boolean Formulas. Advanced Logic Synthesis Ralf Wimmer, Karina Wimmer, Christoph Scholl, Bernd Becker
2018	A	`conf`	Combining PDR and reverse PDR for hardware model checking. DATE Tobias Seufert, Christoph Scholl
2018	A	`conf`	Dependency Quantified Boolean Formulas: An Overview of Solution Methods and Applications - Extended Abstract. SAT Christoph Scholl, Ralf Wimmer
2018	—	`conf`	From DQBF to QBF by Dependency Elimination. MBMV Ralf Wimmer, Andreas Karrenbauer, Ruben Becker, Christoph Scholl, Bernd Becker
2017	A	`conf`	From DQBF to QBF by Dependency Elimination. SAT Ralf Wimmer, Andreas Karrenbauer, Ruben Becker, Christoph Scholl, Bernd Becker
2017	—	`conf`	Sequential Verification Using Reverse PDR. MBMV Tobias Seufert, Christoph Scholl
2017	J	`jnl`	Verification of linear hybrid systems with large discrete state spaces using counterexample-guided abstraction refinement. Sci. Comput. Program. Ernst Althaus, Björn Beber, Werner Damm, Stefan Disch, Willem Hagemann, Astrid Rakow, Christoph Scholl, Uwe Waldmann, Boris Wirtz
2016	A	`conf`	2QBF: Challenges and Solutions. SAT Valeriy Balabanov, Jie-Hong Roland Jiang, Christoph Scholl, Alan Mishchenko, Robert K. Brayton
2016	—	`conf`	Clauses Versus Gates in CEGAR-Based 2QBF Solving. AAAI Workshop: Beyond NP Valeriy Balabanov, Jie-Hong Roland Jiang, Alan Mishchenko, Christoph Scholl
2016	A	`conf`	Dependency Schemes for DQBF. SAT Ralf Wimmer, Christoph Scholl, Karina Wimmer, Bernd Becker
2016	B	`conf`	Skolem Functions for DQBF. ATVA Karina Wimmer, Ralf Wimmer, Christoph Scholl, Bernd Becker
2016	—	`conf`	Task Variants with Different Scratchpad Memory Consumption in Multi-Task Environments. ARCS Martin Böhnert, Christoph Scholl
2016	—	`conf`	The QBF Solver AIGSolve. QBF@SAT Christoph Scholl, Florian Pigorsch
2015	J	`jnl`	Fully symbolic TCTL model checking for complete and incomplete real-time systems. Sci. Comput. Program. Georges Morbé, Christoph Scholl
2015	B	`conf`	Improving Interpolants for Linear Arithmetic. ATVA Ernst Althaus, Björn Beber, Joschka Kupilas, Christoph Scholl
2015	—	`conf`	Modeling Unknown Values in Test and Verification. SyDe Summer School Bernd Becker, Matthias Sauer, Christoph Scholl, Ralf Wimmer
2015	A	`conf`	Preprocessing for DQBF. SAT Ralf Wimmer, Karina Gitina, Jennifer Nist, Christoph Scholl, Bernd Becker
2015	A	`conf`	Solving DQBF through quantifier elimination. DATE Karina Gitina, Ralf Wimmer, Sven Reimer, Matthias Sauer, Christoph Scholl, Bernd Becker
2014	B	`conf`	A dynamic virtual memory management under real-time constraints. RTCSA Martin Böhnert, Christoph Scholl
2014	—	`conf`	Combined Bounded and Symbolic Model Checking for Incomplete Timed Systems. Haifa Verification Conference Georges Morbé, Christian Miller, Christoph Scholl, Bernd Becker
2014	A	`conf`	Simple interpolants for linear arithmetic. DATE Christoph Scholl, Florian Pigorsch, Stefan Disch, Ernst Althaus
2013	—	`conf`	Equivalence Checking for Partial Implementations Revisited. MBMV Karina Gitina, Sven Reimer, Matthias Sauer, Ralf Wimmer, Christoph Scholl, Bernd Becker
2013	C	`conf`	Equivalence checking of partial designs using dependency quantified Boolean formulae. ICCD Karina Gitina, Sven Reimer, Matthias Sauer, Ralf Wimmer, Christoph Scholl, Bernd Becker
2013	J	`jnl`	Fully Symbolic TCTL Model Checking for Incomplete Timed Systems. Electron. Commun. Eur. Assoc. Softw. Sci. Technol. Georges Morbé, Christoph Scholl
2013	A	`conf`	Lemma localization: a practical method for downsizing SMT-interpolants. DATE Florian Pigorsch, Christoph Scholl
2013	—	`conf`	Proving QBF-hardness in Bounded Model Checking for Incomplete Designs. MTV Christian Miller, Christoph Scholl, Bernd Becker
2013	J	`jnl`	Symbolic Model Checking for Incomplete Designs with Flexible Modeling of Unknowns. IEEE Trans. Computers Tobias Nopper, Christoph Scholl
2012	—	`conf`	Enhanced Integration of QBF Solving Techniques. MBMV Sven Reimer, Florian Pigorsch, Christoph Scholl, Bernd Becker
2012	J	`jnl`	Exact and fully symbolic verification of linear hybrid automata with large discrete state spaces. Sci. Comput. Program. Werner Damm, Henning Dierks, Stefan Disch, Willem Hagemann, Florian Pigorsch, Christoph Scholl, Uwe Waldmann, Boris Wirtz
2012	—	`conf`	Fully Symbolic Model Checking for Incomplete Systems of Timed Automata. MBMV Georges Morbé, Christoph Scholl
2012	—	`conf`	Guaranteeing Termination of Fully Symbolic Timed Forward Model Checking. MTV Georges Morbé, Christoph Scholl
2011	A*	`conf`	Fully Symbolic Model Checking for Timed Automata. CAV Georges Morbé, Florian Pigorsch, Christoph Scholl
2011	—	`conf`	Fully Symbolic Model Checking for Timed Automata. MBMV Georges Morbé, Christoph Scholl
2011	A	`conf`	Integration of orthogonal QBF solving techniques. DATE Sven Reimer, Florian Pigorsch, Christoph Scholl, Bernd Becker
2011	—	`conf`	Verifying Incomplete Networks of Timed Automata. MBMV Christian Miller, Christoph Scholl, Bernd Becker
2010	A*	`conf`	A probabilistic and energy-efficient scheduling approach for online application in real-time systems. DAC Thorsten Zitterell, Christoph Scholl
2010	A*	`conf`	An AIG-Based QBF-solver using SAT for preprocessing. DAC Florian Pigorsch, Christoph Scholl
2010	—	`conf`	Bounded Model Checking of Incomplete Networks of Timed Automata. MTV Christian Miller, Karina Gitina, Christoph Scholl, Bernd Becker
2010	—	`conf`	SAT Modulo BDD -- A Combined Verification Approach for Incomplete Designs. MBMV Tobias Nopper, Christian Miller, Matthew Lewis, Bernd Becker, Christoph Scholl
2009	A	`conf`	Computing Optimized Representations for Non-convex Polyhedra by Detection and Removal of Redundant Linear Constraints. TACAS Christoph Scholl, Stefan Disch, Florian Pigorsch, Stefan Kupferschmid
2009	A	`conf`	Exploiting structure in an AIG based QBF solver. DATE Florian Pigorsch, Christoph Scholl
2009	—	`conf`	Symbolic CTL Model Checking for Incomplete Designs by Selecting Property-Specific Subsets of Local Component Assumptions. MBMV Christian Miller, Tobias Nopper, Christoph Scholl
2009	—	`conf`	Using Implications for Optimizing State Set Representations of Linear Hybrid Systems. MBMV Florian Pigorsch, Christoph Scholl
2008	—	`conf`	Dynamische Verwaltung Virtuellen Speichers für Echtzeitsysteme. Echtzeit Martin Böhnert, Thorsten Zitterell, Christoph Scholl
2008	—	`conf`	Improving energy-efficient real-time scheduling by exploiting code instrumentation. IMCSIT Thorsten Zitterell, Christoph Scholl
2008	—	`ed.`	Methoden und Beschreibungssprachen zur Modellierung und Verifikation von Schaltungen und Systemen (MBMV), Freiburg, Germany, March 3-5, 2008 MBMV Christoph Scholl, Stefan Disch
2007	—	`conf`	Combinational Equivalence Checking Using Incremental SAT Solving, Output Ordering, and Resets. ASP-DAC Stefan Disch, Christoph Scholl
2007	A	`conf`	Computation of minimal counterexamples by using black box techniques and symbolic methods. ICCAD Tobias Nopper, Christoph Scholl, Bernd Becker
2007	—	`conf`	Counterexample Generation for Incomplete Designs. MBMV Tobias Nopper, Christoph Scholl
2007	B	`conf`	Exact State Set Representations in the Verification of Linear Hybrid Systems with Large Discrete State Space. ATVA Werner Damm, Stefan Disch, Hardi Hungar, Swen Jacobs, Jun Pang, Florian Pigorsch, Christoph Scholl, Uwe Waldmann, Boris Wirtz
2007	—	`conf`	Towards an Experimental Autonomous Blimp Platform. EMCR Axel Rottmann, Matthias Sippel, Thorsten Zitterell, Wolfram Burgard, Leonhard M. Reindl, Christoph Scholl
2006	—	`conf`	Advanced SAT-Techniques for Bounded Model Checking of Blackbox Designs. MTV Marc Herbstritt, Bernd Becker, Christoph Scholl
2006	—	`conf`	Advanced Unbounded CTL Model Checking By Using AIGs, BDD Sweeping, and Quantifier Scheduling. MBMV Florian Pigorsch, Christoph Scholl, Stefan Disch
2006	B	`conf`	Advanced Unbounded Model Checking Based on AIGs, BDD Sweeping, And Quantifier Scheduling. FMCAD Florian Pigorsch, Christoph Scholl, Stefan Disch
2006	B	`conf`	Automatic Verification of Hybrid Systems with Large Discrete State Space. ATVA Werner Damm, Stefan Disch, Hardi Hungar, Jun Pang, Florian Pigorsch, Christoph Scholl, Uwe Waldmann, Boris Wirtz
2004	B	`conf`	Approximate Symbolic Model Checking for Incomplete Designs. FMCAD Tobias Nopper, Christoph Scholl
2004	—	`conf`	Filter Based Diagnosis for Multiple Design Errors. MBMV Christoph Scholl, Matthias Büche
2002	C	`conf`	Checking Equivalence for Circuits Containing Incompletely Specified Boxes. ICCD Christoph Scholl, Bernd Becker
2002	—	`conf`	Equivalence Checking in the Presence of Incompletely Specified Boxes. MBMV Christoph Scholl, Bernd Becker
2002	J	`jnl`	On WLCDs and the Complexity of Word-Level Decision Diagrams-A Lower Bound for Division. Formal Methods Syst. Des. Christoph Scholl, Bernd Becker, Thomas M. Weis
2001	A*	`conf`	Checking Equivalence for Partial Implementations. DAC Christoph Scholl, Bernd Becker
2001	—	`conf`	Checking Equivalence for Partial Implementations. MBMV (1) Christoph Scholl, Bernd Becker
2001	—	`conf`	Don't Care Minimization of BMDs: Complexity and Algorithms. MBMV (1) Christoph Scholl, Marc Herbstritt, Bernd Becker
2001	—	`conf`	Exploiting don't cares to minimize *BMDs. ISCAS (5) Christoph Scholl, Marc Herbstritt, Bernd Becker
2001	—	`book`	Functional decomposition with applications to FPGA synthesis. Christoph Scholl
2001	—	`conf`	The multiple variable order problem for binary decision diagrams: theory and practical application. ASP-DAC Christoph Scholl, Bernd Becker, Andreas Brogle
2000	A*	`conf`	Distance driven finite state machine traversal. DAC Andreas Hett, Christoph Scholl, Bernd Becker
2000	A	`conf`	On the Generation of Multiplexer Circuits for Pass Transistor Logic. DATE Christoph Scholl, Bernd Becker
2000	—	`conf`	State Traversal guided by Hamming Distance Profiles. MBMV Andreas Hett, Christoph Scholl, Bernd Becker
1999	J	`jnl`	BDD minimization using symmetries. IEEE Trans. Comput. Aided Des. Integr. Circuits Syst. Christoph Scholl, Dirk Möller, Paul Molitor, Rolf Drechsler
1999	—	`book`	Datenstrukturen und effiziente Algorithmen für die Logiksynthese kombinatorischer Schaltungen. Paul Molitor, Christoph Scholl
1998	A	`conf`	Multi-output Functional Decomposition with Exploitation of Don't Cares. DATE Christoph Scholl
1998	A	`conf`	Word-level decision diagrams, WLCDs and division. ICCAD Christoph Scholl, Bernd Becker, Thomas M. Weis
1997	A	`conf`	Functional simulation using binary decision diagrams. ICCAD Christoph Scholl, Rolf Drechsler, Bernd Becker
1997	—	`—`	Mehrstufige Logiksynthese unter Ausnutzung funktionaler Eigenschaften. Christoph Scholl
1997	—	`conf`	Minimizing ROBDD sizes of incompletely specified Boolean functionsby exploiting strong symmetries. ED&TC Christoph Scholl, S. Melchior, Günter Hotz, Paul Molitor
1995	—	`conf`	Communication based FPGA synthesis for multi-output Boolean functions. ASP-DAC Christoph Scholl, Paul Molitor
1994	—	`conf`	Communication based multilevel synthesis for multi-output Boolean functions. Great Lakes Symposium on VLSI Paul Molitor, Christoph Scholl