Publications
The content on this page was translated automatically.
| 2025 | M. Sälzer, P. Wałega, M. Lange The Logical Expressiveness of Temporal GNNs via Two-Dimensional Product Logics Accepted for publication at the 39th Annual Conference on Neural Information Processing Systems, NeuRIPS'25, San Diego, US, 2025 Openreview.net |
| N. Hundeshagen, M. Lange A Study on the Effect of Free Attempts in Theoretical Computer Science Exams Accepted for publication at the 11th Conference on University Didactics in Computer Science, HDI'25, Freiberg, Germany, 2025 | |
| E. Alsmann, M. Lange The Computational Complexity of Satisfiability in State Space Models To appear in the Proceedings of the 28th European Conference on Artificial Intelligence, ECAI'25, Bologna, Italy, 2025 vol. 413 of Frontiers in Artificial Intelligence and Applications, pages 1768–1775, IOS Press | |
| E. Alsmann, M. Lange Linear-Time Metric Temporal Logic with Strict First-Time Semantics In Proceedings of the 32nd International Symposium on Temporal Representation and Reasoning, TIME'25, London, UK, 2025 vol. 355 of LIPIcs, pages 3:1–3:14 DOI | |
| S. Möller, F. Bruse, M. Lange A Finite Abstraction of Real-Valued Functions for Complete Reasoning about Influence In Proceedings of the 15th International Conference on Frontiers of Combining Systems, FroCoS'25, Reykjavik, IS, 2025 vol. 15979 of Lecture Notes in Computer Science, pages 346–363, Springer DOI | |
| M. Herwig, N. Hundeshagen, M. Lange An Earley-Based Universal Error-Correcting Parser In Proceedings of the 29th International Conference on Implementation and Application of Automata, CIAA'25, Palermo, IT, 2025 vol. 15981 of Lecture Notes in Computer Science, pages 208–222, Springer DOI | |
| M. Sälzer, E. Alsmann, M. Lange Transformer Encoder Satisfiability: Complexity and Impact on Formal Reasoning In Proceedings of the 13th International Conference on Learning Representations, ICLR'25, Singapore, SG, 2025 OpenReview.net Link | |
| M. Herwig, N. Hundeshagen, M. Lange Problem-Specific Visual Feedback in Discrete Modelling e-learning & education 16, 2025 | |
| E. Alsmann, M. Lange On the Complexity of Formal Reasoning in State Space Models (Extended Abstract) In Proc. of the 8th Symp. on A.I. Verification, SAIV'25, Zagreb, CR, 2025 vol. 15947 of Lecture Notes in Computer Science, pages 221–226, Springer | |
| M. Hofmann, M. Lange Automata Theory and Logic Springer, 2025, ~420 pages, ISBN 978-3-662-72153-7 DOI | |
| Maurice Herwig, Norbert Hundeshagen, Cedric Kollenberg, and Robin Weber On AI-Generated Reductions from Natural Language Descriptions In Proceedings of the 23rd Conference on Educational Technologies, DELFI 2025, Freiberg pp. 289–293, 2025 | |
| 2024 | F. Bruse, M. Lange Computing All Minimal Ways to Reach a Context-Free Language In Proceedings of the 18th International Conference on Reachability Problems, RP'24, Vienna, Austria, 2024 Vol. 15050 of Lecture Notes in Computer Science, pp. 38–53, Springer DOI |
| M. Herwig, N. Hundeshagen, J. Hundhausen, S. Kablowski, M. Lange Problem-Specific Visual Feedback in Discrete Modeling In Proc. 22nd Symposium on Educational Technologies, DELFI'24, Fulda, Germany, 2024 vol. P356 of Lecture Notes in Informatics, German Informatics Society DOI | |
| M. Sälzer, E. Alsmann, F. Bruse, M. Lange Verifying and Interpreting Neural Networks using Finite Automata In Proc. of the 28th Int. Conf. on Developments in Language Theory, DLT'24, Göttingen, Germany, 2024 vol. 14791 of Lecture Notes in Computer Science, pp. 266–281, Springer | |
| F. Bruse, M. Lange Model Checking Timed Recursive CTL Information and Computation 298:105168, 2024 | |
| E. Alsmann, F. Bruse:“ Real-Time Higher-Order Recursion Schemes.” TIME 2024: 16:1–16:20 | |
| F. Bruse, M. Herwig, M. Lange:“ Weights of Formal Languages Based on Geometric Series with an Application to Automatic Grading.” Theor. Comput. Sci. 983: 114295 (2024) | |
| M. Kastaun, N. Hundeshagen, M. Lange, M. Meier. *AI for the Professional Development of Prospective Biology Teachers: The Case of Hypothesis Formation in the Natural Sciences* In Competencies for Teaching with and about Artificial Intelligence in the Natural Sciences: DiKoLANKI, Waxman, 2024. | |
| M. Herwig, N. Hundeshagen, M. Kastaun, C. Kollenberg *Towards Computer-Aided Teaching of Reductions in Theoretical Computer Science* In /Proc. 22nd Conference on Educational Technologies, DELFI'24/, Fulda, Germany, 2024 vol. P356 of /Lecture Notes in Informatics/, Gesellschaft für Informatik DOI <https://doi.org/10.18420/delfi2024_45> | |
| P. Nunn, F. Schwarzentruber, M. Sälzer, N. Troquard , “A Logic for Reasoning about Aggregate-Combine Graph Neural Networks,” , In: Proceedings of the Thirty-Third International Joint Conference on Artificial Intelligence, IJCAI 2024, Jeju, South Korea, August 3–9, 2024. ijcai.org, 2024, pp. 3532–3540. url: https://www.ijcai.org/proceedings/2024/391 | |
| 2023 | Alexander Artikis, Florian Bruse, Luke Hunsberger , 30th International Symposium on Temporal Representation and Reasoning( , TIME 2023), September 25–26, 2023, NCSR Demokritos, Athens, Greece.LIPIcs 278, Schloss Dagstuhl – Leibniz Center for Computer Science 2023, ISBN 978-3-95977-298-3 |
| M. Sälzer, Beddar-Wiesing Time-Aware Robustness of Temporal Graph Neural Networks for Link Prediction (Extended Abstract) TIME 2023 | |
| F. Bruse, M. Herwig, M. Lange Weights of Formal Languages Based on Geometric Series with an Application to Automatic Grading Theoretical Computer Science 938:114295, 2023 | |
| M. Sälzer, M. Lange Reachability in Simple Neural Networks Fundamenta Informaticae, 189(3-4):241-259, special issue on RP'21, 2023 | |
| F. Bruse, M. Lange, E. Lozes , “The Tail-Recursive Fragment of Timed RecursiveCTL” , *Information and Computation*, 294:105084, special issue on TIME'22, 2023 | |
| F. Bruse, M. Kastaun, M. Lange, S. Möller The Calculus of Temporal Influence In Proceedings of the 30th International Symposium on Temporal Representation and Reasoning, TIME'23, Athens, GR, 2023 vol. 278 of LIPIcs, pages 10:1–10:19 | |
| F. Bruse, M. Lange, S. Möller : Formal Reasoning about Influence in Natural Sciences Experiments In Proceedings of the 29th International Conference on Automated Deduction, CADE'23, Rome, IT, 2023 vol. 14132 of Lecture Notes in Computer Science, pages 153–169, Springer | |
| M. Sälzer, M. Lange Fundamental Limits in Formal Verification of Message-Passing Neural Networks In Proceedings of the 11th International Conference on Learning Representations, ICLR'23, Kigali, RWA, 2023 OpenReview.net, 2023 | |
| M. Sälzer, E. Alsmann, M. Lange On Challenges and Opportunities in the Translation of Deep Neural Networks into Finite Automata In Proceedings of the 5th Workshop on Artificial Intelligence and Formal Verification, Logic, Automata, and Synthesis, OVERLAY'23, Rome, IT, 2023 | |
| 2022 | F. Bruse, D. Kronenberger, M. Lange Capturing Bisimulation-Invariant Time-Complexity Classes via Polyadic Higher-Order Fixpoint Logic In Proceedings of the 13th International Symposium on Games, Automata, Logics, and Formal Verification, Gandalf'22, Madrid, Spain, 2022 vol. 370 of Elect. Proc. in Theor. Computer Science, pages 17–33 |
| F. Bruse, M. Lange, E. Lozes, “ : The Tail-Recursive Fragment of Timed Recursive CTL,” In Proceedings of the 29th International Symposium on Temporal Representation and Reasoning, TIME'22, online, 2022 vol. 247 of LIPIcs, pages 5:1–5:16 | |
| F. Bruse, M. Herwig, M. Lange : A Similarity Measure for Formal Languages Based on Convergent Geometric Series In Proceedings of the 26th International Conference on Implementation and Application of Automata, CIAA'22, Rouen, France, 2022 vol. 13266 of Lecture Notes in Computer Science, pp. 80–92, Springer | |
| M. Herwig, N. Hundeshagen, M. Lange Towards Graphical Feedback in the DiMo Learning Tool Formal Methods Education Online: Tips, Tricks & Tools, FOMEO'22, Haifa, IL, 2022 | |
| F. Bruse, J. Kreiker, M. Lange, M. Sälzer : Local Higher-Order Fixpoint Iteration Information and Computation 289(B):104963, special issue on GandALF'20, 2022 | |
| 2021 | M. Sälzer, M. Lange , “Reachability Is NP-Complete Even for the Simplest Neural Networks” , In Proceedings of the 15th International Conference on Reachability Problems, RP'21, Liverpool, UK, 2021, vol. 13035 of Lecture Notes in Computer Science, pp. 149–164, Springer Abstract |
| F. Bruse, M. Lange, M. Sälzer Finite Convergence of Mu-Calculus Fixpoints on Genuinely Infinite Structures In Proceedings of the 46th International Symposium on Mathematical Foundations of Computer Science, MFCS'21, Tallinn, EE, 2021, vol. 202 of LIPIcs, pp. 24:1–24:19 Link | |
| F. Bruse, M. Lange,“ : Model Checking Timed RecursiveCTL ” In Proceedings of the 28th International Symposium on Temporal Representation and Reasoning, TIME’21, Klagenfurt, Austria, 2021, vol. 206 of LIPIcs, pp. 12:1–12:14 Link | |
| F. Bruse, M. Lange : A Decidable Non-Regular Modal Fixpoint Logic To appear in the Proceedings of the 32nd International Conference on Concurrency Theory, CONCUR'21, Paris, France, 2021, vol. 203 of LIPIcs, pages 23:1–23:18 Link | |
| N. Hundeshagen, M. Lange, G. Siebert DiMo - Discrete Modelling Using Propositional Logic In Proceedings of the 24th International Conference on Theory and Applications of Satisfiability Testing, SAT'21, Barcelona, ES, 2021, vol. 12831 of Lecture Notes in Computer Science, pp. 242–250, Springer Abstract | |
| N. Hundeshagen, M. Lange A Proposal for a Framework to Accompany Learning Tools In Proceedings of the Formal Methods Teaching Workshop and Tutorial, FMTea'21, Beijing, CN, 2021, vol. 13122 of Lecture Notes in Computer Science, pp. 35–42, Springer | |
| E. Alsmann, F. Bruse, M. Lange Separating the Expressive Power of Propositional Dynamic and Modal Fixpoint Logics In Proceedings of the Combined 28th Int. Workshop on Expressiveness in Concurrency and 18th Workshop on Structural Operational Semantics, EXPRESS/SOS'21, Paris, F, 2021, vol. 339 of Electr. Proc. in Theor. Comp. Science, pp. 10–26 Link | |
| M. Sälzer, G. Siebert Towards Learning From Graph-Representable Formal Models OVERLAY@GandALF 2021 | |
| F. Bruse, M. Lange Temporal logic with recursion Information and Computation 281 (2021) | |
| F. Bruse, M. Lange, E. Lozes The Complexity of Model-Checking Tail-Recursive Higher-Order Fixpoint Logic Fundamenta Informaticae 178(1-2) (2021) | |
| 2020 | D. Kernberger, M. Lange On the Expressive Power of Hybrid Branching-Time Logics Theoretical Computer Science 813:362-374, 2020 |
| D. Kernberger, M. Lange Model Checking for Hybrid Branching-Time Logics Journal of Logic and Algebraic Programming 110, special issue on TIME'16, 2020 | |
| M. Kastaun, M. Meier, N. Hundeshagen, M. Lange ProfiLL: Professional Development through Intelligent Teaching and Learning Systems In Education, School, Digitalization, Waxmann-Verlag, 2020 | |
| F. Bruse, J. Kreiker, M. Lange, M. Sälzer Local Higher-Order Fixpoint Iteration In Proc. of the 11th Int. Symp. on Games, Automata, Logics and Formal Verification, Gandalf'20, Brussels, BE, 2020 vol. 326 of Elect. Proc. in Theor. Computer Science, pp. 97–113 | |
| F. Bruse, M. Lange Temporal Logic with Recursion In Proceedings of the 27th International Symposium on Temporal Representation and Reasoning, TIME'20, Bolzano, IT, 2020 vol. 178 of LIPIcs, pages 6:1–6:14 | |
| P. Gawrychowski, M. Lange, N. Rampersad, J. Shallit, M. Szykuła Existential Length Universality In Proceedings of the 37th Symposium on Theoretical Aspects of Computer Science, STACS'20, Montpellier, France, 2020 vol. 154 of LIPIcs, pages 16:1–16:14 | |
| F. Bruse , “Extremal Fixpoints for Higher-Order Modal Logic.” Kassel, Germany, 2018 , Ph.D. dissertation, 2020 | |
| 2019 | Martin Lange Specifying Program Properties Using Modal Fixpoint Logics: A Survey of Results ICLA 2019: 42–51 |
| Christoph Eickhoff, Martin Lange, Simon-Lennert Raesch, Albert Zündorf EMFeR: Model Checking for Object-Oriented (EMF) Models MODELSWARD 2019: 511–518 | |
| Klaus David, Kurt Geihs, Martin Lange, Gerd Stumme INFORMATIK 2019: 50 Years of the German Informatics Society—Informatics for Society, September 23–26, 2019, Kassel, Germany LNI P-294, GI 2019, ISBN 978-3-88579-688-6 | |
| Claude Draude, Martin Lange, Bernhard Sick INFORMATIK 2019: 50 Years of the German Informatics Society—Informatics for Society (Workshop Papers), September 23–26, 2019, Kassel, Germany LNI P-295, GI 2019, ISBN 978-3-88579-689-3 | |
| 2018 | D. Kernberger, M. Lange Model Checking for Hybrid Branching-Time Logics To appear in the Journal of Logic and Algebraic Programming, special issue on TIME'16, 2018 |
| M. Hutagalung, N. Hundeshagen, D. Kuske, M. Lange, E. Lozes Multi-Buffer Simulations: Decidability and Complexity Information and Computation 262(2):280-310, special issue on GandALF'16, 2018 | |
| D. Kernberger, M. Lange On the Expressive Power of Hybrid Branching-Time Logics In Proceedings of the 25th International Symposium on Temporal Representation and Reasoning, TIME'18, Warsaw, PL, 2018, vol. 120 of LIPIcs, pp. 16:1–16:18 | |
| F. Bruse, M. Lange, E. Lozes Collapses of Fixpoint Alternation Hierarchies in Low Type-Levels of Higher-Order Fixpoint Logic Workshop on Programming and Reasoning on Infinite Structures, PARIS'14, Oxford, UK, 2018 | |
| 2017 | D. Kernberger, M. Lange The Fully Hybrid μ-Calculus In Proceedings of the 24th International Symposium on Temporal Representation and Reasoning, TIME'17, Mons, BE, 2017, vol. 90 of LIPIcs, pages 17:1–17:16 |
| N. Hundeshagen, M. Lange Model Checking CTL Over Restricted Classes of Automatic Structures In Proceedings of the 11th International Workshop on Reachability Problems, RP'17, Egham, UK, 2017, vol. 10506 of Lecture Notes in Computer Science, pages 87–100, Springer | |
| F. Bruse, M. Lange, E. Lozes Space-Efficient Fragments of Higher-Order Fixpoint Logic In Proceedings of the 11th International Workshop on Reachability Problems, RP'17, Egham, UK, 2017, vol. 10506 of Lecture Notes in Computer Science, pp. 26–41, Springer | |
| A. Ehle, N. Hundeshagen, M. Lange Automated Reasoning in the Sequent Calculus Trainer In Proceedings of the Workshop on Theorem Proving Components for Educational Software, Gothenburg, Sweden, 2017 | |
| M. Hutagalung , “Topological Characterization of Multi-Buffer Simulation,” , in Proceedings of the Reachability Problem—11th International Workshop, London, UK, 2017, vol. 10506 of Lecture Notes in Computer Science, pp. 101–117 | |
| 2016 | S. Demri, V. Goranko, M. Lange Temporal Logics in Computer Science (Finite-State Systems) Cambridge Tracts in Theoretical Computer Science, Cambridge University Press, 2016, ~750 pages, ISBN 9781107028364 |
| D. Kernberger, M.Lange , “Model Checking for the Full Hybrid Computation Tree Logic,” , In Proceedings of the 23rd International Symposium on Temporal Representation and Reasoning, TIME’16, , Copenhagen, DK, 2016, IEEE Computer Society | |
| M. Hutagalung, N. Hundeshagen, D. Kuske, M. Lange, E. Lozes Multi-Buffer Simulations for Trace Language Inclusion In Proceedings of the 7th International Symposium on Games, Automata, Logics, and Formal Verification, Gandalf'16, Catania, IT, 2016 vol. 226 of Elect. Proceedings in Theoretical Computer Science, pp. 120–134 | |
| F. Bruse, D. Kernberger, M. Lange A Canonical Model Construction for Iteration-Free PDL with Intersection In Proceedings of the 7th International Symposium on Games, Automata, Logics, and Formal Verification, Gandalf'16, Catania, IT, 2016 vol. 226 of Elect. Proc. in Theor. Computer Science, pp. 213–227 | |
| M. Hutagalung, N. Hundeshagen, D. Kuske, M. Lange, E. Lozes Two-Buffer Simulation Games In Proceedings of the CASSTING'16 Workshop, Eindhoven, NL, 2016 vol. 220 of Electronic Proceedings in Theoretical Computer Science, pp. 27–38 | |
| 2015 | O. Friedmann, F. Klaedtke, M. Lange , “Ramsey-based Inclusion Checking for Visibly Pushdown Automata,” , ACM Transactions on Computational Logic 16(4):34.1–34.24, 2015 |
| F. Grandi, M. Lange, A. Lomuscio (eds.) 22nd International Symposium on Temporal Representation and Reasoning, TIME'15 Kassel, Germany, September 23–25, 2015 IEEE Computer Society | |
| M. Lange, E. Lozes, “ : Conjunctive Visibly-Pushdown Path Queries,” , in Proceedings of the 20th International Symposium on Fundamentals of Computation Theory, FCT’15, Gdańsk, Poland, 2015, , vol. 9210 of LNCS, pp. 327–338, Springer | |
| A. Ehle, N. Hundeshagen, M. Lange The Sequent Calculus Trainer—Helping Students to Correctly Construct Proofs In Proceedings of the 4th International Conference on Tools for Teaching Logic, TTL'15, Rennes, FR, 2015 | |
| M. Lange , “The Arity Hierarchy in the Polyadic µ-Calculus,” , in Proceedings of the 11th Workshop on Fixpoints in Computer Science, FICS’15, Berlin, Germany, 2015, , vol. 191 of Electronic Proceedings in Theoretical Computer Science, pp. 105–116 | |
| M. Folschette, L. Pauleve, M. Magnin, O. Roux : Sufficient Conditions for Reachability in Automata Networks with Priorities Theoretical Computer Science, special edition “From Computer Science to Biology and Back,” 608(1): 66–83, 2015 | |
| E. B. Abdallah, M. Folschette, O. Roux, M. Magnin , “Exhaustive Analysis of Dynamical Properties of Biological Regulatory Networks with Answer Set Programming,” , in Proceedings of the IEEE International Conference on Bioinformatics and Biomedicine, BIBM’15, Washington, USA, 2015, , pp. 281–285, IEEE | |
| 2014 | M. Lange, E. Lozes Capturing Bisimulation-Invariant Complexity Classes with Higher-Order Modal Fixpoint Logic In Proceedings of the 8th IFIP International Conference on Theoretical Computer Science, TCS'14, Rome, Italy, 2014 vol. 8705 of LNCS, pp. 90–103, Springer |
| F. Bruse Alternating Parity Krivine Automata In Proceedings of the 39th International Symposium on Mathematical Foundations of Computer Science, MFCS'14, Budapest, HU, 2014 vol. 8634 of LNCS, pp. 111–122 | |
| N. Hundeshagen, P. Leupold Transducing by observing length-reducing and painter rules RAIRO - Theor. Inf. and Applic. 48(1): 85–105, 2014 | |
| N. Hundeshagen, F. Otto, “ : Restarting Transducers, Regular Languages, and Rational Relations,” , Theory of Computing Systems 1432–4350: 1–31, 2014 | |
| R. Ehlers, U. Topcu Resilience to Intermittent Assumption Violations in Reactive Synthesis In Proceedings of the 17th International Conference on Hybrid Systems: Computation and Control, HSCC'14, Berlin, Germany, 2014 pp. 203–212, ACM | |
| R. Ehlers, S. A. Seshia, H. Kress-Gazit, “ -Synthesis with Identifiers” , 15th International Conference on Verification, Model Checking, and Abstract Interpretation, VMCAI’14 , vol. 8318 of LNCS, pp. 415–433, Springer | |
| F. Bruse, M. Falk, M. Lange The Fixpoint-Iteration Algorithm for Parity Games In Proc. of the 5th Int. Symp. on Games, Automata, Logics and Formal Verification, Gandalf'14, Verona, IT, 2014 vol. 161 of Elect. Proc. in Theor. Computer Science, pp. 116–130, 2013 | |
| M. Hutagalung, M. Lange, E. Lozes Buffered Simulation Games for Büchi Automata In Proceedings of the 14th International Conference on Automata and Formal Languages, AFL'14, Szeged, Hungary, 2014 vol. 151 of Elect. Proc. in Theor. Computer Science, pp. 286–300, 2014 | |
| M. Latte, M. Lange Branching-Time Logics with Path Relativization Journal of Computer and System Sciences 80(2):375–389, special issue on WoLLIC’10, 2014 | |
| F. Bruse, O. Friedmann, M. Lange On Guarded Transformation in the Modal µ-Calculus Logic Journal of the IGPL 23(2): 194–216, 2014 | |
| M. Lange, E. Lozes, M. Vargas Guzman , “Model Checking Process Equivalences,” * Theoretical Computer Science* 560(3):326–347, special issue on GandALF’12, 2014 | |
| J. Gutierrez, F. Klaedtke, M. Lange : The µ-Calculus Alternation Hierarchy Collapses over Structures with Bounded Connectivity , Theoretical Computer Science 560(3):292–306, special issue on GandALF'12, 2014 | |
| R. Ehlers, M. Lange , “A Tool That Incrementally Approximates Finite Satisfiability in Full Interval Temporal Logic,” , in Proceedings of the 7th International Joint Conference on Automated Reasoning (IJCAR'14), Vienna, Austria, 2014, , vol. 8562 of LNCS, pp. 360–366, Springer | |
| M. Hutagalung, M. Lange , “Model Checking for String Problems ,” in Proceedings of the 9th International Computer Science Symposium in Russia, CSR’14, Moscow, RU, 2014, , vol. 8476 of LNCS, pp. 190–203, Springer | |
| 2013 | O. Friedmann, M. Lange Deciding the Unguarded Modal µ-Calculus Journal of Applied Non-Classical Logics 23(4):353–371, 2013 |
| O. Friedmann, M. Latte, M. Lange , “Satisfiability Games for Branching-Time Logics,” , *Logical Methods in Computer Science* 9(4:5), 2013 | |
| O. Friedmann, F. Klaedtke, M. Lange , “Ramsey Goes Visibly Pushdown” , in Proceedings of the 40th International Conference on Algorithms, Languages, and Programming (ICALP’13), Riga, Latvia , vol. 7966 of LNCS, pp. 224–237, Springer, 2013 | |
| M. Hutagalung, M. Lange, E. Lozes, “ : Revealing vs. Concealing,” More Simulation Games for Büchi Inclusion In Proceedings of the 7th International Conference on Language and Automata Theory and Applications, LATA'13, Bilbao, ES, 2013 vol. 7810 of LNCS, pp. 347–358, 2013, Springer | |
| 2012 | E. Lozes, J. Villard , “Reliable Contracts for Unreliable Half-Duplex Communications,” , revised selected papers from the 8th International Workshop on Web Services and Formal Methods, WS-FM'11, , vol. 7176 of LNCS, pp. 2–16, Springer, 2012 |
| J. Gutierrez, F. Klaedtke, M. Lange : The µ-Calculus Alternation Hierarchy Collapses over Structures with Bounded Connectivity In Proceedings of the 3rd Symposium on Games, Automata, Logics, and Formal Verification, GandALF'12, Naples, Italy, 2012 vol. 96 of Electronic Proceedings in Theoretical Computer Science, pp. 113–126 | |
| M. Lange, E. Lozes, M. Vargas Guzman Model Checking Process Equivalences In Proc. of the 3rd Symp. on Games, Automata, Logics and Formal Verification, GandALF'12, Naples, IT, 2012 , vol. 96 of Electronic Proceedings in Theoretical Computer Science, pp. 43–56 | |
| K. Heljanko, M. Keinänen, M. Lange, I. Niemelä Solving Parity Games by a Reduction to SAT Journal of Computer and System Sciences 78:430–440, special issue on Games in Verification, 2012 | |
| M. Latte, M. Lange , “Branching Time? Pruning Time!” In Proc. of the 6th Int. Joint Conf. on Automated Reasoning, IJCAR'12, Manchester, UK, 2012 vol. 7364 of LNCS, pp. 393–407, 2012, Springer | |
| O. Friedmann, M. Lange , “Ramsey-Based Analysis of Parity Automata,” , In Proceedings of the 18th International Conference on Tools and Algorithms for the Construction and Analysis of Systems, TACAS’12, Tallinn, EST, 2012, , vol. 7214 of LNCS, pp. 64–78, 2012, Springer | |
| M. Lange, E. Lozes, “ : Model Checking the Higher-Dimensional Modal µ-Calculus,” In Proceedings of the 8th Workshop on Fixpoints in Computer Science, FICS'12, Tallinn, Estonia, 2012 , vol. 77 of Electronic Proceedings in Theoretical Computer Science, pp. 39–46 | |
| F. Jacquemard, E. Lozes, R. Treinen, J. Villard : Multiple Congruence Relations, First-Order Theories on Terms, and the Frames of the Applied Pi-Calculus : Revised Selected Papers of the Workshop on Theory of Security and Applications, TOSCA'11 , vol. 6993 of LNCS, pp. 166–185, Springer, 2012 | |
| 2011 | B. Badban, M. Lange Exact Incremental Analysis of Timed Automata Using an SMT Solver In Proceedings of the 9th International Conference on Formal Modeling and Analysis of Timed Systems, FORMATS'11, Aalborg, DK, 2011 vol. 6919 of LNCS, pp. 177–192, Springer |
| M. Lange, “ , Size-Change Termination, and Satisfiability for Linear-Time Temporal Logics,” , in Proceedings of the 8th International Symposium on Frontiers of Combining Systems, FroCoS’11, Saarbrücken, Germany, 2011, , vol. 6989 of LNCS, pp. 28–39, Springer | |
| R. Axelsson, M. Lange , “Formal Language Constrained Reachability and Model Checking of Propositional Dynamic Logics,” , in Proceedings of the 5th Workshop on Reachability Problems, RP’11, Genoa, Italy, 2011, , vol. 6945 of LNCS, pp. 45–57, Springer | |
| O. Friedmann, M. Lange The Modal µ-Calculus Caught Off Guard In Proc. of the 20th Int. Conf. on Automated Reasoning with Analytic Tableaux and Related Methods, TABLEAUX'11, Bern, CH, 2011 vol. 6793 of LNCS, pp. 149–163, 2011, Springer | |
| M. Lange P-Hardness of the Emptiness Problem for Visibly Pushdown Languages Information Processing Letters 111(7):338–341, 2011 | |
| 2010 | R. Axelsson, M. Hague, S. Kreutzer, M. Lange, M. Latte , “Extended Computation Tree Logic” , In Proceedings of the 17th International Conference on Programming, Artificial Intelligence, and Reasoning (LPAR’10), Yogyakarta, Indonesia, 2010, “ ,” Vol. 6397 of LNCS, pp. 67–81, Springer |
| O. Friedmann, M. Lange : Local Strategy Improvement for Parity Game Solving In Proceedings of the 1st International Symposium on Games, Automata, Logics, and Formal Verification, GandALF'10, Minori, IT, 2010 vol. 25 of Electronic Notes in Theoretical Computer Science, pp. 118–131, 2010 | |
| O. Friedmann, M., Latte, M., and Lange : A Decision Procedure for CTL* Based on Tableaux and Automata In Proceedings of the 5th International Joint Conference on Automated Reasoning, IJCAR'10, Edinburgh, UK, 2010 , vol. 6173 of Lecture Notes in Artificial Intelligence, pp. 331–345, Springer | |
| C. Dax, F. Klaedtke, M. Lange On Regular Temporal Logics with Past *Acta Informatica* 47(4):251–277, 2010 | |
| M. Lange, M. Latte , “A CTL-Based Logic for Program Abstractions ,” in Proceedings of the 17th International Workshop on Logic, Language, Information, and Computation (WoLLIC’10), Brasília, Brazil, 2010, , vol. 6188 of Lecture Notes in Artificial Intelligence, pp. 19–33, Springer |