Truth - A verification platform for concurrent systems. - Martin Lange; Martin Leucker; Thomas Noll 001; Stephan Tobies (Tool Support for System Specification, Development and Verification, 1998)

Focus Games for Satisfiability and Completeness of Temporal Logic. - Martin Lange; Colin Stirling (LICS, 2001)

Local Model Checking Games for Fixed Point Logic with Chop. - Martin Lange (CONCUR, 2002)

Model Checking Fixed Point Logic with Chop. - Martin Lange; Colin Stirling (FoSSaCS, 2002)

Alternating Context-Free Languages and Linear Time mu-Calculus with Sequential Composition. - Martin Lange (EXPRESS, 2002)

Model Checking Games for Branching Time Logics. - Martin Lange; Colin Stirling (J. Log. Comput., 2002)

CTL+ Is Complete for Double Exponential Time. - Jan Johannsen; Martin Lange (ICALP, 2003)

Games for modal and temporal logics. - Martin Lange (2003)

A Lower Complexity Bound for Propositional Dynamic Logic with Intersection. - Martin Lange (Advances in Modal Logic, 2004)

Symbolic Model Checking of Non-regular Properties. - Martin Lange (CAV, 2004)

Game Over: The Foci Approach to LTL Satisfiability and Model Checking. - Christian Dax; Martin Lange (GDV@CAV, 2004)

Parallel and Symbolic Model Checking for Fixpoint Logic with Chop. - Martin Lange; Hans-Wolfgang Loidl (PDMC, 2004)

The Complexity of Model Checking Higher Order Fixpoint Logic. - Martin Lange; Rafal Somla (MFCS, 2005)

Don't Know in the µ-Calculus. - Orna Grumberg; Martin Lange; Martin Leucker; Sharon Shoham (VMCAI, 2005)

Weak Automata for the Linear Time µ-Calculus. - Martin Lange (VMCAI, 2005)

Bounded Model Checking for All Regular Properties. - Markus Jehle; Jan Johannsen; Martin Lange; Nicolas Rachinsky (BMC@CAV, 2005)

2-ExpTime lower bounds for propositional dynamic logics with intersection. - Martin Lange; Carsten Lutz (J. Symb. Log., 2005)

A quick axiomatisation of LTL with past. - Martin Lange (Math. Log. Q., 2005)

Bounded Model Checking for Weak Alternating Büchi Automata. - Keijo Heljanko; Tommi A. Junttila; Misa Keinänen; Martin Lange; Timo Latvala (CAV, 2006)

A Proof System for the Linear Time µ-Calculus. - Christian Dax; Martin Hofmann 001; Martin Lange (FSTTCS, 2006)

The alternation hierarchy in fixpoint logic with chop is strict too. - Martin Lange (Inf. Comput., 2006)

Propositional dynamic logic of context-free programs and fixpoint logic with chop. - Martin Lange; Rafal Somla (Inf. Process. Lett., 2006)

Model checking propositional dynamic logic with all extras. - Martin Lange (J. Appl. Log., 2006)

Linear Time Logics Around PSL: Complexity, Expressiveness, and a Little Bit of Succinctness. - Martin Lange (CONCUR, 2007)

Model Checking the First-Order Fragment of Higher-Order Fixpoint Logic. - Roland Axelsson; Martin Lange (LPAR, 2007)

When not losing is better than winning: Abstraction and refinement for the full mu-calculus. - Orna Grumberg; Martin Lange; Martin Leucker; Sharon Shoham (Inf. Comput., 2007)

Three notes on the complexity of model checking fixpoint logic with chop. - Martin Lange (RAIRO Theor. Informatics Appl., 2007)

The Complexity of Model Checking Higher-Order Fixpoint Logic. - Roland Axelsson; Martin Lange; Rafal Somla (Log. Methods Comput. Sci., 2007)

Non-regular fixed-point logics and games. - Stephan Kreutzer; Martin Lange (Logic and Automata, 2008)

Analyzing Context-Free Grammars Using an Incremental SAT Solver. - Roland Axelsson; Keijo Heljanko; Martin Lange (ICALP (2), 2008)

A purely model-theoretic proof of the exponential succinctness gap between CTL+ and CTL. - Martin Lange (Inf. Process. Lett., 2008)

Cut-free sequent systems for temporal logic. - Kai Brünnler; Martin Lange (J. Log. Algebraic Methods Program., 2008)

