DBLP    Google Scholar    ORCID    arXiv    ResearchGate

Edited proceedings

  • Model Checking Software - 29th International Symposium, SPIN 2023, together with G. Caltais. [doi] [bib]

Book chapters

Conference publications

  • Safety verification of decision-tree policies in continuous time, at NeurIPS 2023, together with A. Lukina, E. Demirović, and K. G. Larsen. Spotlight (top 3%) [pdf] [bib] [slides] [poster] [video] [open review]
  • Shielded reinforcement learning for hybrid systems, at (A)ISoLA 2023, together with A. H. Brorholt, P. G. Jensen, K. G. Larsen, and F. Lorber. [doi] [pdf] [bib]
  • The inverse problem for neural networks, at (A)ISoLA 2023, together with M. Forets. [doi] [pdf] [bib] [slides]
  • Open- and closed-loop neural network verification using polynomial zonotopes, at NFM 2023, together with N. Kochdumper, M. Althoff, and S. Bak. [doi] [pdf] [bib]
  • symQV: Automated symbolic verification of quantum programs, at FM 2023, together with F. Bauer-Marquart and S. Leue. [doi] [pdf] [bib] [slides]
  • Synthesis of parametric hybrid automata from time series, at ATVA 2022, together with M. García Soto and T. A. Henzinger. [doi] [pdf] [bib]
  • SpecRepair: Counter-example guided safety repair for deep neural networks, at SPIN 2022, together with F. Bauer-Marquart, D. Boetius, and S. Leue. [doi] [pdf] [bib]
  • Conservative time discretization: A comparative study, at iFM 2022, together with M. Forets. [doi] [pdf] [bib] [slides]
  • Verification of neural-network control systems by integrating Taylor models and zonotopes, at AAAI 2022, together with M. Forets and S. Guadalupe. [doi] [pdf] [bib] [slides] [poster] [video]
  • Reachability of weakly nonlinear systems using Carleman linearization, at RP 2021, together with M. Forets. [doi] [pdf] [bib]
  • Into the unknown: Active monitoring of neural networks, at RV 2021, together with A. Lukina and T. A. Henzinger. [doi] [pdf] [bib] [Watch on Youtube]
  • Synthesis of hybrid automata with affine dynamics from time-series data, at HSCC 2021, together with M. García Soto and T. A. Henzinger. [doi] [pdf] [bib] [Watch on Youtube]
  • Efficient reachability analysis of parametric linear hybrid systems with time-triggered transitions, at MEMOCODE 2020, together with M. Forets and D. Freire. [doi] [pdf] [bib] [Watch on Youtube]
  • Outside the box: Abstraction-based monitoring of neural networks, at ECAI 2020, together with T. A. Henzinger and A. Lukina. [doi] [pdf] [bib] [slides]
  • Membership-based synthesis of linear hybrid automata, at CAV 2019, together with M. García Soto, T. A. Henzinger, and L. Zeleznik. [doi] [pdf] [bib] [slides]
  • JuliaReach: A toolbox for set-based reachability, at HSCC 2019, together with S. Bogomolov, M. Forets, G. Frehse, and K. Potomkin. [doi] [extended version] [bib]
  • Semantic fault localization and suspiciousness ranking, at TACAS 2019, together with M. Christakis, M. Heizmann, M. N. Mansur, and V. Wüstholz. [doi] [pdf] [bib]
  • Reach set approximation through decomposition with low-dimensional sets and high-dimensional matrices, at HSCC 2018, together with S. Bogomolov, M. Forets, G. Frehse, A. Podelski, and F. Viry. [doi] [extended version] [bib] [slides]
  • Safety verification of nonlinear hybrid systems based on invariant clusters, at HSCC 2017, together with H. Kong, S. Bogomolov, Y. Jiang, and T. A. Henzinger. [doi] [pdf] [bib]
  • Minimization of visibly pushdown automata using partial Max-SAT, at TACAS 2017, together with M. Heizmann and D. Tischner. [doi] [extended version] [bib] [slides]
  • Abstraction-based parameter synthesis for multiaffine systems, at HVC 2015, together with S. Bogomolov, E. Bartocci, G. Batt, H. Kong, and R. Grosu. [doi] [pdf] [bib]
  • Adaptive moment closure for parameter inference of biochemical reaction networks, at CMSB 2015, together with S. Bogomolov, T. A. Henzinger, A. Podelski, and J. Ruess. [doi] [pdf] [bib] [slides]
  • Runtime verification for hybrid analysis tools, at RV 2015, together with L. V. Nguyen, S. Bogomolov, and T. T. Johnson. [doi] [pdf] [bib]
  • Implementations of two algorithms for the threshold synthesis problem, at ISAIM 2012, together with J.-G. Smaus and F. Wenzelmann. [pdf] [bib]

