author | kleing |
Thu, 25 Jan 2001 11:59:52 +0100 | |
changeset 10977 | 4b47d8aaf5af |
parent 10462 | adf901eb9c40 |
child 11109 | ce1cefc6c14c |
permissions | -rw-r--r-- |
8056 | 1 |
%title% |
2 |
Isabelle at Munich |
|
3 |
||
4 |
||
5 |
%body% |
|
6 |
||
7 |
<h1>Isabelle at Munich</h1> |
|
8 |
||
9 |
<p> |
|
10 |
||
11 |
<a href="http://isabelle.in.tum.de/">Isabelle</a> is a generic theorem |
|
12 |
proving environment developed at Cambridge University (<a |
|
13 |
href="http://www.cl.cam.ac.uk/users/lcp/">Larry Paulson</a>) and TU |
|
14 |
Munich (<a href="http://www.in.tum.de/~nipkow/">Tobias Nipkow</a>). |
|
15 |
This is the local page of the Munich group. |
|
16 |
||
10019 | 17 |
|
8056 | 18 |
<h2>People</h2> |
19 |
||
20 |
The following people are involved in Isabelle applications or |
|
10462 | 21 |
development in our group (alphabetical order): |
22 |
<p> |
|
23 |
<b>Researches:</b> |
|
8056 | 24 |
|
25 |
<ul> |
|
26 |
||
27 |
<li> <a href="http://www.in.tum.de/~bauerg/">Gertrud Bauer</a> |
|
8455
2b828d22b538
made links to homepages absolute, avoids trouble with relative links on the
kleing
parents:
8061
diff
changeset
|
28 |
<li> <a href="http://www4.in.tum.de/~berghofe/">Stefan Berghofer</a> |
2b828d22b538
made links to homepages absolute, avoids trouble with relative links on the
kleing
parents:
8061
diff
changeset
|
29 |
<li> <a href="http://www4.in.tum.de/~kleing/">Gerwin Klein</a> |
2b828d22b538
made links to homepages absolute, avoids trouble with relative links on the
kleing
parents:
8061
diff
changeset
|
30 |
<li> <a href="http://www4.in.tum.de/~narasche/">Wolfgang Naraschewski</a> |
2b828d22b538
made links to homepages absolute, avoids trouble with relative links on the
kleing
parents:
8061
diff
changeset
|
31 |
<li> <a href="http://www4.in.tum.de/~nipkow/">Tobias Nipkow</a> |
2b828d22b538
made links to homepages absolute, avoids trouble with relative links on the
kleing
parents:
8061
diff
changeset
|
32 |
<li> <a href="http://www4.in.tum.de/~oheimb/">David von Oheimb</a> |
2b828d22b538
made links to homepages absolute, avoids trouble with relative links on the
kleing
parents:
8061
diff
changeset
|
33 |
<li> <a href="http://www4.in.tum.de/~prensani/">Leonor Prensa Nieto</a> |
2b828d22b538
made links to homepages absolute, avoids trouble with relative links on the
kleing
parents:
8061
diff
changeset
|
34 |
<li> <a href="http://www4.in.tum.de/~pusch/">Cornelia Pusch</a> |
10977
4b47d8aaf5af
added Martin Strecker, Christian Buttenberg, Alexandra Kirsch and project
kleing
parents:
10462
diff
changeset
|
35 |
<li> <a href="http://www4.in.tum.de/~streckem/">Martin Strecker</a> |
8455
2b828d22b538
made links to homepages absolute, avoids trouble with relative links on the
kleing
parents:
8061
diff
changeset
|
36 |
<li> <a href="http://www4.in.tum.de/~wenzelm/">Markus Wenzel</a> |
8056 | 37 |
|
38 |
</ul> |
|
39 |
||
10462 | 40 |
<p> |
41 |
<b>Students:</b> |
|
42 |
||
43 |
<ul> |
|
44 |
||
10977
4b47d8aaf5af
added Martin Strecker, Christian Buttenberg, Alexandra Kirsch and project
kleing
parents:
10462
diff
changeset
|
45 |
<li> <a href="mailto:buttenbe@in.tum.de">Christian Buttenberg</a> </li> |
4b47d8aaf5af
added Martin Strecker, Christian Buttenberg, Alexandra Kirsch and project
kleing
parents:
10462
diff
changeset
|
46 |
<li> <a href="http://home.informatik.tu-muenchen.de/~kirsch/">Alexandra Kirsch</a> </li> |
10462 | 47 |
<li> <a href="http://www.informatik.tu-muenchen.de/~nanz/">Sebastian Nanz</a> </li> |
48 |
<li> <a href="http://www.informatik.tu-muenchen.de/~pfeifrot/">Johannes Pfeifroth</a> </li> |
|
49 |
||
50 |
</ul> |
|
51 |
||
8056 | 52 |
|
53 |
<h2>Projects</h2> |
|
54 |
||
55 |
The main Isabelle related projects at TU Munich are currently: |
|
56 |
||
57 |
<ul> |
|
58 |
||
10180 | 59 |
<li> <b><a href="Bali/index.html">Isabelle/Bali</a></b> Java and JVM |
8056 | 60 |
formalization --- type system, semantics, compilers |
61 |
||
10180 | 62 |
<li> <b><a href="Isar/index.html">Isabelle/Isar</a></b> Intelligible |
8056 | 63 |
semi-automated reasoning --- readable formal proof documents |
64 |
||
10180 | 65 |
<li><b><a href="IOA/index.html">Isabelle/IOA</a></b> Verification of |
8056 | 66 |
distributed, reactive systems using I/O Automata |
67 |
||
8061 | 68 |
<li> <b>Isabelle/HOOL</b> Object-oriented verification of |
69 |
object-oriented programs |
|
70 |
||
10977
4b47d8aaf5af
added Martin Strecker, Christian Buttenberg, Alexandra Kirsch and project
kleing
parents:
10462
diff
changeset
|
71 |
<li> <b><a href="VerifiCard/">Isabelle/VerifiCard</a></b> |
4b47d8aaf5af
added Martin Strecker, Christian Buttenberg, Alexandra Kirsch and project
kleing
parents:
10462
diff
changeset
|
72 |
Tool-assisted Specification and Verification of JavaCardŽ Programs |
4b47d8aaf5af
added Martin Strecker, Christian Buttenberg, Alexandra Kirsch and project
kleing
parents:
10462
diff
changeset
|
73 |
|
8056 | 74 |
</ul> |
75 |
||
76 |
<p> |
|
77 |
||
78 |
<b>Important local information:</b> Students are welcome to |
|
10180 | 79 |
participate, see <a href="stud/index.html">Isabelle Projekte für |
80 |
Studenten</a> (in German) for more information. |