Solving Parity Games in Practice. - Oliver Friedmann; Martin Lange (ATVA, 2009)

A Note on the Relation between Inflationary Fixpoints and Least Fixpoints of Higher Order. - Stephan Kreutzer; Martin Lange (FICS, 2009)

On the Hybrid Extension of CTL and CTL+. - Ahmet Kara 002; Volker Weber; Martin Lange; Thomas Schwentick (MFCS, 2009)

On the Hybrid Extension of CTL and CTL+ - Ahmet Kara 002; Martin Lange; Thomas Schwentick; Volker Weber (CoRR, 2009)

To CNF or not to CNF? An Efficient Yet Presentable Version of the CYK Algorithm. - Martin Lange; Hans Leiß (Informatica Didact., 2009)

A Solver for Modal Fixpoint Logics. - Oliver Friedmann; Martin Lange (M4M, 2009)

Model Checking for Hybrid Logic. - Martin Lange (J. Log. Lang. Inf., 2009)

Polyadic Dynamic Logics for HPSG Parsing. - Anders Søgaard; Martin Lange (J. Log. Lang. Inf., 2009)

A Decision Procedure for CTL* Based on Tableaux and Automata. - Oliver Friedmann; Markus Latte; Martin Lange (IJCAR, 2010)

Extended Computation Tree Logic. - Roland Axelsson; Matthew Hague; Stephan Kreutzer; Martin Lange; Markus Latte (LPAR (Yogyakarta), 2010)

A CTL-Based Logic for Program Abstractions. - Martin Lange; Markus Latte (WoLLIC, 2010)

On regular temporal logics with past. - Christian Dax; Felix Klaedtke; Martin Lange (Acta Informatica, 2010)

Local Strategy Improvement for Parity Game Solving - Oliver Friedmann; Martin Lange (GANDALF, 2010)

Automatentheorie und Logik. - Martin Hofmann 001; Martin Lange (Springer, 2011)

Exact Incremental Analysis of Timed Automata with an SMT-Solver. - Bahareh Badban; Martin Lange (FORMATS, 2011)

Size-Change Termination and Satisfiability for Linear-Time Temporal Logics. - Martin Lange (FroCoS, 2011)

Formal Language Constrained Reachability and Model Checking Propositional Dynamic Logics. - Roland Axelsson; Martin Lange (RP, 2011)

The Modal μ-Calculus Caught Off Guard. - Oliver Friedmann; Martin Lange (TABLEAUX, 2011)

Tableaux(-like) Methods for the Satisfiability Problems of Temporal Logics. - Martin Lange (TABLEAUX (Workshops, Tutorials, and Short Papers), 2011)

P-hardness of the emptiness problem for visibly pushdown languages. - Martin Lange (Inf. Process. Lett., 2011)

More on balanced diets. - Oliver Friedmann; Martin Lange (J. Funct. Program., 2011)

Branching Time? Pruning Time! - Markus Latte; Martin Lange (IJCAR, 2012)

Ramsey-Based Analysis of Parity Automata. - Oliver Friedmann; Martin Lange (TACAS, 2012)

Model-Checking the Higher-Dimensional Modal mu-Calculus - Martin Lange; Étienne Lozes (FICS, 2012)

Two Local Strategy Iteration Schemes for Parity Game Solving. - Oliver Friedmann; Martin Lange (Int. J. Found. Comput. Sci., 2012)

Solving parity games by a reduction to SAT. - Keijo Heljanko; Misa Keinänen; Martin Lange; Ilkka Niemelä (J. Comput. Syst. Sci., 2012)

Ramsey Goes Visibly Pushdown. - Oliver Friedmann; Felix Klaedtke; Martin Lange (ICALP (2), 2013)

Revealing vs. Concealing: More Simulation Games for Büchi Inclusion. - Milka Hutagalung; Martin Lange; Étienne Lozes (LATA, 2013)

Satisfiability Games for Branching-Time Logics. - Oliver Friedmann; Markus Latte; Martin Lange (Log. Methods Comput. Sci., 2013)

Guarded Transformation for the Modal mu-Calculus - Florian Bruse; Oliver Friedmann; Martin Lange (CoRR, 2013)

Deciding the unguarded modal µ-calculus. - Oliver Friedmann; Martin Lange (J. Appl. Non Class. Logics, 2013)

A Tool That Incrementally Approximates Finite Satisfiability in Full Interval Temporal Logic. - Rüdiger Ehlers; Martin Lange (IJCAR, 2014)

