Author:Christoph Weidenbach

Publications
Efficient Linear Model Building and Clause Evaluation Simon Schwarz, Christoph Weidenbach and Fabian Wobito In:Proceedings of 16th International Workshop on the Implementation on Logics. Proceedings of the 26th Conference on Logic for Programming, Artificial Intelligence, and Reasoning (short papers)
Extending SMT Solving with Non-Ground Clause Learning Yasmine Briefs and Christoph Weidenbach In:Proceedings of the 26th Conference on Logic for Programming, Artificial Intelligence, and Reasoning
Automatic Bit- and Memory-Precise Verification of eBPF Code Martin Bromberger, Simon Schwarz and Christoph Weidenbach In:Proceedings of 25th Conference on Logic for Programming, Artificial Intelligence and Reasoning
Exploring Partial Models with SCL Martin Bromberger, Simon Schwarz and Christoph Weidenbach In:Proceedings of 24th International Conference on Logic for Programming, Artificial Intelligence and Reasoning
A Verified SAT Solver Framework including Optimization and Partial Valuations Mathias Fleury and Christoph Weidenbach In:LPAR23. LPAR-23: 23rd International Conference on Logic for Programming, Artificial Intelligence and Reasoning
Do Portfolio Solvers Harm? Christoph Weidenbach In:ARCADE 2017. 1st International Workshop on Automated Reasoning: Challenges, Applications, Directions, Exemplary Achievements
BDI: A New Decidable First-order Clause Class Manuel Lamotte-Schubert and Christoph Weidenbach In:LPAR-19. 19th International Conference on Logic for Programming, Artificial Intelligence and Reasoning
Satisfiability Checking and Query Answering for Large Ontologies Christoph Weidenbach and Patrick Wischnewski In:PAAR-2012. Third Workshop on Practical Aspects of Automated Reasoning

Keyphrases

CDCL², CDCL with branch and bound, clauses, Constrained Horn Clauses, decidability, eBPF, first-order², first-order logic, first-order model building, first-order reasoning², hyper-resolution, model building, non-redundant learning, Ontology Reasoning, ordered resolution, portfolio, program verification, query answering, resolution, SAT, satisfiability checking, SCL², SCL(FOL), SMT, solver, SPASS(SCL), superposition², theorem prover, verification.