ORCID    DBLP    Google Scholar     arXiv    ResearchGate

Conference publications

  • Synthesis of parametric hybrid automata from time series, accepted at ATVA 2022, together with M. García Soto and T. A. Henzinger. [pdf]
  • 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 presentation]
  • 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 presentation]
  • 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 presentation]
  • 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 presentation]
  • 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] [bib] [slides]
  • Runtime verification for hybrid analysis tools, at RV 2015, together with L. V. Nguyen, S. Bogomolov, and T. T. Johnson. [doi] [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

  • Decomposing reach set computations with low-dimensional sets and high-dimensional matrices, accepted for a special issue in Information and Computation 2022, together with S. Bogomolov, M. Forets, G. Frehse, and A. Podelski. [doi]
  • LazySets.jl: Scalable symbolic-numeric set computations, in Proceedings of the JuliaCon Conferences 2021, together with M. Forets. [doi] [pdf]
  • 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 presentation]
  • 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] [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]

Competitions

  • 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, P. S. Duggirala, J. Alexandre dit Sandretto, M. Althoff, L. Benet, A. Chapoutot, P. Collins, P. 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]
  • 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]
  • 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

  • Rigorous time evolution of p-boxes in non-linear ODEs, accepted at ESREL 2022, together with A. Gray, M. Forets, L. Benet, and S. Ferson.
  • Active monitoring of neural networks, at BNAIC/BeneLearn 2021, together with A. Lukina and T. A. Henzinger. [pdf] [proceedings]

Posters

  • Verification of neural-network control systems by integrating Taylor models and zonotopes, AAAI 2022. [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.
  • HyRG: A random generation tool for affine hybrid automata, at HSCC 2015, together with L. V. Nguyen, S. Bogomolov, and T. T. Johnson. [doi] [bib]
  • A pretty complete combinatorial algorithm for the threshold synthesis problem, at IWOCA 2013, together with J.-G. Smaus and F. Wenzelmann. [doi] [bib]

Slides

  • Synthesis of hybrid automata, Aalborg University 2022. [slides]
  • A gentle introduction to reachability analysis, Institute for Risk and Uncertainty 2022. [slides]
  • Conservative time discretization: A comparative study, iFM 2022. [slides]
  • Verification of neural-network control systems by integrating Taylor models and zonotopes, AAAI 2022. [slides]
  • Reachability analysis and neural-network controlled systems, Julia Lab 2021. [slides]
  • Reachability analysis of linear hybrid systems via block decomposition, EMSOFT 2020. [slides]
  • Outside the box: Abstraction-based monitoring of neural networks, ECAI 2020. [slides]
  • Calculus with convex sets in a nutshell, IST Austria 2019. [slides]
  • Scientific writing in computer science, IST Austria 2019. [slides]
  • Membership-based synthesis of linear hybrid automata, CAV 2019. [slides]
  • Reach set approximation through decomposition with low-dimensional sets and high-dimensional matrices, HSCC 2018. [slides]
  • Minimization of visibly pushdown automata using partial Max-SAT, TACAS 2017. [slides]
  • Adaptive moment closure for parameter inference of biochemical reaction networks, CMSB 2015. [slides]

Thesis

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