Veröffentlichungen
| 2023 | Alexander Artikis, Florian Bruse, Luke Hunsberger |
| 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 Recursive CTL 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 Proc. of the 30th Int. Symp. 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 Proc. of the 29th Int. Conf. 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 Proc. of the 11th Int. Conf. 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 Proc. 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 Proc. of the 13th Int. Symp. on Games, Automata, Logics and Formal Verification, Gandalf'22, Madrid, E, 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 Proc. of the 29th Int. Symp. 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 Proc. of the 26th Int. Conference on Implementation and Application of Automata, CIAA'22, Rouen, F, 2022 vol. 13266 of Lecture Notes in Computer Science, pages 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 Proc. of the 15th Int. Conference on Reachability Problems, RP'21, Liverpool, UK, 2021 vol. 13035 of Lecture Notes in Computer Science, pages 149-164, Springer Abstract |
| F. Bruse, M. Lange, M. Sälzer Finite Convergence of Mu-Calculus Fixpoints on Genuinely Infinite Structures In Proc. of 46th Int. Symp. on Mathematical Foundations of Computer Science, MFCS'21, Tallin, EE, 2021 vol. 202 of LIPIcs, pages 24:1-24:19 Link | |
| F. Bruse, M. Lange Model Checking Timed Recursive CTL In Proc. of the 28th Int. Symp. on Temporal Representation and Reasoning, TIME'21, Klagenfurt, A, 2021 vol. 206 of LIPIcs, pages 12:1-12:14 Link | |
| F. Bruse, M. Lange A Decidable Non-Regular Modal Fixpoint Logic To appear in Proc. of the 32nd Int. Conf. on Concurrency Theory, CONCUR'21, Paris, F, 2021 vol. 203 of LIPIcs, pages 23:1-23:18 Link | |
| N. Hundeshagen, M. Lange, G. Siebert DiMo - Discrete Modelling Using Propositional Logic In Proc. of the 24th Int. Conf. on Theory and Applications of Satisfiability Testing, SAT'21, Barcelona, ES, 2021 vol. 12831 of Lecture Notes in Computer Science, pages 242-250, Springer Abstract | |
| N. Hundeshagen, M. Lange A Proposal for a Framework to Accompany Learning Tools In Proc. 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 |
D. Kernberger, M. Lange | |
M. Kastaun, M. Meier, N. Hundeshagen, M. Lange | |
F. Bruse, J. Kreiker, M. Lange, M. Sälzer | |
F. Bruse, M. Lange | |
P. Gawrychowski, M. Lange, N. Rampersad, J. Shallit, M. Szykuła | |
F. Bruse | |
| 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 Jahre Gesellschaft für Informatik - Informatik für Gesellschaft, 23.-26.9.2019, Kassel, Deutschland LNI P-294, GI 2019, ISBN 978-3-88579-688-6 | |
| Claude Draude, Martin Lange, Bernhard Sick INFORMATIK 2019: 50 Jahre Gesellschaft für Informatik - Informatik für Gesellschaft (Workshop-Beiträge), 23.-26.9.2019, Kassel, Deutschland 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 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 Proc. of the 25th Int. Symp. on Temporal Representation and Reasoning, TIME'18, Warsaw, PL, 2018 vol. 120 of LIPIcs, pages 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 Proc. of the 24th Int. Symp. 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 Proc. of the 11th Int. 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 Proc. of the 11th Int. Workshop on Reachability Problems, RP'17, Egham, UK , 2017, vol. 10506 of Lecture Notes in Computer Science, pages 26-41, Springer | |
| A. Ehle, N. Hundeshagen, M. Lange Automated Reasoning in the Sequent Calculus Trainer In Proc. of the Workshop on Theorem Proving Components for Educational Software, Gothenburg, S, 2017 | |
| M. Hutagalung Topological Characterisation of Multi-Buffer Simulation In Proc. 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 Proc. of the 23rd Int. Symp. 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 Proc. of the 7th Int. Symp. on Games, Automata, Logics and Formal Verification, Gandalf'16, Catania, IT, 2016 vol. 226 of Elect. Proc. in Theor. Computer Science, pp. 120-134 | |
| F. Bruse, D. Kernberger, M. Lange A Canonical Model Construction for Iteration-Free PDL with Intersection In Proc. of the 7th Int. Symp. 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 Proc. 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, D, September 23-25, 2015 IEEE Computer Society | |
| M. Lange, E. Lozes Conjunctive Visibly-Pushdown Path Queries In Proc. of 20th Int. Symp. on Fundamentals of Computation Theory, FCT'15, Gdansk, PL, 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 Proc. of the 4th Int. Conf. on Tools for Teaching Logic, TTL'15, Rennes, FR, 2015 | |
| M. Lange The Arity Hierarchy in the Polyadic µ-Calculus In Proc. 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 Proc. 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 Proc. of the 8th IFIP Int. Conf. on Theoretical Computer Science, TCS'14, Rome, IT, 2014 vol. 8705 of LNCS, pp. 90-103, Springer |
| F. Bruse Alternating Parity Krivine Automata In Proc. of the 39th Int. Symp. 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 Proc. of the 17th International Conference on Hybrid Systems: Computation and Control, HSCC'14, Berlin, D, 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 Proc. of the 14th Int. Conf. on Automata and Formal Languages, AFL'14, Szeged, H, 2014 vol. 151 of Elect. Proc. in Theor. Computer Science, pp. 286-300, 2014 | |
| M. Latte, M. Lange Branching-Time Logics with Path Relativisation 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 Proc. of the 7th Int. Joint Conf. on Automated Reasoning, IJCAR'14, Vienna, A, 2014 vol. 8562 of LNCS, pp. 360-366, Springer | |
| M. Hutagalung, M. Lange Model Checking for String Problems In Proc. of the 9th Int. Computer Science Symp. 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 Proc. of the 40th Int. Coll. on Algorithms, Languages and Programming, ICALP'13, Riga, LV 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 Proc. of the 7th Int. Conf. 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 of the 8th Int. 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 Proc. of the 3rd Symp. on Games, Automata, Logics and Formal Verification, GandALF'12, Napoli, IT, 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, Napoli, 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 Proc. of the 18th Int. Conf. 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 Proc. 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 Proc. of the 9th Int. Conf. on Formal Modelling 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 Proc. 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 Propositional Dynamic Logics In Proc. of the 5th Workshop on Reachability Problems, RP'11, Genova, 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 Proc. of the 17th Int. Conf. on Programming, Artificial Intelligence and Reasoning LPAR'10, Yogyakarta, RI, 2010 vol. 6397 of LNCS, pp. 67-81, Springer |
| O. Friedmann, M. Lange Local Strategy Improvement for Parity Game Solving In Proc. of the 1st Int. Symp. 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. Lange A Decision Procedure for CTL* Based on Tableaux and Automata In Proc. of the 5th Int. 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 Proc. of the 17th Int. Workshop on Logic, Language, Information and Computation WoLLIC'10, Brasilia, BR, 2010 vol. 6188 of Lecture Notes in Artificial Intelligence, pp. 19-33, Springer |