Journal articles

  • RangeEnclosures.jl: A framework to bound function ranges, in Proceedings of the JuliaCon Conferences 2024, together with L. Ferranti and M. Forets. [doi] [pdf] [open review]
  • Verified propagation of imprecise probabilities in non-linear ODEs, in IJAR 2023, together with A. Gray, M. Forets, S. Ferson, and L. Benet. [doi] [bib]
  • Into the unknown: Active monitoring of neural networks (extended version), special issue in STTT 2023, together with K. Kueffner, A. Lukina, and T. A. Henzinger. [doi] [bib]
  • Decomposing reach set computations with low-dimensional sets and high-dimensional matrices, special issue in Information and Computation 2022, together with S. Bogomolov, M. Forets, G. Frehse, and A. Podelski. [doi] [bib]
  • LazySets.jl: Scalable symbolic-numeric set computations, in Proceedings of the JuliaCon Conferences 2021, together with M. Forets. [doi] [pdf] [open review]
  • Reachability analysis of linear hybrid systems via block decomposition, in TCAD 2020, special issue for EMSOFT 2020, together with S. Bogomolov, M. Forets, G. Frehse, and K. Potomkin. [doi] [pdf] [bib] [slides] [Watch on Youtube]
  • Hybrid automata: From verification to implementation, in STTT 2017, together with S. Bak, O. A. Beg, S. Bogomolov, T. T. Johnson, and L. V. Nguyen. [doi] [pdf] [bib]
  • Adaptive moment closure for parameter inference of biochemical reaction networks, in Biosystems 2016, together with S. Bogomolov, T. A. Henzinger, A. Podelski, and J. Ruess. [doi] [bib]

Workshop & tutorial publications

  • TaylorModels.jl: Taylor models in Julia and their application to validated solutions of ODEs, at SWIM 2019, together with L. Benet, M. Forets, and D. P. Sanders. [pdf] [bib]
  • Discrete abstraction of multiaffine systems, at HSB 2016, together with H. Kong, E. Bartocci, S. Bogomolov, R. Grosu, T. A. Henzinger, and Y. Jiang. [doi] [pdf] [bib]
  • Tutorial: Software tools for hybrid systems verification, transformation, and synthesis: C2E2, HyST, and TuLiP, at CCA 2016 (tutorial), together with many people. [doi] [pdf] [bib]
  • High-level hybrid systems analysis with Hypy, at ARCH 2016, together with S. Bak and S. Bogomolov. best tool paper award [doi] [pdf] [bib]
  • Implementation of two algorithms for the threshold synthesis problem, at FAC 2014, together with J.-G. Smaus and F. Wenzelmann. [pdf]
  • A pretty complete combinatorial algorithm for the threshold synthesis problem, at IWOCA 2013, together with J.-G. Smaus and F. Wenzelmann. [doi] [pdf] [bib]

