Uwe Waldmann – Research

Current Research

Combining and extending deductive systems,
e.g., higher-order and first-order theorem provers; first-order theorem provers and mathematical reasoners; tableau calculi and equality.

Extending the range of fully symbolic first-order model checking.

Publications

E. Althaus, et al.:
Verification of Linear Hybrid Systems with Large Discrete State Spaces Using Counterexample-Guided Abstraction Refinement,
to appear in SCP, 2017.

H. Becker, J. C. Blanchette, U. Waldmann, D. Wand:
A Transfinite Knuth-Bendix Order for Lambda-Free Higher-Order Terms,
to appear in CADE-26, 2017.

J. C. Blanchette, U. Waldmann, D. Wand:
A Lambda-Free Higher-Order Recursive Path Order,
in FoSSaCS 2017, LNCS 10203, pp. 461-479, 2017.

R. A. Schmidt, U. Waldmann:
Modal Tableau Systems with Blocking and Congruence Closure,
in TABLEAUX 2015, LNAI 9323, pp. 38-53, 2015.

P. Baumgartner, J. Bax, U. Waldmann:
Beagle – A Hierarchic Superposition Theorem Prover,
in CADE-25, LNAI 9195, pp. 367-377, 2015.

U. Waldmann:
Hierarchic superposition revisited (Abstract),
invited talk, PAAR 2014.

P. Baumgartner, J. Bax, U. Waldmann:
Finite quantification in hierarchic theorem proving,
in IJCAR 2014, LNAI 8562, pp. 152-167, 2014.

P. Baumgartner, U. Waldmann:
Hierarchic superposition: Completeness without compactness,
in MACIS 2013, pp. 8-12, 2013.

P. Baumgartner, U. Waldmann:
Hierarchic superposition with weak abstraction,
in CADE-24, LNAI 7898, pp. 39-57, 2013.

T. Hillenbrand, R. Piskac, U. Waldmann, C. Weidenbach:
From search to computation: Redundancy criteria and simplification at work,
in Programming Logics, Essays in Memory of Harald Ganzinger, LNCS 7797, pp. 169-193, 2013.

W. Damm, et al.:
Exact and fully symbolic verification of linear hybrid automata with large discrete state spaces,
in SCP, 77(10-11):1122-1150, 2012.

P. Baumgartner, U. Waldmann:
A combined superposition and model evolution calculus,
in JAR, 47(2):191-227, 2011.

P. Baumgartner, U. Waldmann:
Superposition and model evolution combined,
in CADE-22, LNAI 5663, pp. 17-34, 2009.

W. Damm, et al.:
Exact state set representation in the verification of linear hybrid systems with large discrete state space,
in ATVA 2007, LNCS 4762, pp. 425-440, 2007.

M. Ludwig, U. Waldmann:
An extension of the Knuth-Bendix ordering with LPO-like properties,
in LPAR 2007, LNAI 4790, pp. 348-362, 2007.

S. Jacobs, U. Waldmann:
Comparing instance generation methods for automated reasoning,
in JAR, 38:57-78, 2007.

W. Damm, et al.:
Automatic verification of hybrid systems with large discrete state space,
in ATVA 2006, LNCS 4218, pp. 276-291, 2006.

H. Ganzinger, V. Sofronie-Stokkermans, U. Waldmann:
Modular proof systems for partial functions with Evans equality,
in I&C, 204:1453-1492, 2006.

V. Prevosto, U. Waldmann:
SPASS+T,
in ESCoR, pp. 18-33, 2006.

S. Jacobs, U. Waldmann:
Comparing instance generation methods for automated reasoning,
in TABLEAUX 2005, LNAI 3702, pp. 153-168, 2005.

H. Ganzinger, V. Sofronie-Stokkermans, U. Waldmann:
Modular proof systems for partial functions with weak equality,
in IJCAR 2004, LNAI 3097, pp. 168-182, 2004.

H. Ganzinger, T. Hillenbrand, U. Waldmann:
Superposition modulo a Shostak theory,
in CADE-19, LNAI 2741, pp. 182-196, 2003.

U. Waldmann:
Cancellative abelian monoids and related structures in refutational theorem proving (Part I).
in JSC, 33(6):777-829, 2002.

U. Waldmann:
Cancellative abelian monoids and related structures in refutational theorem proving (Part  II).
in JSC, 33(6):831-861, 2002.

U. Waldmann:
A new input technique for accented letters in alphabetical scripts.
in IUC 20, 2002.

