Matthias Schmalz

Publications

• Matthias Schmalz
  Term Rewriting in Logics of Partial Functions.
  Proceedings ICFEM 2011
  (13th International Conference on Formal Engineering Methods)
  LNCS ??, pp. ??-??, Springer, 2011.
  © 2011 Springer-Verlag Springer Link Technical Report
• Matthias Schmalz, Daniele Varacca, and Hagen Völzer:
  Counterexamples in Probabilistic LTL Model Checking for Markov Chains.
  Proceedings CONCUR 2009
  (20th International Conference on Concurrency Theory),
  LNCS 5710, pp. 587-602, Springer, 2009.
  © 2009 Springer-Verlag Springer Link Technical Report Talk
• Ralf Hielscher, Daniel Potts, Jürgen Prestin, Helmut Schaeben, Matthias Schmalz:
  The Radon Transform on SO(3): a Fourier Slice Theorem and Numerical Inversion.
  Inverse Problems 24 (2008) 025011.
  Preliminary Version
• Matthias Schmalz, Hagen Völzer and Daniele Varacca:
  Model Checking Almost All Paths Can Be Less Expensive Than Checking All Paths.
  Proceedings FSTTCS 2007
  (Annual Conference on Foundations of Software Technology and Theoretical Computer Science),
  LNCS 4855, pp. 532-543, Springer, Dec 2007.
  © 2007 Springer-Verlag Springer Link Technical Report Talk

Diploma Thesis

1.3.2007:
Extensions of an Algorithm for Generalised Fair Model Checking

Tools

Isabelle for Event-B

The foundations are described in this technical report (theory files used for the technical report).

The tool is now available (installation instructions).

Currahee

Currahee(E, iProver) is a theorem prover for TPTP problems with many irrelevant axioms. Currahee(E,iProver) applies a number of axiom selection strategies in parallel, and passes the resulting smaller problems to E and/or iProver. Currahee(E, iProver) version 0.1 has achieved the second rank in the LTB division of the CADE ATP systems competition of 2010.

Currahee uses the following axiom selection strategies:

• a technique resembling the original idea underlying SInE,
• (contextual) direct and indirect relevance (Roederer A., Puzis Y., Sutcliffe G. (2009), Divvy: an atp meta-system based on axiom relevance ordering, CADE, pp. 157-162),
• Meng and Paulson's relevance filter for Sledgehammer (Meng J., Paulson L. C. (2009), Lightweight relevance filtering for machine-generated resolution problems, J. Applied Logic, pp. 41-57).

Note that there are versions of E and iProver, namely E-LTB and iProver-SInE, that have been specially designed for problems with many irrelevant axioms. Currahee(E, iProver) uses the "ordinary" versions of E and iProver instead of E-LTB and iProver-SInE.

Downloads

• Currahee(E, iProver) version 0.1

Teaching

• Winter 2007: teaching assistant for Lineare Algebra (Informatik Bachelor)
  Course material can be found here. (Use your ethz username and password for authentication.)
• Summer 2008: teaching assistant for Formal Methods and Functional Programming
• Winter 2008: teaching assistant for System Development in Event-B
• Summer 2009: teaching assistant for Informatik 1 (D-MAVT)
  Course material can be found here. (Use your ethz username and password for authentication.)

Miscellaneous

My PGP key