ORCID    DBLP    arXiv    Google Scholar     ResearchGate

Conference publications

  • Into the unknown: Active monitoring of neural networks, accepted at RV 2021, together with A. Lukina and T. A. Henzinger. [pdf]
  • Synthesis of hybrid automata with linear differential dynamics, in HSCC 2021, together with M. García Soto and T. A. Henzinger. [doi] [pdf] [bib]
  • Efficient reachability analysis of parametric linear hybrid systems with time-triggered transitions, in MEMOCODE 2020, together with M. Forets and D. Freire. [doi] [pdf] [bib] [presentation]
  • Outside the box: abstraction-based monitoring of neural networks, in ECAI 2020, together with T. A. Henzinger and A. Lukina. [doi] [pdf] [bib] [slides]
  • Membership-based synthesis of linear hybrid automata, in 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, in HSCC 2019, together with S. Bogomolov, M. Forets, G. Frehse, and K. Potomkin. [doi] [extended version] [bib]
  • Semantic fault localization and suspiciousness ranking, in 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, in 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, in 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, in TACAS 2017, together with M. Heizmann and D. Tischner. [doi] [extended version] [bib] [slides]
  • Abstraction-based parameter synthesis for multiaffine systems, in HVC 2015, together with S. Bogomolov, E. Bartocci, G. Batt, H. Kong, and R. Grosu. [doi] [bib]
  • Adaptive moment closure for parameter inference of biochemical reaction networks, in CMSB 2015, together with S. Bogomolov, T. A. Henzinger, A. Podelski, and J. Ruess. [doi] [bib] [slides]
  • Runtime verification for hybrid analysis tools, in RV 2015, together with L. V. Nguyen, S. Bogomolov, and T. T. Johnson. [doi] [bib]
  • Implementations of two algorithms for the threshold synthesis problem, in ISAIM 2012, together with J.-G. Smaus and F. Wenzelmann. [pdf] [bib]

Journal articles

  • 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] [presentation] [slides]
  • 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 its application to validated solutions of ODEs, in SWIM 2019, together with L. Benet, M. Forets, and D. P. Sanders. [pdf] [bib]
  • Discrete abstraction of multiaffine systems, in HSB 2016, together with H. Kong, E. Bartocci, S. Bogomolov, R. Grosu, T. A. Henzinger, and Y. Jiang. [doi] [bib]
  • Tutorial: software tools for hybrid systems verification, transformation, and synthesis: C2E2, HyST, and TuLiP, in CCA 2016 (tutorial), together with many people. [doi] [bib]
  • High-level hybrid systems analysis with Hypy, in 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, in FAC 2014, together with J.-G. Smaus and F. Wenzelmann. [pdf]

Competitions

  • ARCH-COMP20 category report: continuous and hybrid systems with linear continuous dynamics, in 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]
  • ARCH-COMP20 category report: continuous and hybrid systems with nonlinear continuous dynamics, in ARCH 2020, together with L. Geretti, J. Alexandre, 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]
  • ARCH-COMP19 category report: continuous and hybrid systems with linear continuous dynamics, in 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, in 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, in 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), in MSE 2018, together with M. Heizmann. [doi] [pdf]
  • Ultimate Automizer and the search for perfect interpolants, in 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, in 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, in 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, in 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, in 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, in TACAS 2013, together with M. Heizmann, J. Christ, D. Dietsch, E. Ermis, J. Hoenicke, M. Lindenmann, A. Nutz, and A. Podelski. [doi] [bib]

Posters

  • Semantic fault localization and suspiciousness ranking, in TACAS 2019, together with M. Christakis, M. Heizmann, M. N. Mansur., and V. Wüstholz.
  • Ultimate Automizer, in 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, in 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, in IWOCA 2013, together with J.-G. Smaus and F. Wenzelmann. [doi] [bib]

Slides

  • Calculus with convex sets in a nutshell, 2019. [slides]
  • Scientific writing in computer science, 2019. [slides]

Thesis

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