Competition reports

  • ARCH-COMP23 category report: Continuous and hybrid systems with linear continuous dynamics, at ARCH 2023, together with M. Althoff, M. Forets, Y. Li, S. Mitra, M. Wetzlinger, and D. Zhuang. [doi] [pdf]
  • ARCH-COMP23 category report: Continuous and hybrid systems with nonlinear continuous dynamics, at ARCH 2023, together with L. Geretti, J. Alexandre dit Sandretto, M. Althoff, L. Benet, P. Collins, M. Forets, E. Ivanova, Y. Li, S. Mitra, S. Mitsch, M. Wetzlinger, and D. Zhuang. [doi] [pdf]
  • ARCH-COMP23 category report: Artificial intelligence and neural network control systems (AINNCS) for continuous and hybrid systems plants, at ARCH 2023, together with D. Manzanas Lopez, M. Althoff, M. Forets, T. T. Johnson, and T. Ladner. [doi] [pdf]
  • ARCH-COMP22 category report: Continuous and hybrid systems with linear continuous dynamics, at ARCH 2022, together with M. Althoff, M. Forets, and M. Wetzlinger. [doi] [pdf]
  • ARCH-COMP22 category report: Continuous and hybrid systems with nonlinear continuous dynamics, at ARCH 2022, together with L. Geretti, J. Alexandre dit Sandretto, M. Althoff, L. Benet, P. Collins, P. S. Duggirala, M. Forets, E. Kim, S. Mitsch, and M. Wetzlinger. [doi] [pdf]
  • ARCH-COMP22 category report: Artificial intelligence and neural network control systems (AINNCS) for continuous and hybrid systems plants, at ARCH 2022, together with D. Manzanas Lopez, M. Althoff, L. Benet, X. Chen, J. Fan, M. Forets, C. Huang, T. T. Johnson, T. Ladner, W. Li, and Q. Zhu. [doi] [pdf]
  • ARCH-COMP21 category report: Continuous and hybrid systems with linear continuous dynamics, at ARCH 2021, together with M. Althoff, E. Ábrahám, M. Forets, G. Frehse, D. Freire, S. Schupp, and M. Wetzlinger. [doi] [pdf] [bib]
  • ARCH-COMP21 category report: Continuous and hybrid systems with nonlinear continuous dynamics, at ARCH 2021, together with L. Geretti, J. Alexandre dit Sandretto, M. Althoff, L. Benet, A. Chapoutot, P. Collins, P. S. Duggirala, M. Forets, E. Kim, U. Linares, D. P. Sanders, and M. Wetzlinger. [doi] [pdf] [bib]
  • ARCH-COMP21 category report: Artificial intelligence and neural network control systems (AINNCS) for continuous and hybrid systems plants, at ARCH 2021, together with T. T. Johnson, D. Manzanas Lopez, L. Benet, M. Forets, S. Guadalupe, R. Ivanov, T. J. Carpenter, J. Weimer, and I. Lee. [doi] [pdf] [bib]
  • ARCH-COMP20 category report: Continuous and hybrid systems with linear continuous dynamics, at ARCH 2020, together with M. Althoff, S. Bak, Z. Bao, M. Forets, G. Frehse, D. Freire, N. Kochdumper, Y. Li, S. Mitra, R. Ray, S. Schupp, and M. Wetzlinger. Best Result award [doi] [pdf] [bib]
  • ARCH-COMP20 category report: Continuous and hybrid systems with nonlinear continuous dynamics, at ARCH 2020, together with L. Geretti, J. Alexandre dit Sandretto, M. Althoff, L. Benet, A. Chapoutot, X. Chen, P. Collins, M. Forets, D. Freire, F. Immler, N. Kochdumper, and D. P. Sanders. Best Result award [doi] [pdf] [bib]
  • ARCH-COMP19 category report: Continuous and hybrid systems with linear continuous dynamics, at ARCH 2019, together with M. Althoff, S. Bak, M. Forets, G. Frehse, N. Kochdumper, R. Ray, and S. Schupp. [doi] [pdf] [bib]
  • ARCH-COMP19 category report: Continuous and hybrid systems with nonlinear dynamics, at ARCH 2019, together with F. Immler, M. Althoff, L. Benet, A. Chapoutot, X. Chen, M. Forets, L. Geretti, N. Kochdumper, and D. P. Sanders. [doi] [pdf] [bib]
  • ARCH-COMP18 category report: Continuous and hybrid systems with linear continuous dynamics, at ARCH 2018, together with M. Althoff, S. Bak, X. Chen, C. Fan, M. Forets, G. Frehse, N. Kochdumper, Y Li, S. Mitra, R. Ray, and S. Schupp. Best friendly competition result award [doi] [bib]
  • MaxSAT evaluation 2018 (Benchmark contribution), at MSE 2018, together with M. Heizmann. [doi] [pdf]
  • Ultimate Automizer and the search for perfect interpolants, at TACAS 2018, together with M. Heizmann, Y.-F. Chen, D. Dietsch, M. Greitschus, J. Hoenicke, Y. Li, A. Nutz, B. Musa, T. Schindler, and A. Podelski. [doi] [bib]
  • Ultimate Taipan with dynamic block encoding, at TACAS 2018, together with D. Dietsch, M. Greitschus, M. Heizmann, J. Hoenicke, A. Nutz, A. Podelski, and T. Schindler. [doi] [bib] [poster]
  • Ultimate Automizer with an on-demand construction of Floyd-Hoare automata, at TACAS 2017, together with M. Heizmann, Y.-W. Chen, D. Dietsch, M. Greitschus, B. Musa, A. Nutz, C. Schätzle, F. Schüssele, and A. Podelski. [doi] [bib]
  • Ultimate Taipan: Trace abstraction and abstract interpretation, at TACAS 2017, together with M. Greitschus, D. Dietsch, M. Heizmann, A. Nutz, C. Schätzle, F. Schüssele, and A. Podelski. [doi] [bib]
  • Ultimate Automizer with unsatisfiable cores, at TACAS 2014, together with M. Heizmann. J. Christ, D. Dietsch, J. Hoenicke, M. Lindenmann, B. Musa, S. Wissert, and A. Podelski. [doi] [bib] [poster]
  • Ultimate Automizer with SMTInterpol, at TACAS 2013, together with M. Heizmann, J. Christ, D. Dietsch, E. Ermis, J. Hoenicke, M. Lindenmann, A. Nutz, and A. Podelski. [doi] [bib]

