Prof. Tobias Nipkow

Now soliciting your submission: AFP: The Archive of Formal Proofs The Isabelle/HOL Tutorial Term Rewriting and All That Publications Isabelle Bachelor&Masterarbeiten Bafög

• Lehrveranstaltungen im SS 2012:
  • Equational Logic
  • Perlen der Informatik 2
• Some recommended events:
  • Summer School Marktoberdorf 2011 Material
  • VMCAI 2012
  • VSTTE 2012
  • Isabelle Users Workshop 2012
  • ITP 2012
  • IJCAR 2012
  • TACAS 2013
• 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

Executing HOL - DFG Project


Secure Type Systems and Deduction - DFG Project


CAVA: Computer Aided Verification of Automata - DFG Project


Reliably Secure Software Systems - DFG Priority Program


Puma - DFG Doctorate Program Program and Model Analysis

Past

Verisoft - Verified Software

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

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

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

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

Sprechstunde: Im Semester mittwochs 11:00-12:00, sonst nach Vereinbarung.