Prof. Tobias Nipkow

Now soliciting your submission: AFP: The Archive of Formal Proofs Now out: The Isabelle/HOL Tutorial Now out in paperback: Term Rewriting and All That Publications Isabelle Bachelor&Masterarbeiten Neu: Gilt log 2x ≥ 2 log log x?, SAT-Löser Bafög

• Lehrveranstaltungen im SS 2009:
  • Einführung in die Theoretische Informatik
  • Perlen der Informatik 2
• Some recommended events:
  • TPHOLs 2009 (in Munich!)
  • ISLA 2010
  • IJCAR 2010
  • ITP 2010
  • CSL 2010
  • ICTAC 2010
• Some recommended journals:
  • JOURNAL OF AUTOMATED REASONING (JAR)
  • ACM Transactions on Computational Logic (TOCL)
  • Logical Methods in Computer Science (LMCS)
• Some recommended texts and images.
• Projects
• Miscellany

Research Interests

Projects

Reliably Secure Software Systems - DFG Priority Program


Puma - DFG Doctorate Program Program and Model Analysis


Verisoft - Verified Software

Past

TYPES - Mathematical modelling and reasoning using typed logics. EU Working Group.

GKLI - PhD programme Logic in Informatics

InopSys - Calculi for system modelling

VerifiCard - Theorem proving for JavaCard

Isar - Intelligible semi-automated reasoning

Bali - Formalizing Java in Isabelle

CCL - Construction of Computational Logics. ESPRIT Working Group.

DEDUCTION - Formal verification in Higher-Order Logic in Isabelle

Address
         Prof. Tobias Nipkow
         Institut für Informatik
	 Technische Universität München
         Boltzmannstr. 3
         85748 Garching
         Germany

Phone:   +49 (89) 289 17302
Fax:     +49 (89) 289 17307
Office:  01.11.058

E-mail:  last-name at in.tum.de