Extended abstracts

  • Shielded reinforcement learning for hybrid systems, at SYNT 2023, together with A. H. Brorholt, P. G. Jensen, K. G. Larsen, and F. Lorber.
  • Rigorous time evolution of p-boxes in non-linear ODEs, at ESREL 2022, together with A. Gray, M. Forets, L. Benet, and S. Ferson. [pdf] [proceedings]
  • Active monitoring of neural networks, at BNAIC/BeneLearn 2021, together with A. Lukina and T. A. Henzinger. [pdf] [proceedings]
  • HyRG: A random generation tool for affine hybrid automata, at HSCC 2015, together with L. V. Nguyen, S. Bogomolov, and T. T. Johnson. [doi] [pdf] [bib] [poster]

Posters

  • Safety verification of decision-tree policies in continuous time, NeurIPS 2023, together with A. Lukina, E. Demirović, and K. G. Larsen. [poster]
  • Verification of neural-network control systems by integrating Taylor models and zonotopes, AAAI 2022, together with M. Forets and S. Guadalupe. [poster]
  • Semantic fault localization and suspiciousness ranking, at TACAS 2019, together with M. Christakis, M. Heizmann, M. N. Mansur, and V. Wüstholz.
  • Ultimate Automizer, at TACAS 2019, together with M. Heizmann, Y.-F. Chen, D. Dietsch, M. Greitschus, J. Hoenicke, Y. Li, A. Nutz, P. Andrianov, T. Schindler, and A. Podelski. [poster]
  • Ultimate Automizer, at TACAS 2018, together with M. Heizmann, Y.-F. Chen, D. Dietsch, M. Greitschus, J. Hoenicke, Y. Li, A. Nutz, B. Musa, T. Schindler, and A. Podelski. [poster]
  • Ultimate Kojak, at TACAS 2018, together with D. Dietsch, M. Greitschus, M. Heizmann, J. Hoenicke, A. Nutz, and T. Schindler. [poster]
  • Ultimate Taipan, at TACAS 2018, together with D. Dietsch, M. Greitschus, M. Heizmann, J. Hoenicke, A. Nutz, A. Podelski, and T. Schindler. [poster]
  • Ultimate Automizer, at TACAS 2017, together with M. Heizmann, Y.-W. Chen, D. Dietsch, M. Greitschus, A. Nutz, B. Musa, C. Schätzle, F. Schüssele, and A. Podelski. [poster]
  • Cartesian decomposition of linear continuous systems, at Microsoft Research PhD Summer School 2016, together with S. Bogomolov, M. Forets, G. Frehse, and A. Podelski. [poster]
  • HyRG: A random generation tool for affine hybrid automata, at HSCC 2015, together with L. V. Nguyen, S. Bogomolov, and T. T. Johnson. [poster]
  • Ultimate Automizer, at TACAS 2014, together with M. Heizmann, J Christ, D. Dietsch, J. Hoenicke, M. Lindenmann, B. Musa, S. Wissert, and A. Podelski. [poster]

Presentations

Thesis

  • Fundamental techniques for the scalable analysis of systems, Freiburg, 2018. [pdf]