Christoph Weidenbach
31 publications
4 venues
H Index 13
Affiliation
Max Planck Institute for Informatics, Saarbr cken, GermanyLinks
| Name | Venue | Year | citations |
|---|---|---|---|
Computing Ground Congruence Classes.
|
CADE | 2025 | 0 |
| A Stepwise Refinement Proof that SCL(FOL) Simulates Ground Ordered Resolution.
|
CADE | 2025 | 0 |
| Automatic Bit- and Memory-Precise Verification of eBPF Code.
|
LPAR | 2024 | 2 |
| An Isabelle/HOL Formalization of the SCL(FOL) Calculus.
|
CADE | 2023 | 1 |
| SCL(FOL) Can Simulate Non-Redundant Superposition Clause Learning.
|
CADE | 2023 | 1 |
| Exploring Partial Models with SCL.
|
LPAR | 2023 | 0 |
| Generalized Completeness for SOS Resolution and its Application to a New Notion of Relevance.
|
CADE | 2021 | 7 |
| A Verified SAT Solver Framework including Optimization and Partial Valuations.
|
LPAR | 2020 | 2 |
| SCL Clause Learning from Simple Models.
|
CADE | 2019 | 17 |
| SPASS-SATT - A CDCL(LA) Solver.
|
CADE | 2019 | 7 |
| Decidability of the Monadic Shallow Linear First-Order Fragment with Straight Dismatching Constraints.
|
CADE | 2017 | 7 |
| On the Combination of the Bernays-Schönfinkel-Ramsey Fragment with Simple Linear Integer Arithmetic.
|
CADE | 2017 | 10 |
| A Verified SAT Solver Framework with Learn, Forget, Restart, and Incrementality.
|
IJCAI | 2017 | 0 |
| Linear Integer Arithmetic Revisited.
|
CADE | 2015 | 15 |
| Computing Tiny Clause Normal Forms.
|
CADE | 2013 | 12 |
| Labelled Superposition for PLTL.
|
LPAR | 2012 | 10 |
| Automatic Generation of Invariants for Circular Derivations in SUP(LA).
|
LPAR | 2012 | 8 |
| Decidability Results for Saturation-Based Model Building.
|
CADE | 2009 | 10 |
| SPASS Version 3.5.
|
CADE | 2009 | 311 |
| System Description: SpassVersion 3.0.
|
CADE | 2007 | 59 |
| Labelled Clauses.
|
CADE | 2007 | 15 |
| S PASS Version 2.0.
|
CADE | 2002 | 51 |
| First-Order Atom Definitions Extended.
|
LPAR | 2001 | 4 |
| System Description: Spass Version 1.0.0.
|
CADE | 1999 | 133 |
| Towards an Automatic Analysis of Security Protocols in First-Order Logic.
|
CADE | 1999 | 185 |
| On Generating Small Clause Normal Forms.
|
CADE | 1998 | 75 |
| Soft Typing for Ordered Resolution.
|
CADE | 1997 | 47 |
| SPASS & FLOTTER Version 0.42.
|
CADE | 1996 | 87 |
| Unification in Pseudo-Linear Sort Theories is Decidable.
|
CADE | 1996 | 7 |
| Extending the Resolution Method with Sorts.
|
IJCAI | 1993 | 18 |
| A Resolution Calculus with Dynamic Sort Structures and Partial Functions.
|
ECAI | 1990 | 23 |