BibSLEIGH — Christoph

Travelled to:

1 × Canada
1 × Denmark
1 × Japan
1 × Portugal
2 × Australia
2 × Italy
2 × United Kingdom
3 × Germany
3 × USA

Collaborated with:

M.Horbach ∅ M.Bromberger M.Suda P.Wischnewski A.Fietzke G.Rock C.Meyer M.Fleury N.Azmy A.Teucke A.Fiori T.Hillenbrand D.Topic T.Sturm P.Fontaine S.Merz A.Nonnengart F.Jacquemard H.Ganzinger B.Gaede J.C.Blanchette M.Voigt D.Dhungana C.H.Tang T.Lev-Ami T.W.Reps M.Sagiv S.Schwarz R.A.Schmidt R.Rusev D.Dimova R.Kumar U.Brahm E.Keen C.Theobalt

Talks about:

version (5) spass (5) decid (5) linear (4) claus (4) theori (3) system (3) order (3) model (3) label (3)

Person: Christoph Weidenbach

DBLP: Weidenbach:Christoph

Facilitated 1 volumes:

Contributed to:

2015

2013

2012

2010

2009

2008

2007

2002

1999

1998

1997

1996

2016

2017

2019

Wrote 27 papers:

CADE-2015-Bromberger0W #integer #linear #revisited: Linear Integer Arithmetic Revisited (MB, TS, CW), pp. 623–637.
ASE-2013-DhunganaTWW #automation #interactive #rule-based #verification: Automated verification of interactive rule-based configuration systems (DD, CHT, CW, PW), pp. 551–561.
CADE-2013-AzmyW #normalisation: Computing Tiny Clause Normal Forms (NA, CW), pp. 109–125.
IJCAR-2012-FontaineMW #decidability: Combination of Disjoint Theories: Beyond Decidability (PF, SM, CW), pp. 256–270.
IJCAR-2012-SudaW: A PLTL-Prover Based on Labelled Superposition with Partial Model Guidance (MS, CW), pp. 537–543.
IJCAR-2010-SudaWW #on the: On the Saturation of YAGO (MS, CW, PW), pp. 441–456.
CADE-2009-HorbachW #decidability: Decidability Results for Saturation-Based Model Building (MH, CW), pp. 404–420.
CADE-2009-WeidenbachDFKSW: SPASS Version 3.5 (CW, DD, AF, RK, MS, PW), pp. 140–145.
CSL-2009-HorbachW #induction #query: Deciding the Inductive Validity of FOR ALL THERE EXISTS * Queries (MH, CW), pp. 332–347.
CSL-2008-HorbachW: Superposition for Fixed Domains (MH, CW), pp. 293–307.
IJCAR-2008-FietzkeW: Labelled Splitting (AF, CW), pp. 459–474.
CADE-2007-Lev-AmiWRS: Labelled Clauses (TLA, CW, TWR, MS), pp. 311–327.
CADE-2007-WeidenbachSHRT: System Description: SpassVersion 3.0 (CW, RAS, TH, RR, DT), pp. 514–520.
CADE-2002-WeidenbachBHKTT: S PASS Version 2.0 (CW, UB, TH, EK, CT, DT), pp. 275–279.
CADE-1999-Weidenbach #analysis #automation #first-order #logic #protocol #security #towards: Towards an Automatic Analysis of Security Protocols in First-Order Logic (CW), pp. 314–328.
CADE-1999-Weidenbach99a: System Description: Spass Version 1.0.0 (CW), pp. 378–382.
CADE-1998-NonnengartRW #generative #normalisation #on the: On Generating Small Clause Normal Forms (AN, GR, CW), pp. 397–411.
RTA-1998-JacquemardMW #equation #unification: Unification in Extension of Shallow Equational Theories (FJ, CM, CW), pp. 76–90.
CADE-1997-GanzingerMW #order #type system: Soft Typing for Ordered Resolution (HG, CM, CW), pp. 321–335.
CADE-1996-Weidenbach #decidability #pseudo #unification: Unification in Pseudo-Linear Sort Theories is Decidable (CW), pp. 343–357.
CADE-1996-WeidenbachGR: SPASS & FLOTTER Version 0.42 (CW, BG, GR), pp. 141–145.
IJCAR-2016-BlanchetteFW #framework #satisfiability: A Verified SAT Solver Framework with Learn, Forget, Restart, and Incrementality (JCB, MF, CW), pp. 25–44.
IJCAR-2016-BrombergerW #constraints #performance #testing #theorem proving: Fast Cube Tests for LIA Constraint Solving (MB, CW), pp. 116–132.
CADE-2017-HorbachVW #integer #linear #on the: On the Combination of the Bernays-Schönfinkel-Ramsey Fragment with Simple Linear Integer Arithmetic (MH, MV, CW), pp. 77–94.
CADE-2017-TeuckeW #constraints #decidability #first-order #linear #monad: Decidability of the Monadic Shallow Linear First-Order Fragment with Straight Dismatching Constraints (AT, CW), pp. 202–219.
CADE-2019-BrombergerFSW: SPASS-SATT - A CDCL(LA) Solver (MB, MF, SS, CW), pp. 111–122.
CADE-2019-FioriW #learning #modelling: SCL Clause Learning from Simple Models (AF, CW), pp. 233–249.