Publications
DBLP Google Scholar ORCID arXiv ResearchGate
Edited proceedings
-
AI Verification - 1st International Symposium, SAIV 2024,
together with G. Avni, M. Giacobbe, T. T. Johnson, G. Katz, A. Lukina, and N. Narodytska.
[doi] [bib] -
Model Checking Software - 29th International Symposium, SPIN 2023,
together with G. Caltais.
[doi] [bib]
Conference publications
-
Efficient shielded synthesis via state-space transformations,
accepted at AISoLA 2024,
together with A. H. Brorholt, A. H. Høeg-Petersen, and K. G. Larsen.
[pdf] [slides] -
The reachability problem for neural-network control systems,
at AISoLA 2023 (post-proceedings),
together with M. Zimmermann.
[doi] [pdf] -
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] [open review] -
Shielded reinforcement learning for hybrid systems,
at AISoLA 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 AISoLA 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] -
Simulation relations and applications in formal methods,
in Principles of Systems Design 2022,
together with K. G. Larsen and J. Srba.
[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] [ 
] -
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] [ ] -
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] [ ] -
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] [ ] -
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] [ ] -
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,
special issue 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-COMP24 category report: Continuous and hybrid systems with linear continuous dynamics,
at ARCH 2024,
together with M. Althoff, M. Forets, and M. Wetzlinger.
[doi] [pdf] -
ARCH-COMP24 category report: Continuous and hybrid systems with nonlinear continuous dynamics,
at ARCH 2024,
together with L. Geretti, J. Alexandre dit Sandretto, M. Althoff, L. Benet, P. Collins, M. Forets, S. Mitsch, J. Tillet, and M. Wetzlinger.
[doi] [pdf] -
ARCH-COMP24 category report: Artificial intelligence and neural network control systems (AINNCS) for continuous and hybrid systems plants,
at ARCH 2024,
together with D. Manzanas Lopez, M. Althoff, L. Benet, C. Blab, M. Forets, Y. Jia, T. T. Johnson, M. Kranzl, T. Ladner, L. Linauer, P. Neubauer, S. Neubauer, H. Zhang, and X. Zhong.
[doi] [pdf] -
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] [bib] -
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] [bib] -
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] [bib] -
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] [bib] -
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] [bib] -
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] [bib] -
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
-
Controller synthesis from deep reinforcement learning policies,
at BNAIC/BeNeLearn 2024,
together with F. Delgrange, G. Avni, A. Lukina, A. Nowé, and G. A. Pérez.
[pdf] -
Controller synthesis from deep reinforcement learning policies,
at EWRL 2024,
together with F. Delgrange, G. Avni, A. Lukina, A. Nowé, and G. A. Pérez.
[pdf] -
Controller synthesis from deep reinforcement learning policies,
at MODeM 2024,
together with F. Delgrange, G. Avni, A. Lukina, A. Nowé, and G. A. Pérez.
[pdf] - 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
-
Efficient shielded synthesis via state-space transformations,
AISoLA 2024.
[slides] -
Verification of AI-controlled systems,
Klitgaarden Refugium 2024.
[slides] -
Verification of AI-controlled systems,
University of Konstanz 2024.
[slides] -
Safety verification of decision-tree policies in continuous time,
AAU AI/ML seminar 2024.
[slides] -
To safe AI control systems in three steps,
D3A 2024.
[slides] -
Verification of AI-controlled systems,
DIREC Workshop on Verifiable and Robust AI 2023.
[slides] -
Safety verification of decision-tree policies in continuous time,
AISoLA 2023.
[slides] -
The inverse problem for neural networks,
AISoLA 2023.
[slides] -
Reachability for neural-network control systems,
AISoLA 2023.
[slides] -
Safety verification of decision-tree policies in continuous time,
NeurIPS 2023.
[slides] -
Automatic symbolic analysis of quantum programs,
PhD course at Aalborg University 2023.
[slides] -
Shielded reinforcement learning for hybrid systems,
University of Konstanz 2023.
[slides] -
symQV: Automated symbolic verification of quantum programs,
FM 2023.
[slides] -
Reachability of weakly nonlinear systems using Carleman linearization,
CSE 2023.
[slides] -
Verification of neural-network control systems,
DIREC Seminar 2022.
[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,
ISTA 2019.
[slides] -
Scientific writing in computer science,
ISTA 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]