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.1em } </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:#002288" align="center"> <font style="color:white">Projects</font> </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:#DCDCDC" align="center" onmouseover="highlight(this)" onmouseout="lowlight(this)"> <a href="students.html" style="text-decoration:none; color:black">Students</a> </td> </tr> </table> <table width="90%" border="1" cellspacing="0" cellpadding="10" style="margin-top:-2px"> <tr> <td colspan="7" border="1"> <div id="bereich"> <br> <b><a href="http://www.tcs.ifi.lmu.de/~axelsson/veri_non_reg/vnr.html">VeriNonReg</a></b>, <i>Verification of Non-Regular Properties</i><br> This project aims to extend the scope of automatic program verification to structurally more complex properties, namely non-regular languages of words and trees. It is funded by the <a href="http://www.dfg.de">Deutsche Forschungsgemeinschaft</a> and employs PhD student <a href="http://www.tcs.ifi.lmu.de/~axelsson">Roland Axelsson</a>. <br><br><br> <b><a href="http://www.tcs.ifi.lmu.de/~mlange/pgsolver/index.html">PGSolver</a></b><br> The <tt>PGSolver</tt> library is a collection of algorithms for solving parity games that appear somewhere in the literature, as well as some new heuristics etc. It also defines a standard specification format for parity games as well as winning regions and strategies, and provides a collection of benchmark games. Co-developer of this tool is Oliver Friedmann. <br><br><br> <b><a href="http://www.tcs.ifi.lmu.de/~mlange/cfganalyzer/index.html">CFGAnalyzer</a></b><br> A tool that analyzes context-free grammars w.r.t. certain undecidable problems: universality, language inclusion, equivalence, intersection, and ambiguity. It uses an incremental SAT solver to implement semi-decision procedures - not an approximation, i.e. the answers are sound and complete but the program may not terminate. It is described in a paper with Roland Axelsson and Keijo Heljanko. <br><br><br> <b><a href="http://www.tcs.ifi.lmu.de/~mlange/stringalg/index.html">Antichain Based String Algorithms</a></b><br> A small collection of tools that solve NP-complete string algorithms using the power of antichains. Currently, there are available implementations for <i>Longest Common Substring</i> and <i>Hitting String</i>. <br><br><br> <b><a href="http://www.tcs.ifi.lmu.de/musabre">μ-Sabre</a></b>, <i>SAT-Based Verification of Regular Properties</i><br> We develop a verification tool for ω-regular linear time properties focussing on bounded model checking. Co-founder of this project is Jan Johannsen. <br><br><br> <b><a href="http://www.tcs.ifi.lmu.de/~mlange/semexp/index.html">SemExp</a></b>, <i>Semantical Expansion of Boolean Formulas</i><br> A tool to expand boolean formulas in PLA format in order to aid minimisation. <br><br><br> </div> </td> </tr> </table> </tr> </table> </body>