Martin Lange's homepage</a> <script type="text/javascript"> function highlight(n) { n.style.backgroundColor="#5179F1"; } function lowlight(n) { n.style.backgroundColor="#DCDCDC"; } </script> <style type="text/css"> body { background-color:#FFFFCC; } a { text-decoration:none } #bereich { line-height:1.3em } </style> </head> <body style="margin-left:40px"> <table border="0" style="float:left"> <tr align="left"> <table width="800" border="1" frame="void" cellspacing="0" cellpadding="0"> <tr> <td style="height:15px; width:100px; background-color:#DCDCDC" align="center" onmouseover="highlight(this)" onmouseout="lowlight(this)"> <a href="index.html" style="text-decoration:none; color:black">Home</a> </td> <td style="height:15px; width:100px; background-color:#DCDCDC" align="center" onmouseover="highlight(this)" onmouseout="lowlight(this)"> <a href="projects.html" style="text-decoration:none; color:black">Projects</a> </td> <td style="height:15px; width:100px; background-color:#DCDCDC" align="center" onmouseover="highlight(this)" onmouseout="lowlight(this)"> <a href="publications.html" style="text-decoration:none; color:black">Publications</a> </td> <td style="height:15px; width:100px; background-color:#DCDCDC" align="center" onmouseover="highlight(this)" onmouseout="lowlight(this)"> <a href="activities.html" style="text-decoration:none; color:black">Activities</a> </td> <td style="height:15px; width:100px; background-color:#DCDCDC" align="center" onmouseover="highlight(this)" onmouseout="lowlight(this)"> <a href="teaching.html" style="text-decoration:none; color:black">Teaching</a> </td> <td style="height:15px; width:100px; background-color:#002288" align="center"> <font style="color:white">Students</font> </td> </tr> </table> <table width="90%" border="1" cellspacing="0" cellpadding="10" style="margin-top:-2px"> <tr> <td colspan="7" border="1"> <b>Postgraduate students</b> (for PhD or equivalent)<br> <ul> <li> <a href="www.cip.ifi.lmu.de/~latte/inhalt.html">Markus Latte</a>, 2008-...,<br> <i>Automata for program and model analysis</i> </li> <li> <a href="http://www.tcs.ifi.lmu.de/~friedman">Oliver Friedmann</a>, 2008-..., (co-supervised by <a href="http://www.tcs.ifi.lmu.de/~mhofmann">Martin Hofmann</a>)<br> <i>Algorithms and Lower Bounds for 2-Player Games</i> </li> <li> <a href="http://www.tcs.ifi.lmu.de/~axelsson">Roland Axelsson</a>, 2006-...<br> <i>Verification of non-regular properties</i> </li> </ul> <br> <b>Graduate students</b> (for MSc or equivalent)<br> <ul> <li> Dongyuan Yu, 7/2008<br> <i>Algorithms for String Problems</i> </li> <li> Oliver Friedmann, 2008, co-supervised by Martin Hofmann <br> <i>A proof system for ECTL*<sub>μ</sub></i> </li> <li> <a href="http://www.markus-jehle.de/">Markus Jehle</a>, 02/2008<br> <i>Bounded model checking for All regular Properties</i> </li> <li> Marie-Fleur Revel, 12/2006<br> <i>Translating PSL into the linear time μ-calculus</i> </li> <li> <a href="http://daxc.de/">Christian Dax</a>, 02/2006<br> <i>Games for the linear time μ-calculus</i> </li> <li> Boris Lohner, 12/2005, co-supervised by Hans-Dietmar Jäger<br> <i>Design and implementation of a course evaluation system</i> </li> <li> <a href="http://www.cs.nott.ac.uk/~rxr/">Robert Reitmeier</a>, 09/2005, co-supervised by Jan Johannsen<br> <i>SAT encoding of linear time μ-calculus and weak alternating parity automata</i> </li> </ul> <br> <b>Undergraduate students</b> (for BSc or equivalent)<br> <ul> <li> Dongyuan Yu, 7/2008<br> <i>Factorisation with a SAT solver</i> </li> <li> Oliver Friedmann, 10/2006, co-supervised by Martin Hofmann <br> <i>A proof system for the modal μ-calculus</i> </li> <li> Karl Mehltretter, 06/2006<br> <i>Translations between weak alternating parity automata and the linear time μ-calculus</i> </li> <li> A. Feichtner and S. Sojer, 02/2006<br> <i>A Reduction from Parity Games to SAT</i> </li> <li> <a href="http://www.tcs.ifi.lmu.de/~hoffmann/">Jan Hoffmann</a>, 01/2006<br> <i>Minimising weak alternating parity automata</i> </li> <li> <a href="http://www.markus-jehle.de/">Markus Jehle</a>, 07/2005, co-supervised by Jan Johannsen <br> <i>Bounded model checking for the alternation-free linear time μ-calculus</i> </li> <li> <a href="http://www.rachinsky.de/nicolas/">Nicolas Rachinsky</a>, 07/2005, co-supervised by Jan Johannsen<br> <i>Specifying transition systems in CCS</i> </li> <li> <a href="http://daxc.de/">Christian Dax, 07/2004</a><br> <i>Implementation of LTL focus games</i> </li> </ul> </td> </tr> </table> </tr> </table> </body>