Model Checking for String Problems. - Milka Hutagalung; Martin Lange (CSR, 2014)

Capturing Bisimulation-Invariant Complexity Classes with Higher-Order Modal Fixpoint Logic. - Martin Lange; Étienne Lozes (IFIP TCS, 2014)

The Fixpoint-Iteration Algorithm for Parity Games. - Florian Bruse; Michael Falk; Martin Lange (GandALF, 2014)

Buffered Simulation Games for Büchi Automata. - Milka Hutagalung; Martin Lange; Étienne Lozes (AFL, 2014)

Branching-time logics with path relativisation. - Markus Latte; Martin Lange (J. Comput. Syst. Sci., 2014)

The μ-calculus alternation hierarchy collapses over structures with restricted connectivity. - Julian Gutierrez 001; Felix Klaedtke; Martin Lange (Theor. Comput. Sci., 2014)

Model-checking process equivalences. - Martin Lange; Étienne Lozes; Manuel Vargas Guzmán 001 (Theor. Comput. Sci., 2014)

Conjunctive Visibly-Pushdown Path Queries. - Martin Lange; Étienne Lozes (FCT, 2015)

The Sequent Calculus Trainer - Helping Students to Correctly Construct Proofs. - Arno Ehle; Norbert Hundeshagen; Martin Lange (CoRR, 2015)

The Arity Hierarchy in the Polyadic μ-Calculus. - Martin Lange (FICS, 2015)

On guarded transformation in the modal μ-calculus. - Florian Bruse; Oliver Friedmann; Martin Lange (Log. J. IGPL, 2015)

Ramsey-Based Inclusion Checking for Visibly Pushdown Automata. - Oliver Friedmann; Felix Klaedtke; Martin Lange (ACM Trans. Comput. Log., 2015)

Temporal Logics in Computer Science: Finite-State Systems - Stéphane Demri; Valentin Goranko; Martin Lange (Cambridge University Press, 2016)

Model Checking for the Full Hybrid Computation Tree Logic. - Daniel Kernberger; Martin Lange (TIME, 2016)

A Canonical Model Construction for Iteration-Free PDL with Intersection. - Florian Bruse; Daniel Kernberger; Martin Lange (GandALF, 2016)

Multi-Buffer Simulations for Trace Language Inclusion. - Milka Hutagalung; Norbert Hundeshagen; Dietrich Kuske; Martin Lange; Étienne Lozes (GandALF, 2016)

Two-Buffer Simulation Games. - Milka Hutagalung; Norbert Hundeshagen; Dietrich Kuske; Martin Lange; Étienne Lozes (Cassting/SynCoP, 2016)

Space-Efficient Fragments of Higher-Order Fixpoint Logic. - Florian Bruse; Martin Lange; Étienne Lozes (RP, 2017)

Model Checking CTL over Restricted Classes of Automatic Structures. - Norbert Hundeshagen; Martin Lange (RP, 2017)

The Fully Hybrid mu-Calculus. - Daniel Kernberger; Martin Lange (TIME, 2017)

The Sequent Calculus Trainer with Automated Reasoning - Helping Students to Find Proofs. - Arno Ehle; Norbert Hundeshagen; Martin Lange (ThEdu@CADE, 2017)

22nd International Symposium on Temporal Representation and Reasoning (TIME 2015). - Fabio Grandi 001; Martin Lange; Alessio Lomuscio (Inf. Comput., 2018)

Multi-buffer simulations: Decidability and complexity. - Milka Hutagalung; Norbert Hundeshagen; Dietrich Kuske; Martin Lange; Étienne Lozes (Inf. Comput., 2018)

Specifying Program Properties Using Modal Fixpoint Logics: A Survey of Results. - Martin Lange (ICLA, 2019)

EMFeR: Model Checking for Object Oriented (EMF) Models. - Christoph Eickhoff; Martin Lange; Simon-Lennert Raesch; Albert Zündorf (MODELSWARD, 2019)

Existential Length Universality. - Pawel Gawrychowski; Martin Lange; Narad Rampersad; Jeffrey O. Shallit; Marek Szykula (STACS, 2020)

Local Higher-Order Fixpoint Iteration. - Florian Bruse; Jörg Kreiker; Martin Lange; Marco Sälzer (GandALF, 2020)

Model checking for hybrid branching-time logics. - Daniel Kernberger; Martin Lange (J. Log. Algebraic Methods Program., 2020)

