Using AIGs and zonotopes for first-order model checking
Combining model elimination and superposition
Superposition and Model Evolution Combined,
with Peter Baumgartner.
In CADE 2009, pp. 17-34, 2009.
Exact state set representation in the verification of linear hybrid systems with large discrete state space,
with Werner Damm et al.
In ATVA 2007, pp. 425-440, 2007.
An Extension of the Knuth-Bendix Ordering with LPO-like Properties,
with Michel Ludwig.
In LPAR 2007, pp. 348-362, 2007.
Comparing instance generation methods for automated reasoning,
with Swen Jacobs.
In JAR, 38:57-78, 2007.
Automatic verification of hybrid systems with large discrete state space,
with Werner Damm et al.
In ATVA 2006, pp. 276-291, 2006.
Modular proof systems for partial functions with Evans equality,
with Harald Ganzinger and Viorica Sofronie-Stokkermans.
In I&C, 204:1453-1492, 2006.
SPASS+T,
with Virgile Prevosto.
In ESCoR, pp. 18-33, 2006.
Comparing instance generation methods for automated reasoning,
with Swen Jacobs.
In TABLEAUX 2005, LNAI 3702, pp. 153-168, 2005.
Modular proof systems for partial functions with weak equality,
with Harald Ganzinger and Viorica Sofronie-Stokkermans.
In IJCAR 2004, LNAI 3097, pp. 168-182, 2004.
Superposition modulo a Shostak theory,
with Harald Ganzinger and Thomas Hillenbrand.
In CADE-19, LNAI 2741, pp. 182-196, 2003.
Cancellative abelian monoids and related structures in refutational theorem proving (Part I).
In JSC, 33(6):777-829, 2002.
Cancellative abelian monoids and related structures in refutational theorem proving (Part II).
In JSC, 33(6):831-861, 2002.
A new input technique for accented letters in alphabetical scripts.
In IUC 20, 2002.
Superposition and chaining for totally ordered divisible abelian groups.
In IJCAR 2001, LNAI 2083, pp. 226-241, 2001.
Cancellative superposition decides the theory of divisible torsion-free abelian groups.
In LPAR'99, LNAI 1705, pp. 131-147, 1999.
Extending reduction orderings to ACU-compatible reduction orderings.
In IPL, 67(1):43-49, 1998.
Superposition for divisible torsion-free abelian groups.
In CADE-15, LNAI 1421, pp. 144-159, 1998.
Cancellative Abelian Monoids in Refutational Theorem Proving.
PhD Thesis, Universität des Saarlandes, 1997.
Theorem proving in cancellative abelian monoids,
with Harald Ganzinger.
In CADE-13, LNAI 1104, pp. 388-402, 1996.
Refutational theorem proving for hierarchic first-order theories,
with Leo Bachmair and Harald Ganzinger.
In AAECC, 5(3/4):193-212, 1994.
Superposition with simplification as a decision procedure for the monadic class with equality,
with Leo Bachmair and Harald Ganzinger.
In KGC'93, LNCS 713, pp. 83-96, 1993.
Set constraints are the monadic class,
with Leo Bachmair and Harald Ganzinger.
In LICS 8, pp. 75-83, 1993.
Theorem proving for hierarchic first-order theories,
with Leo Bachmair and Harald Ganzinger.
In ALP'92, pp. 420-434, 1992.
Termination proofs of well-moded logic programs via conditional rewrite systems,
with Harald Ganzinger.
In CTRS'92, LNCS 656, pp. 430-437, 1992.
Semantics of order-sorted specifications.
In TCS, 94(1):1-35, 1992.
Compatibility of order-sorted rewrite rules.
In CTRS'90, LNCS 516, pp. 407-416, 1990.
Unitary unification in order-sorted signatures (extended abstract).
In UNIF'89, pp. 106-110, 1989.
PAAR-2008, IJCAR 2008 Workshop on Practical Aspects of Automated Reasoning, Sydney, Australia, August 2008 (PC member)
ESARM, CICM 2008 Workshop on Empirically Successful Automated Reasoning for Mathematics, Birmingham, United Kingdom, July/August 2008 (PC member)
ESARLT, CADE-21 Workshop on Empirically Successful Automated Reasoning in Large Theories, Bremen, Germany, July 2007 (PC member)
ESCoR, FLoC'06 Workshop on Empirically Successful Computerized Reasoning, Seattle, USA, August 2006 (PC member)
RTA'03, 14th International Conference on Rewriting Techniques and Applications, Valencia, Spain, June 9-11, 2003 (PC member)
AVACS - Automatic Verification and Analysis of Complex Systems
Verisoft - Beweisen als Ingenieurwissenschaft (until June 2006)
PhD in Computer Science (Dr.-Ing.), Universität des Saarlandes, July 1997.
Thesis:
Cancellative
Abelian Monoids in Refutational Theorem Proving.
Diploma in Computer Science (Dipl.-Inf.), Universität Dortmund, August 1989.
Thesis: Vervollständigung von Spezifikationen mit Subsortendeklarationen
(Completion of Specifications with Subsort Declarations).