U. Waldmann:
Superposition and chaining for totally ordered divisible abelian groups.
in IJCAR 2001, LNAI 2083, pp. 226-241, 2001.

U. Waldmann:
Cancellative superposition decides the theory of divisible torsion-free abelian groups.
in LPAR'99, LNAI 1705, pp. 131-147, 1999.

U. Waldmann:
Extending reduction orderings to ACU-compatible reduction orderings.
in IPL, 67(1):43-49, 1998.

U. Waldmann:
Superposition for divisible torsion-free abelian groups.
in CADE-15, LNAI 1421, pp. 144-159, 1998.

U. Waldmann:
Cancellative Abelian Monoids in Refutational Theorem Proving.
PhD Thesis, Universität des Saarlandes, 1997.

H. Ganzinger, U. Waldmann:
Theorem proving in cancellative abelian monoids,
in CADE-13, LNAI 1104, pp. 388-402, 1996.

L. Bachmair, H. Ganzinger, U. Waldmann:
Refutational theorem proving for hierarchic first-order theories,
in AAECC, 5(3/4):193-212, 1994.

L. Bachmair, H. Ganzinger, U. Waldmann:
Superposition with simplification as a decision procedure for the monadic class with equality,
in KGC'93, LNCS 713, pp. 83-96, 1993.

L. Bachmair, H. Ganzinger, U. Waldmann:
Set constraints are the monadic class,
in LICS 8, pp. 75-83, 1993.

L. Bachmair, H. Ganzinger, U. Waldmann:
Theorem proving for hierarchic first-order theories,
in ALP'92, LNCS 632, pp. 420-434, 1992.

H. Ganzinger, U. Waldmann:
Termination proofs of well-moded logic programs via conditional rewrite systems,
in CTRS'92, LNCS 656, pp. 430-437, 1992.

U. Waldmann:
Semantics of order-sorted specifications.
in TCS, 94(1):1-35, 1992.

U. Waldmann:
Compatibility of order-sorted rewrite rules.
in CTRS'90, LNCS 516, pp. 407-416, 1990.

U. Waldmann:
Unitary unification in order-sorted signatures (extended abstract).
in UNIF'89, pp. 106-110, 1989.

Software

SPASS+T

Conferences and Workshops

IWIL 2017, 12th International Workshop on the Implementation of Logics,
Maun, Botswana, May 2017 (PC member)

PAAR-2016, 5th Workshop on Practical Aspects of Automated Reasoning,
Coimbra, Portugal, July 2nd, 2016 (PC member)

IWIL 2015, 11th International Workshop on the Implementation of Logics,
Suva, Fiji, November 2015 (PC member)

IJCAR 2014, 7th International Joint Conference on Automated Reasoning,
Vienna, Austria, July 2014 (PC member)

IWIL 2013, 10th International Workshop on the Implementation of Logics,
Stellenbosch, South Africa, December 2013 (PC member)

MACIS 2013, Fifth International Conference on Mathematical Aspects of Computer and Information Sciences,
Nanning, China, December 2013 (Track co-chair)

CADE-24, 24th International Conference on Automated Deduction,
Lake Placid, NY, USA, June 2013 (PC member)

LfSA'12, CAV 2012 Workshop on Logics for System Analysis,
Berkeley, USA, July 2012 (PC member)

IWIL 2012, LPAR-18 Workshop on the Implementation of Logics,
Merida, Venezuela, March 2012 (PC member)

LfSA'10, FLoC 2010 Workshop on Logics for System Analysis,
Edinburgh, United Kingdom, July 2010 (PC member)

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 2003 (PC member)

Journals

Mathematics in Computer Science, Special Focus on Constraints and Combinations, 9(3), 2015 (Guest editor, with Pascal Fontaine and Thomas Sturm)

Projects

AVACS - Automatic Verification and Analysis of Complex Systems (until December 2015)

Verisoft - Beweisen als Ingenieurwissenschaft (until June 2006)

Degrees

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).

Awards

LICS Test-of-Time Award 2013 for Set constraints are the monadic class.

Winner of the TFA category (Typed First-order with Arithmetic)
at the CADE Automated Theorem Prover Competition 2013 with SPASS+T.

Winner of the TFA category (Typed First-order with Arithmetic)
at the CADE Automated Theorem Prover Competition 2011 with SPASS+T.


Previous | Up | Next
Uwe Waldmann <uwe@mpi-inf.mpg.de>, 2017-02-22.