On the expressive power of hybrid branching-time logics. - Daniel Kernberger; Martin Lange (Theor. Comput. Sci., 2020)

A Decidable Non-Regular Modal Fixpoint Logic. - Florian Bruse; Martin Lange (CONCUR, 2021)

Finite Convergence of μ-Calculus Fixpoints on Genuinely Infinite Structures. - Florian Bruse; Marco Sälzer; Martin Lange (MFCS, 2021)

Reachability is NP-Complete Even for the Simplest Neural Networks. - Marco Sälzer; Martin Lange (RP, 2021)

DiMo - Discrete Modelling Using Propositional Logic. - Norbert Hundeshagen; Martin Lange; Georg Siebert (SAT, 2021)

A Proposal for a Framework to Accompany Formal Methods Learning Tools - (Short Paper). - Norbert Hundeshagen; Martin Lange (FMTea, 2021)

Separating the Expressive Power of Propositional Dynamic and Modal Fixpoint Logics. - Eric Alsmann; Florian Bruse; Martin Lange (EXPRESS/SOS, 2021)

The Complexity of Model-Checking Tail-Recursive Higher-Order Fixpoint Logic. - Florian Bruse; Martin Lange; Étienne Lozes (Fundam. Informaticae, 2021)

Temporal logic with recursion. - Florian Bruse; Martin Lange (Inf. Comput., 2021)

The Tail-Recursive Fragment of Timed Recursive CTL. - Florian Bruse; Martin Lange; Étienne Lozes (TIME, 2022)

A Similarity Measure for Formal Languages Based on Convergent Geometric Series. - Florian Bruse; Maurice Herwig; Martin Lange (CIAA, 2022)

We Cannot Guarantee Safety: The Undecidability of Graph Neural Network Verification. - Marco Sälzer; Martin Lange (CoRR, 2022)

Capturing Bisimulation-Invariant Exponential-Time Complexity Classes. - Florian Bruse; David Kronenberger; Martin Lange (GandALF, 2022)

Reachability in Simple Neural Networks. - Marco Sälzer; Martin Lange (Fundam. Informaticae, 2022)

Formal Reasoning About Influence in Natural Sciences Experiments. - Florian Bruse; Martin Lange; Sören Möller (CADE, 2023)

Fundamental Limits in Formal Verification of Message-Passing Neural Networks. - Marco Sälzer; Martin Lange (ICLR, 2023)

On Challenges and Opportunities in the Translation of Deep Neural Networks into Finite Automata. - Marco Sälzer; Eric Alsmann; Martin Lange (OVERLAY@AI*IA, 2023)

The Calculus of Temporal Influence. - Florian Bruse; Marit Kastaun; Martin Lange; Sören Möller (TIME, 2023)

The tail-recursive fragment of timed recursive CTL. - Florian Bruse; Martin Lange (Inf. Comput., 2023)

Problem-Specific Visual Feedback in Discrete Modelling. - Maurice Herwig; Norbert Hundeshagen; John Hundhausen; Stefan Kablowski; Martin Lange (DeLFI, 2024)

Verifying and Interpreting Neural Networks Using Finite Automata. - Marco Sälzer; Eric Alsmann; Florian Bruse; Martin Lange (DLT, 2024)

Computing All Minimal Ways to Reach a Context-Free Language. - Florian Bruse; Martin Lange (RP, 2024)

The Computational Complexity of Formal Reasoning for Encoder-Only Transformers. - Marco Sälzer; Eric Alsmann; Martin Lange (CoRR, 2024)

Model checking timed recursive CTL. - Florian Bruse; Martin Lange (Inf. Comput., 2024)

Weights of formal languages based on geometric series with an application to automatic grading. - Florian Bruse; Maurice Herwig; Martin Lange (Theor. Comput. Sci., 2024)

Transformer Encoder Satisfiability: Complexity and Impact on Formal Reasoning. - Marco Sälzer; Eric Alsmann; Martin Lange (ICLR, 2025)

The Logical Expressiveness of Temporal GNNs via Two-Dimensional Product Logics. - Marco Sälzer; Przemyslaw Andrzej Walega; Martin Lange (CoRR, 2025)

Balancing Privacy and Utility in Correlated Data: A Study of Bayesian Differential Privacy. - Martin Lange; Patricia Guerra-Balboa; Javier Parra-Arnau; Thorsten Strufe (CoRR, 2025)