Ezio Bartocci
Univ.Prof.
Research Focus
- Computer Engineering: 100%
Research Areas
- Formal Methods, Cyber-Physical Systems, Machine Learning, Cybersecurity, Formal verification
About
He is a Full Professor for Formal Methods in Cyber-Physical Systems Engineering at the Faculty of Computer Science TU Wien, and he is leading the Trustworthy Cyber-Physical Systems (TrustCPS) Group of the Cyber-Physical System Research Unit.
Roles
- Curriculum Commission for Computer Engineering
Substitute Member - Faculty Council
Principal Member - Full Professor
Cyber-Physical Systems, E191-01 - Research Focus Coordinator
Computer Engineering
Contact
- ezio.bartocci@tuwien.ac.at
- +43-1-58801-18226
- 1040 Wien, Treitlstrasse 3 / Room DE0324
- vCard from TISS
- www.eziobartocci.com
- orcid.org/0000-0002-8004-6601
- informatics.tuwien.ac.at/people/ezio-bartocci
- tiss.tuwien.ac.at/person/251490
Courses
Summer 2026
- Bachelor Thesis for Computer Science and Business Informatics / 182.715 PR
- Computer Engineering Practical / 191.005 PR
- Computer Engineering Project / 191.006 PR
- GPU Architectures and Computing / 182.731 VU
- Introduction to Logical Methods in Computer Science / 184.766 VO
- PhD Seminar / 191.013 SE
- Project in Computer Science 1 / 191.008 PR
- Project in Computer Science 2 / 191.009 PR
- Research Seminar LogiCS / 184.767 SE
- Scientific Project Computer Engineering / 191.007 PR
- Scientific Research and Writing / 193.052 SE
- Seminar Computer Engineering / 182.760 SE
- Seminar for Master Students in Computer Engineering / 180.778 SE
- Seminar for Master Students in Software Engineering (Computer Engineering) / 180.011 SE
Winter 2025
- Bachelor Thesis for Computer Science and Business Informatics / 182.715 PR
- Computer Engineering Practical / 191.005 PR
- Computer Engineering Project / 191.006 PR
- Internet of Things / 182.753 VU
- Introduction to Logical Methods in Computer Science / 184.766 VO
- Research Seminar LogiCS / 184.767 SE
- Scientific Project Computer Engineering / 191.007 PR
- Scientific Research and Writing / 193.052 SE
- Seminar Computer Engineering / 182.760 SE
- Seminar for Master Students in Computer Engineering / 180.778 SE
- Seminar for PhD students / 182.008 SE
Projects
- 2026 – 2029 / Austrian Science Fund (FWF)
- 2025 – 2029 / Austrian Science Fund (FWF) / Publications (2)
- 2025 – 2028 / European Commission
- 2025 – 2027 / European Commission / Publication
- 2024 – 2025 / TTTech Industrial Automation AG
- 2023 – 2028 / TTTech Auto AG / Publications (3)
- 2023 – 2028 / Vienna Science and Technology Fund (WWTF) / Website / Publications (24)
- 2023 – 2025 / European Commission / Publications (5)
- 2022 – 2026 / Austrian Research Promotion Agency (FFG) / Publication
- 2020 – 2025 / Vienna Science and Technology Fund (WWTF) / Publications (34)
- 2019 – 2024 / Austrian Science Fund (FWF) / Publications (8)
- 2017 – 2020 / Austrian Research Promotion Agency (FFG) / Publication
Publications
2026
- Clement, M.-L., Farsang, M., Stanusoiu, M.-T., Rus, D., Hasani, R., Grosu, R., Bartocci, E. (2026). Evaluating Domain-Shift Generalization of Liquid Neural Networks in Autonomous Driving. In Catch, Adapt, and Operate: Monitoring ML Models Under Drift Workshop. Catch, Adapt, and Operate: Monitoring ML Models Under Drift Workshop, Rio de Janeiro, Brazil. Peer-reviewed.HDL: 20.500.12708/227937 / Project: DK - AR
- Yadav, D., Mandrioli, C., Bartocci, E., Bianculli, D. (2026). Fault Injection for Simulink-based CPS Models: Insights and Future Directions. In 40th IEEE/ACM International Conference on Automated Software Engineering (ASE) (pp. 3834–3839). IEEE. Peer-reviewed.
2025
- Bartocci, E., Chalupa, M., Henzinger, T. A., Ničković, D., Oliveira Da Costa, A. (2025). Hypernode automata. Acta Informatica, 62(4), Article 43. Peer-reviewed.DOI: 10.1007/s00236-025-00509-8 / Project:
- Bartocci, E., Henzinger, T. A., Nickovic, D., Oliveira Da Costa, A. (2025). Information-Flow Interfaces and Security Lattices. In M. Fränzle, J. Niehaus, B. Westphal (Eds.), Engineering Safe and Trustworthy Cyber Physical Systems : Essays Dedicated to Werner Damm on the Occasion of His 71st Birthday (Vol. 15471, pp. 251–263). Springer. Peer-reviewed.DOI: 10.1007/978-3-031-97537-0_15 / Project:
- Chen, H., Zhang, Z., Roy, S., Bartocci, E., Smolka, S. A., Stoller, S., Lin, S. (2025). Cumulative-Time Signal Temporal Logic. ACM Transactions on Embedded Computing Systems, 24(5s), 1–23. Peer-reviewed.DOI: 10.1145/3763237
- Melani, B., Bartocci, E., Chiari, M. (2025). A Tree-Shaped Tableau for Checking the Satisfiability of Signal Temporal Logic with Bounded Temporal Operators. ACM Transactions on Embedded Computing Systems, 24(5s), 1–26. Peer-reviewed.
- Hsu, T.-H., Oliveira Da Costa, A., Wintenberg, A., Bartocci, E., Bonakdarpour, B. (2025). Gray-box runtime enforcement of hyperproperties. Acta Informatica, 62(3), Article 30. Peer-reviewed.
- Pontiggia, F., Bartocci, E., Chiari, M. (2025). POPACheck: A Model Checker for Probabilistic Pushdown Automata. In R. Piskac Z. Rakamaric (Eds.), Computer Aided Verification : 37th International Conference, CAV 2025, Zagreb, Croatia, July 23-25, 2025, Proceedings, Part II (pp. 105–121). Springer. Peer-reviewed.
- Nesterini, E., Bartocci, E., Gambi, A., Nickovic, D., Seshia, S. A., Torfah, H. (2025). Mining Specifications for Predictive Safety Monitoring. In Proceedings of the ACM/IEEE 16th International Conference on Cyber-Physical Systems (with CPS-IoT Week 2025) (pp. 1–11). Association for Computing Machinery. Peer-reviewed.
- Kofnov, A., Bartocci, E., Bura, E. (2025). Moment-based Density Elicitation with Applications in Probabilistic Loops. ACM Transactions on Probabilistic Machine Learning. Peer-reviewed.DOI: 10.1145/3728648 / Project: ProbInG
- Liu, W., Alsalehi, S., Mehdipour, N., Bartocci, E., Belta, C. (2025). Quantifying the Satisfaction of Spatio-Temporal Logic Specifications for Multi-Agent Control. IEEE Transactions on Automatic Control, 1–16. Peer-reviewed.
- Lopez-Miguel, I. D., Adam, S. P., Bartocci, E., Eiter, T., Tappler, M. (2025). OFTEN-DEEPRL: On-the-Fly Teaching of Ethical Norms to Deep Reinforcement Learning Agents. In ECAI 2025 : 28th European Conference on Artificial Intelligence, 25-30 October 2025, Bologna, Italy : Including 14th Conference on Prestigious Applications of Intelligent Systems (PAIS 2025) (pp. 3315–3322). Peer-reviewed.
- Bartocci, E., Mariani, L., Ničković, D., Yadav, D. (2025). Signal Feature Coverage and Testing for CPS Dataflow Models. ACM Transactions on Software Engineering and Methodology. Peer-reviewed.DOI: 10.1145/3714467
- Maderbacher, B., Schupp, S. A., Bartocci, E., Bloem, R., Nickovic, D., Könighofer, B. (2025). An Adaptive, Provable Correct Simplex Architecture. International Journal on Software Tools for Technology Transfer, 1–19. Peer-reviewed.DOI: 10.1007/s10009-025-00779-0 / Project: TAIGER
- Moosbrugger, M., Müllner, J., Bartocci, E., Kovacs, L. (2025). Polar: An Algebraic Analyzer for (Probabilistic) Loops. In Principles of Verification: Cycling the Probabilistic Landscape (Vol. 15260, pp. 179–200). Peer-reviewed.
- Bartocci, E., Desharnais, J., Lindner, P., Sokolova, A. (2025). A Probabilistic Analysis of Simplified Cluedo with Storm: The Birthday Cake Case. In N. Jansen, S. Junges, B. L. Kaminski, C. Matheja, T. Noll, T. Quatmann, M. Stoelinga, M. Volk (Eds.), Principles of Verification: Cycling the Probabilistic Landscape (Vol. 15261, pp. 75–97). Springer. Peer-reviewed.DOI: 10.1007/978-3-031-75775-4_4 / Project: ProbInG
- Tappler, M., Lopez-Miguel, I. D., Tschiatschek, S., Bartocci, E. (2025). Rule-Guided Reinforcement Learning Policy Evaluation and Improvement. In Proceedings of the Thirty-Fourth International Joint Conference on Artificial Intelligence (pp. 6254–6262). Peer-reviewed.DOI: 10.24963/ijcai.2025/696 / Project: TAIGER
- Kofnov, A., Kapla, D. B., Bartocci, E., Bura, E. (2025). Exact Upper and Lower Bounds for the Output Distribution of Neural Networks with Random Inputs. In Proceedings of 42nd International Conference on Machine Learning (pp. 31133–31157). Peer-reviewed.HDL: 20.500.12708/219936 / Project: ProbInG
2024
- Bartocci, E., Essbai, W. (2024). A Comparison of Monitoring Techniques for Deep Neural Networks. In Bridging the Gap Between AI and Reality : Second International Conference, AISoLA 2024, Crete, Greece, October 30 – November 3, 2024, Proceedings. AISoLA 2024: International Conference on Bridging the Gap between AI and Reality, Kreta, Greece. Peer-reviewed.
- Kofnov, A., Moosbrugger, M., Stankovic, M., Bartocci, E., Bura, E. (2024). Exact and Approximate Moment Derivation for Probabilistic Loops With Non-Polynomial Assignments. ACM Transactions on Modeling and Computer Simulation, 34(3), Article 18. Peer-reviewed.
- Indri, P., Blohm, P., Athavale, A., Bartocci, E., Weissenbacher, G., Maffei, M., Nickovic, D., Gärtner, T., Malhotra, S. (2024). Distillation based Robustness Verification with PAC Guarantees. In International Conference on Machine Learning 2024 - Next Generation of AI Safety Workshop. International Conference on Machine Learning 2024 - Next Generation of AI Safety Workshop, Vienna, Austria. Peer-reviewed.HDL: 20.500.12708/200890
- Amrollahi, D., Bartocci, E., Kenison, G. J., Kovacs, L., Moosbrugger, M., Stankovic, M. (2024). (Un)Solvable loop analysis. Formal Methods in System Design. Peer-reviewed.
- Bartocci, E., Ferrère, T., Henzinger, T., Nickovic, D., Oliveira da Costa, A. (2024). Information-flow interfaces. Formal Methods in System Design. Peer-reviewed.
- Amrollahi, D., Bartocci, E., Kenison, G., Kovacs, L., Moosbrugger, M., Stankovič, M. (2024). Correction: (Un)Solvable loop analysis. Formal Methods in System Design.DOI: 10.1007/s10703-024-00465-y / Project: ProbInG
- Bartocci, E. (2024). The PROBING Project: Advancing Automatic Analysis of Probabilistic Loops. In T. Margaria B. Steffen (Eds.), Leveraging Applications of Formal Methods, Verification and Validation. REoCAS Colloquium in Honor of Rocce De Nicola (pp. 152–167). Springer. Invited and peer-reviewed.DOI: 10.1007/978-3-031-73709-1_10 / Project: ProbInG
- Qu, M., He, J., Tucakovic, Z., Bartocci, E., Nickovic, D., Isakovic, H., Grosu, R. (2024). DeepRIoT: Continuous Integration and Deployment of Robotic-IoT Applications. In DAC ’24: Proceedings of the 61st ACM/IEEE Design Automation Conference (pp. 1–6). Peer-reviewed.
- Visconti, E., Bartocci, E., Falcone, Y., Nenzi, L. (2024). Adaptable Configuration of Decentralized Monitors. In V. Castiglioni A. Francalanza (Eds.), Formal Techniques for Distributed Objects, Components, and Systems. FORTE 2024 (pp. 197–217). Springer. Peer-reviewed.
- Stankovic, M., Bartocci, E. (2024). Probabilistic Loop Synthesis from Sequences of Moments. In J. Hillston, S. Soudjani, M. Waga (Eds.), Quantitative Evaluation of Systems and Formal Modeling and Analysis of Timed Systems (pp. 233–248). Peer-reviewed.
- Athavale, A., Bartocci, E., Christakis, M., Maffei, M., Ničković, D., Weissenbacher, G. (2024). Verifying Global Two-Safety Properties in Neural Networks with Confidence. In A. Gurfinkel V. Ganesh (Eds.), Computer Aided Verification (pp. 329–351). Springer. Peer-reviewed.
- Bartocci, E. (2024). Quantifying Uncertainty in Probabilistic Loops Without Sampling: A Fully Automated Approach. In L. Kovacs A. Sokolova (Eds.), Reachability Problems (pp. 3–8). Springer. Peer-reviewed.DOI: 10.1007/978-3-031-72621-7_1 / Project: ProbInG
2023
- Tundo, A., Mobilio, M., Ilager, S. S., Brandic, I., Bartocci, E., Mariani, L. (2023). An Energy-Aware Approach to Design Self-Adaptive AI-based Applications on the Edge. In 2023 38th IEEE/ACM International Conference on Automated Software Engineering (ASE) (pp. 281–293). IEEE. Peer-reviewed.
- Dobe, O., Schupp, S. A., Bartocci, E., Bonakdarpour, B., Legay, A., Pajic, M., Wang, Y. (2023). Lightweight Verification of Hyperproperties. In É. André J. Sun (Eds.), Automated Technology for Verification and Analysis : 21st International Symposium, ATVA 2023, Singapore, October 24–27, 2023, Proceedings, Part II (pp. 3–25). Springer. Peer-reviewed.DOI: 10.1007/978-3-031-45332-8_1 / Project: ZK 35-G
- Aguilar, E. A., Bartocci, E., Mateis, C., Nesterini, E., Nickovic, D. (2023). Mining Specification Parameters for Multi-class Classification. In P. Katsaros L. Nenzi (Eds.), Runtime Verification : 23rd International Conference, RV 2023, Thessaloniki, Greece, October 3–6, 2023, Proceedings (pp. 86–105). Springer. Peer-reviewed.DOI: 10.1007/978-3-031-44267-4_5 / Project: ProbInG
- Garlich, L., Dobe, O., Ábrahám, E., Bartocci, E., Bonakdarpour, B. (2023). Introducing Asynchronicity to Probabilistic Hyperproperties. In N. Jansen M. Tribastone (Eds.), Quantitative Evaluation of Systems : 20th International Conference, QEST 2023, Antwerp, Belgium, September 20–22, 2023, Proceedings (pp. 47–64). IEEE. Peer-reviewed.DOI: 10.1007/978-3-031-43835-6_4 / Project: ProbInG
- Andriushchenko, R., Bartocci, E., Češka, M., Pontiggia, F., Sallinger, S. S. (2023). Deductive Controller Synthesis for Probabilistic Hyperproperties. In N. Jansen M. Tribastone (Eds.), Quantitative Evaluation of Systems - 20th International Conference, QEST 2023 (pp. 47–64). Springer. Peer-reviewed.DOI: 10.1007/978-3-031-43835-6_20 / Project: ProbInG
- He, J., Nickovic, D., Bartocci, E., Grosu, R. (2023). TD-Magic: From Pictures of Timing Diagrams To Formal Specifications. In 2023 60th ACM/IEEE Design Automation Conference (DAC) (pp. 1–6). IEEE. Peer-reviewed.DOI: 10.1109/DAC56929.2023.10247685 / Project: ADEX
- Bartocci, E., Henzinger, T. A., Nickovic, D., Oliveira Da Costa, A. A. (2023). Hypernode Automata. In G. Perez J.-F. Raskin (Eds.), 34th International Conference on Concurrency Theory (CONCUR 2023) (pp. 1–16). Schloss-Dagstuhl - Leibniz Zentrum für Informatik. Peer-reviewed.DOI: 10.4230/LIPIcs.CONCUR.2023.21 / Project: ZK 35-G
- Bartocci, E., Mateis, C., Nesterini, E., Nickovic, D. (2023). Mining Hyperproperties using Temporal Logics. ACM Transactions on Embedded Computing Systems, 22(5s), 1–26. Peer-reviewed.DOI: 10.1145/3609394
- Nenzi, L., Bartocci, E., Bortolussi, L., Silvetti, S., Loreti, M. (2023). MoonLight: a lightweight tool for monitoring spatio-temporal properties. International Journal on Software Tools for Technology Transfer, 25(4), 503–517. Peer-reviewed.DOI: 10.1007/s10009-023-00710-5 / Project: ZK 35-G
- Soldà, D., López Miguel, I. D., Bartocci, E., Eiter, T. (2023). Progression for Monitoring in Temporal ASP. In K. Gal, A. Nowé, G. J. Nalepa, R. Fairstein, R. Rădulescu (Eds.), ECAI 2023 : 26th European Conference on Artificial Intelligence. Including 12th Conference on Prestigious Applications of Intelligent Systems (PAIS 2023). Proceedings (pp. 2170–2177). Frontiers. Peer-reviewed.
- Bartocci, E., Mariani, L., Ničković, D., Yadav, D. (2023). Property-Based Mutation Testing. In 2023 IEEE Conference on Software Testing, Verification and Validation (ICST) (pp. 222–233). IEEE. Peer-reviewed.
- Maderbacher, B., Schupp, S., Bartocci, E., Bloem, R., Ničković, D., Könighofer, B. (2023). Provable Correct and Adaptive Simplex Architecture for Bounded-Liveness Properties. In G. Caltais C. Schilling (Eds.), Model Checking Software. SPIN 2023 (pp. 141–160). Springer Cham. Peer-reviewed.DOI: 10.1007/978-3-031-32157-3_8 / Project: ZK 35-G
2022
- Bartocci, E., Mariani, L., Nickovic, D., Yadav, D. (2022). Search-based Testing for Accurate Fault Localization in CPS. In Proceedings 2022 IEEE 33rd International Symposium on Software Reliability Engineering (ISSRE) (pp. 145–156). Peer-reviewed.
- Bartocci, E., Mariani, L., Ničković, D., Yadav, D. (2022). FIM: fault injection and mutation for Simulink. In ESEC/FSE 2022: Proceedings of the 30th ACM Joint European Software Engineering Conference and Symposium on the Foundations of Software Engineering (pp. 1716–1720). Association for Computing Machinery (ACM). Peer-reviewed.DOI: 10.1145/3540250.3558932 / Download: PDF
- Bartocci, E., Mateis, C., Nesterini, E., Nickovic, D. (2022). Survey on mining signal temporal logic specifications. Information and Computation, 289(Part A), Article 104957. Peer-reviewed.
- Bartocci, E., Bloem, R., Maderbacher, B., Manjunath, M., Ničković, D. (2022). Adaptive testing for specification coverage and refinement in CPS models. NONLINEAR ANALYSIS-HYBRID SYSTEMS, 46, Article 101254. Peer-reviewed.
- Moosbrugger, M., Stankovic, M., Bartocci, E., Kovacs, L. (2022). This Is the Moment for Probabilistic Loops. Proceedings of the ACM on Programming Languages, 6(OOPSLA2), 1497–1525. Peer-reviewed.DOI: 10.1145/3563341
- Karimi, A., Moosbrugger, M., Stankovič, M., Kovács, L., Bartocci, E., Bura, E. (2022). Distribution Estimation for Probabilistic Loops. In E. Ábrahám M. Paolieri (Eds.), Quantitative Evaluation of Systems (pp. 26–42). Springer-Verlag. Peer-reviewed.
- Moosbrugger, M., Bartocci, E., Katoen, J.-P., Kovacs, L. (2022). The probabilistic termination tool amber. Formal Methods in System Design, 61(1), 90–109. Peer-reviewed.
- Bartocci, E., Ferrère, T., Henzinger, T. A., Nickovic, D., Oliveira Da Costa, A. A. (2022). Information-flow Interfaces. In Fundamental Approaches to Software Engineering (pp. 3–22). Springer-Verlag. Peer-reviewed.
- Kofnov, A., Moosbrugger, M., Stankovič, M., Bartocci, E., Bura, E. (2022). Moment-Based Invariants for Probabilistic Loops with Non-polynomial Assignments. In E. Ábrahám M. Paolieri (Eds.), Quantitative Evaluation of Systems (pp. 3–25). Springer. Peer-reviewed.
- Bartocci, E., Putot, S. (Eds.). (2022). 25th ACM International Conference on Hybrid Systems: Computation and Control.DOI: 10.1145/3501710
- He, J., Bartocci, E., Ničković, D., Isakovic, H., Grosu, R. (2022). DeepSTL - From English Requirements to Signal Temporal Logic. In ICSE ’22: Proceedings of the 44th International Conference on Software Engineering (pp. 610–622). Association for Computing Machinery. Peer-reviewed.
- Nenzi, L., Bartocci, E., Bortolussi, L., Loreti, M. (2022). A Logic for Monitoring Dynamic Networks of Spatially-distributed Cyber-Physical Systems. Logical Methods in Computer Science, 18(1), 4:1-4:30. Peer-reviewed.
- Dobe, O., Ábrahám, E., Bartocci, E., Bonakdarpour, B. (2022). Model checking hyperproperties for Markov decision processes. Information and Computation, 289(Part B), Article 104978. Peer-reviewed.
- Dobe, O., Wilke, L., Ábrahám, E., Bartocci, E., Bonakdarpour, B. (2022). Probabilistic Hyperproperties with Rewards. In J. V. Deshmukh, K. Havelund, I. Perez (Eds.), NASA Formal Methods : 14th International Symposium, NFM 2022, Pasadena, CA, USA, May 24–27, 2022, Proceedings (pp. 656–673). Springer. Peer-reviewed.
- Amrollahi, D., Bartocci, E., Kenison, G., Kovács, L., Moosbrugger, M., Stankovič, M. (2022). Solving Invariant Generation for Unsolvable Loops. In Static Analysis: 29th International Symposium, SAS 2022 (pp. 19–43). Peer-reviewed.
- Neufeld, E. A., Bartocci, E., Ciabattoni, A. (2022). On Normative Reinforcement Learning via Safe Reinforcement Learning. In PRIMA 2022: Principles and Practice of Multi-Agent Systems - Proceedings (pp. 72–89).DOI: 10.1007/978-3-031-21203-1_5 / Project:
- Stankovič, M., Bartocci, E., Kovács, L. (2022). Moment-based analysis of Bayesian network properties. Theoretical Computer Science, 903, 113–133. Peer-reviewed.
- Neufeld, E. A., Bartocci, E., Ciabattoni, A., Governatori, G. (2022). Enforcing ethical goals over reinforcement-learning policies. Ethics and Information Technology, 24(4), Article 43. Peer-reviewed.
- Bartocci, E., Ferrère, T., Henzinger, T. A., Nickovic, D., da Costa, A. O. (2022). Flavors of Sequential Information Flow. In Verification, Model Checking, and Abstract Interpretation : 23rd International Conference, VMCAI 2022, Philadelphia, PA, USA, January 16–18, 2022, Proceedings (pp. 1–19). Springer.
2021
- Bartocci, E., Manjunath, N., Mariani, L., Mateis, C., Ničković, D. (2021). CPSDebug: Automatic Failure Explanation in CPS Models. International Journal on Software Tools for Technology Transfer, 23(5), 783–796. Peer-reviewed.
- Bartocci, E., Bender, M. A. (2021). A Perspective on “CCS Expressions, Finite State Processes, and Three Problems of Equivalence.” ACM SIGACT News, 52(4), 76–77. Invited.
- Meiyi, M., Stankovic, J., Bartocci, E., Feng, L. (2021). Predictive Monitoring with Logic-Calibrated Uncertainty for Cyber-Physical Systems. ACM Transactions on Embedded Computing Systems, 20(5s), 1–25. Peer-reviewed.DOI: 10.1145/3477032
- Meiyi, M., Bartocci, E., Lifland, E., Stankovic, J., Feng, L. (2021). A Novel Spatial-Temporal Specification-Based Monitoring System for Smart Cities. IEEE Internet of Things Journal, 8(15), 11793–11806. Peer-reviewed.
- Treml, L. M., Bartocci, E., Gizzi, A. (2021). Modeling and Analysis of Cardiac Hybrid Cellular Automata via GPU-accelerated Monte Carlo Simulation. Mathematics, 9(2), 164. Peer-reviewed.DOI: 10.3390/math9020164
- Marcel Moosbrugger, Ezio Bartocci, Katoen, J.-P., Laura Kovács. (2021). The Probabilistic Termination Tool Amber. In Formal Methods. FM 2021 (pp. 667–675). Peer-reviewed.
- Visconti, E., Bartocci, E., Loreti, M., Nenzi, L. (2021). Online monitoring of spatio-temporal properties for imprecise signals. In Proceedings of the 19th ACM-IEEE International Conference on Formal Methods and Models for System Design. MEMOCODE’21: the 19th ACM-IEEE International Conference on Formal Methods and Models for System Design, Beijing, China (Online due to Covid), China. Peer-reviewed.
- Bartocci, E., Deshmukh, J., Mateis, C., Nesterini, E., Ničković, D., Qin, X. (2021). Mining Shape Expressions with ShapeIt. In Software Engineering and Formal Methods (pp. 110–117). 13085. Peer-reviewed.
- Bartocci, E., Falcone, Y., Leucker, M. (2021). Preface. In E. Bartocci, Y. Falcone, M. Leucker (Eds.), Formal Methods in Outer Space. Essays Dedicated to Klaus Havelund on the Occasion of His 65th Birthday (pp. vii–viii). Springer, Lecture Notes in Computer Science.HDL: 20.500.12708/55665
- Bartocci, E., Falcone, Y., Leucker, M. (2021). Preface. In E. Bartocci, Y. Falcone, M. Leucker (Eds.), Formal Methods in Outer Space. Essays Dedicated to Klaus Havelund on the Occasion of His 65th Birthday (pp. vii–viii). Springer, Lecture Notes in Computer Science.HDL: 20.500.12708/55665
- Treml, L. M., Gizzi, A., Bartocci, E. (2021). Cardiac Hybrid Cellular Automata Simulation For 2d Cardiac Dynamics. In Book Of Abstracts (p. 201).HDL: 20.500.12708/55675
- Moosbrugger, M., Bartocci, E., Katoen, J.-P., Kovács, L. (2021). Automated Termination Analysis of Polynomial Probabilistic Programs. In Programming Languages and Systems (pp. 491–518). Springer. Peer-reviewed.
- Bartocci, E., Bloem, R., Maderbacher, B., Manjunath, N., Ničković, D. (2021). Adaptive Testing for Specification Coverage in CPS Models. In 7th IFAC Conference on Analysis and Design of Hybrid Systems ADHS 2021: Brussels, Belgium, 7-9 July 2021 (pp. 229–234). Elsevier. Peer-reviewed.
- Neufeld, E., Bartocci, E., Ciabattoni, A., Governatori, G. (2021). A Normative Supervisor for Reinforcement Learning Agents. In Automated Deduction – CADE 28 (pp. 565–576). Peer-reviewed.
- Dobe, O., Ábrahám, E., Bartocci, E., Bonakdarpour, B. (2021). HyperProb: A Model Checker for Probabilistic Hyperproperties. In Formal Methods (pp. 657–666). Peer-reviewed.
- Alsalehi, S., Mehdipour, N., Bartocci, E., Belta, C. (2021). Neural Network-based Control for Multi-Agent Systems from Spatio-Temporal Specifications. In 2021 60th IEEE Conference on Decision and Control (CDC). CDC 2021: the 60th IEEE Conference on Decision and Control, Austin, Texas, United States of America (the). Peer-reviewed.
2020
- Bartocci, E., Deshmukh, J., Gigler, F., Mateis, C., Nickovic, D., Qin, X. (2020). Mining Shape Expressions from Positive Examples. IEEE Transactions on Computer-Aided Design of Integrated Circuits and Systems, 39(11), 3809–3820. Peer-reviewed.
- Abraham, E., Bartocci, E., Bonakdarpour, B., Dobe, O. (2020). Parameter Synthesis for Probabilistic Hyperproperties. In LPAR-23: 23rd International Conference on Logic for Programming, Artificial Intelligence and Reasoning (pp. 12–31). Peer-reviewed.DOI: 10.29007/37lf
- Bartocci, E., Kovács, L., Stankovič, M. (2020). Analysis of Bayesian Networks via Prob-Solvable Loops. In Theoretical Aspects of Computing – ICTAC 2020 (pp. 221–241). Springer. Peer-reviewed.
- Bartocci, E., Kovács, L., Stankovič, M. (2020). Mora - Automatic Generation of Moment-Based Invariants. In Tools and Algorithms for the Construction and Analysis of Systems (pp. 492–498). Springer. Peer-reviewed.
- Bartocci, E., Bortolussi, L., Loreti, M., Nenzi, L., Silvetti, S. (2020). MoonLight: A Lightweight Tool for Monitoring Spatio-Temporal Properties. In L. Nenzi (Ed.), Runtime Verification (pp. 417–428). Springer. Peer-reviewed.
- Zapridou, E., Bartocci, E., Katsaros, P. (2020). Runtime Verification of Autonomous Driving Systems in CARLA. In Runtime Verification (pp. 172–183). Springer. Peer-reviewed.
- Bartocci, E., Manjunath, N., Mariani, L., Mateis, C., Ničković, D., Pastore, F. (2020). CPSDebug: a tool for explanation of failures in cyber-physical systems. In Proceedings of the 29th ACM SIGSOFT International Symposium on Software Testing and Analysis. Proc. of ISSTA 2020: the 29th ACM SIGSOFT International Symposium on Software Testing and Analysis, Virtual Event, United States of America (the). ACM. Peer-reviewed.
- Ábrahám, E., Bartocci, E., Bonakdarpour, B., Dobe, O. (2020). Probabilistic Hyperproperties with Nondeterminism. In Automated Technology for Verification and Analysis (pp. 518–534). Peer-reviewed.
- Meiyi, M., Bartocci, E., Lifland, E., Stankovic, J., Feng, L. (2020). SaSTL: Spatial Aggregation Signal Temporal Logic for Runtime Monitoring in Smart Cities. In 2020 ACM/IEEE 11th International Conference on Cyber-Physical Systems (ICCPS). Proc. of ICCPS 2020: the ACM/IEEE 11th International Conference on Cyber-Physical Systems, Sydney, Australia. IEEE. Peer-reviewed.
- Meiyi, M., Bartocci, E., Stankovic, J., Feng, L. (2020). Predictive monitoring with uncertainty for deep learning enabled smart cities: poster abstract. In Proceedings of the 18th Conference on Embedded Networked Sensor Systems. SenSys ’20: Proceedings of the 18th Conference on Embedded Networked Sensor Systems, Virtual Event, Japan.
- Nenzi, L., Bartocci, E., Bortolussi, L., Loreti, M., Visconti, E. (2020). Monitoring Spatio-Temporal Properties (Invited Tutorial). In Runtime Verification 20th International Conference, RV 2020, Los Angeles, CA, USA, October 6–9, 2020, Proceedings. Proc. of RV 2020: the 20th International Conference on Runtime Verification, Los Angeles, United States of America (the). Springer.
- Shmarov, F., Soudjani, S., Paoletti, N., Bartocci, E., Lin, S., Smolka, S. A., Zuliani, P. (2020). Automated Synthesis of Safe Digital Controllers for Sampled-Data Stochastic Nonlinear Systems. IEEE Access, 8, 180825–180843. Peer-reviewed.
2019
- Abbas, H., Rodionova, A., Mamouras, K., Bartocci, E., Smolka, S. A., Grosu, R. (2019). Quantitative Regular Expressions for Arrhythmia Detection. IEEE/ACM Transactions on Computational Biology and Bioinformatics, 16(5), 1586–1597. Peer-reviewed.
- Sánchez, C., Schneider, G., Ahrendt, W., Bartocci, E., Bianculli, D., Colombo, C., Falcone, Y., Francalanza, A., Krstić, S., Lourenço, J. M., Nickovic, D., Pace, G. J., Rufino, J., Signoles, J., Traytel, D., Weiss, A. (2019). A survey of challenges for runtime verification from advanced application domains (beyond software). Formal Methods in System Design, 54(3), 279–335. Peer-reviewed.
- Ratasich, D., Khalid, F., Geissler, F., Grosu, R., Shafique, M., Bartocci, E. (2019). A Roadmap Toward the Resilient Internet of Things for Cyber-Physical Systems. IEEE Access, 7, 13260–13283. Peer-reviewed.
- Gurung, A., Ray, R., Bartocci, E., Bogomolov, S., Grosu, R. (2019). Parallel reachability analysis of hybrid systems in XSpeed. International Journal on Software Tools for Technology Transfer, 21(4), 401–423. Peer-reviewed.
- Bartocci, E., Cleaveland, R., Grosu, R., Sokolsky, O. (Eds.). (2019). From Reactive Systems to Cyber-Physical Systems - Essays Dedicated to Scott A. Smolka on the Occasion of His 65th Birthday. Springer-Verlag Berlin Heidelberg.
- Bartocci, E., Falcone, Y., Bonakdarpour, B., Colombo, C., Decker, N., Havelund, K., Joshi, Y., Klaedtke, F., Milewicz, R., Reger, G., Rosu, G., Signoles, J., Thoma, D., Zalinescu, E., Zhang, Y. (2019). First international Competition on Runtime Verification: rules, benchmarks, tools, and final results of CRV 2014. International Journal on Software Tools for Technology Transfer, 21, 31–70. Peer-reviewed.DOI: 10.1007/s10009-017-0454-5 / Download: PDF
- Bartocci, E., Beyer, D., Black, P. (2019). TOOLympics 2019: An Overview of Competitions in Formal Methods. In Tools and Algorithms for the Construction and Analysis of Systems 25 Years of TACAS: TOOLympics, Held as Part of ETAPS 2019, Prague, Czech Republic, April 6–11, 2019, Proceedings, Part III. Tools and Algorithms for the Construction and Analysis of Systems- 25 Years of TACAS, Prague, Czechia.
- Piho, P., Margetiny, F., Bartocci, E., Ribchester, R. R., Hillston, J. (2019). Extending a Hodgkin-Huxley Model for Larval Drosophila Muscle Excitability via Particle Swarm Fitting. In Computational Methods in Systems Biology 17th International Conference, CMSB 2019, Trieste, Italy, September 18–20, 2019, Proceedings. 17th International Conference on Computational Methods in Systems Biology, Trieste, Italy. Peer-reviewed.
- Hirsch, C., Bartocci, E., Grosu, R. (2019). Capacitive Soil Moisture Sensor Node for IoT in Agriculture and Home. In 2019 IEEE 23rd International Symposium on Consumer Technologies (ISCT). 2019 IEEE 23rd International Symposium on Consumer Technologies (ISCT), Ancona, Italy. Peer-reviewed.
- Bartocci, E., Falcone, Y., Reger, G. (2019). International Competition on Runtime Verification (CRV). In Tools and Algorithms for the Construction and Analysis of Systems (pp. 41–49).
- Bartocci, E., Manjunath, N., Mariani, L., Mateis, C., Nickovic, D. (2019). Automatic Failure Explanation in CPS Models. In Software Engineering and Formal Methods 17th International Conference, SEFM 2019, Oslo, Norway, September 18–20, 2019, Proceedings. 17th International Conference on Software Engineering and Formal Methods, Oslo, Norway. Peer-reviewed.
- Kong, H., Bartocci, E., Jiang, Y., Henzinger, T. A. (2019). Piecewise Robust Barrier Tubes for Nonlinear Hybrid Systems with Uncertainty. In É. André M. Stoelinga (Eds.), Formal Modeling and Analysis of Timed Systems (pp. 123–141). Springer. Peer-reviewed.
- Bartocci, E., Kovacs, L., Stankovic, M. (2019). Automatic Generation of Moment-Based Invariants for Prob-Solvable Loops. In Y.-F. Chen, C.-H. Cheng, J. Esparza (Eds.), Automated Technology for Verification and Analysis (pp. 255–276). Springer. Peer-reviewed.
- Haghighi, I., Mehdipour, N., Bartocci, E., Belta, C. (2019). Control from Signal Temporal Logic Specifications with Smooth Cumulative Quantitative Semantics. In Proc. of CDC 2019: the 2019 IEEE Conference on Decision and Control. 2019 IEEE Conference on Decision and Control (CDC), Nice, France. IEEE. Peer-reviewed.HDL: 20.500.12708/57866
- Ratasich, D., Platzer, M., Grosu, R., Bartocci, E. (2019). Adaptive Fault Detection Exploiting Redundancy with Uncertainties in Space and Time. In 2019 IEEE 13th International Conference on Self-Adaptive and Self-Organizing Systems (SASO). 13th IEEE International Conference on Self-Adaptive and Self-Organizing Systems, Umeå, Sweden. IEEE. Peer-reviewed.
2018
- Bartocci, E., Falcone, Y., Francalanza, A., Reger, G. (2018). Introduction to Runtime Verification. In E. Bartocci Y. Falcone (Eds.), Lectures on Runtime Verification. Introductory and Advanced Topics (Vol. 10457, pp. 1–33). Springer-Verlag Berlin Heidelberg.
- Bartocci, E., Falcone, Y., Francalanza, A., Reger, G. (2018). Introduction to Runtime Verification. In E. Bartocci Y. Falcone (Eds.), Lectures on Runtime Verification. Introductory and Advanced Topics (Vol. 10457, pp. 1–33). Springer-Verlag Berlin Heidelberg.
- Bartocci, E., Deshmukh, R. G., Donze, A., Fainekos, G., Maler, O., Nickovic, D., Sankaranarayanan, S. (2018). Specification-Based Monitoring of Cyber-Physical Systems: A Survey on Theory, Tools and Applications. In E. Bartocci Y. Falcone (Eds.), Lectures on Runtime Verification, Introductory and Advanced Topics (pp. 135–175). Springer-Verlag Berlin Heidelberg. Peer-reviewed.
- Bartocci, E., Deshmukh, R. G., Donze, A., Fainekos, G., Maler, O., Nickovic, D., Sankaranarayanan, S. (2018). Specification-Based Monitoring of Cyber-Physical Systems: A Survey on Theory, Tools and Applications. In E. Bartocci Y. Falcone (Eds.), Lectures on Runtime Verification, Introductory and Advanced Topics (pp. 135–175). Springer-Verlag Berlin Heidelberg. Peer-reviewed.
- Bartocci, E., Falcone, Y. (Eds.). (2018). Lectures on Runtime Verification : Introductory and Advanced Topics. Springer-Verlag.
- Bartocci, E., Lio, P., Paoletti, N. (2018). Guest Editors’ Introduction to the Special Section on the 14th International Conference on Computational Methods in Systems Biology (CMSB 2016). IEEE/ACM Transactions on Computational Biology and Bioinformatics, 15(4), 1122–1123.
- Jakšić, S., Bartocci, E., Grosu, R., Nguyen, T., Ničković, D. (2018). Quantitative monitoring of STL with edit distance. Formal Methods in System Design, 53(1), 83–112. Peer-reviewed.
- Jaksic, S., Bartocci, E., Grosu, R., Nickovic, D. (2018). An algebraic framework for runtime verification. IEEE Transactions on Computer-Aided Design of Integrated Circuits and Systems, 37(11), 2233–2243. Peer-reviewed.
- Bartocci, E., Aydin Gol, E., Haghighi, I., Belta, C. (2018). A Formal Methods Approach to Pattern Recognition and Synthesis in Reaction Diffusion Networks. IEEE Transactions on Control of Network Systems, 5(1), 308–320. Peer-reviewed.
- Bartocci, E., Falcone, Y. (2018). RV-TheToP: Runtime Verification from Theory to the Industry Practice (Track Introduction). In T. Margaria B. Steffen (Eds.), Leveraging Applications of Formal Methods, Verification and Validation. Industrial Practice. ISoLA 2018, Proceedings, Part IV (pp. 3–8). Springer. Peer-reviewed.
- Silvetti, S., Nenzi, L., Bartocci, E., Bortolussi, L. (2018). Signal Convolution Logic. In Automated Technology for Verification and Analysis (pp. 267–283). Peer-reviewed.
- Fan, C., Meng, Y., Maier, J., Bartocci, E., Mitra, S., Schmid, U. (2018). Verifying nonlinear analog and mixed-signal circuits with inputs. In 6th IFAC Conference on Analysis and Design of Hybrid Systems ADHS 2018: Oxford, United Kingdom, 11—13 July 2018 (pp. 241–246). Elsevier. Peer-reviewed.
- Kong, H., Bartocci, E., Henzinger, T. A. (2018). Reachable Set Over-Approximation for Nonlinear Systems Using Piecewise Barrier Tubes. In H. Chockler G. Weissenbacher (Eds.), Computer Aided Verification: 30th International Conference, CAV 2018 (pp. 449–467). Springer. Peer-reviewed.
- Bartocci, E., Bloem, R., Nickovic, D., Roeck, F. (2018). A Counting Semantics for Monitoring LTL Specifications over Finite Traces. In H. Chockler G. Weissenbacher (Eds.), Computer Aided Verification: 30th International Conference, CAV 2018 (pp. 547–564). Springer. Peer-reviewed.
- Bartocci, E., Ferrere, T., Manjunath, N., Nickovic, D. (2018). Localizing Faults in Simulink/Stateflow Models with {STL}. In Proceedings of the 21st International Conference on Hybrid Systems: Computation and Control (part of {CPS} Week). Proceedings of the 21st International Conference on Hybrid Systems: Computation and Control (part of {CPS} Week), Porto, Portugal. Peer-reviewed.
- Arming, S., Bartocci, E., Chatterjee, K., Katoen, J.-P., Sokolova, A. (2018). Parameter-Independent Strategies for pMDPs via POMDPs. In A. McIver A. Horvath (Eds.), Quantitative Evaluation of Systems: 15th International Conference, QEST 2018 (pp. 53–70). Springer. Peer-reviewed.
- Bartocci, E. (2018). Monitoring, Learning and Control of Cyber-Physical Systems with STL (Tutorial). In C. Colombo M. Leucker (Eds.), Runtime Verification (pp. 35–42). Springer. Peer-reviewed.
- Nenzi, L., Silvetti, S., Bartocci, E., Bortolussi, L. (2018). A Robust Genetic Algorithm for Learning Temporal Specifications from Data. In Quantitative Evaluation of Systems 15th International Conference, QEST 2018, Beijing, China, September 4-7, 2018, Proceedings. Proc. of QEST 2018: the 15th International Conference on Quantitative Evaluation of Systems, Peking, China. Peer-reviewed.
2017
- Bartocci, E., Bortolussi, L., Brázdil, T., Milios, D., Sanguinetti, G. (2017). Policy learning in Continuous-Time Markov Decision Processes using Gaussian Processes. Performance Evaluation, 116, 84–100. Peer-reviewed.
- Abbas, H., Rodionova, A., Bartocci, E., Smolka, S. A., Grosu, R. (2017). Quantitative Regular Expressions for Arrhythmia Detection Algorithms. In Computational Methods in Systems Biology (pp. 23–39). Springer. Peer-reviewed.
- Arming, S., Bartocci, E., Sokolova, A. (2017). SEA-PARAM: Exploring Schedulers in Parametric MDPs. In Electronic Proceedings in Theoretical Computer Science (pp. 25–38). EPCTS. Peer-reviewed.DOI: 10.4204/eptcs.250.3
- Shmarov, F., Paoletti, N., Bartocci, E., Lin, S., Smolka, S. A., Zuliani, P. (2017). SMT-based Synthesis of Safe and Robust PID Controllers for Stochastic Hybrid Systems. In Hardware and Software: Verification and Testing (pp. 131–146). Springer. Peer-reviewed.
- Selyunin, K., Jaksic, S., Nguyen, T., Reidl, C., Hafner, U., Bartocci, E., Nickovic, D., Grosu, R. (2017). Runtime Monitoring with Recovery of the SENT Communication Protocol. In Computer Aided Verification (pp. 336–355). Springer. Peer-reviewed.
- Bartocci, E., Bortolussi, L., Loreti, M., Nenzi, L. (2017). Monitoring mobile and spatially distributed cyber-physical systems. In Proceedings of the 15th ACM-IEEE International Conference on Formal Methods and Models for System Design. MEMOCODE 2017: the 15th ACM-IEEE International Conference on Formal Methods and Models for System Design, Wien, Austria. ACM. Peer-reviewed.
- Baldi, M., Bartocci, E., Chiaraluce, F., Cucchiarelli, A., Senigagliesi, L., Spalazzi, L., Spegni, F. (2017). A Probabilistic Small Model Theorem to Assess Confidentiality of Dispersed Cloud Storage. In Quantitative Evaluation of Systems (pp. 123–139). Springer. Peer-reviewed.
- Ben Sassi, M. A., Bartocci, E., Sankaranarayanan, S. (2017). A Linear Programming-based Iterative Approach to Stabilizing Polynomial Dynamics. In 20th IFAC World Congress (pp. 10462–10469). Elsevier. Peer-reviewed.
- Lukina, A., Esterle, L., Hirsch, C., Bartocci, E., Yang, J., Tiwari, A., Smolka, S. A., Grosu, R. (2017). ARES: Adaptive Receding-Horizon Synthesis of Optimal Plans. In A. Legay T. Margaria (Eds.), Tools and Algorithms for the Construction and Analysis of Systems (pp. 286–302). Springer. Peer-reviewed.
- Selyunin, K., Hasani, R., Ratasich, D., Bartocci, E., Grosu, R. (2017). Computing with Biophysical and Hardware-efficient Neural Models. In I. Rojas, G. Joya, A. Catala (Eds.), Advances in Computational Intelligence (pp. 535–547). Springer. Peer-reviewed.
2016
- Bartocci, E., Ramakrishnan, C. R. (2016). Preface of the special issue on Model Checking of Software : Selected papers of the 20th International SPIN Symposium on Model Checking of Software. International Journal on Software Tools for Technology Transfer.DOI: 10.1007/s10009-016-0414-5 / Download: PDF
- Bartocci, E., Lió, P. (2016). Computational modeling, formal analysis and tools for systems biology. PLoS Computational Biology, 12(1), e1004591. Peer-reviewed.
- Gurung, A., Kumar, D. A., Bartocci, E., Bogomolov, S., Grosu, R., Ray, R. (2016). Parallel reachability analysis for hybrid systems. In 2016 ACM/IEEE International Conference on Formal Methods and Models for System Design (MEMOCODE). Proc. of MEMOCODE 2016: the 14th ACM-IEEE International Conference on Formal Methods and Models for System Design, ACM, 2016, Kanpur, India. Peer-reviewed.
- Selyunin, K., Nguyen, T., Basa, A.-D., Bartocci, E., Nickovic, D., Grosu, R. (2016). Applying High-Level Synthesis for Synthesizing Hardware Runtime STL Monitors of Mission-Critical Properties. In Design and Verification Conference and Exhibition (p. 8). Online. Peer-reviewed.HDL: 20.500.12708/56824
- Selyunin, K., Nguyen, T., Bartocci, E., Grosu, R. (2016). Applying Runtime Monitoring for Automotive Electronic Development. In Runtime Verification (pp. 462–469). Springer International Publishing. Peer-reviewed.
- Nguyen, T., Bartocci, E., Ničković, D., Grosu, R., Jaksic, S., Selyunin, K. (2016). The HARMONIA Project: Hardware Monitoring for Automotive Systems-of-Systems. In T. Margaria B. Steffen (Eds.), Leveraging Applications of Formal Methods, Verification and Validation: Discussion, Dissemination, Applications. ISoLA 2016, Proceedings, Part II (pp. 371–379). Springer.
- Bartocci, E., Falcone, Y. (2016). Runtime Verification and Enforcement, the (Industrial) Application Perspective (Track Introduction). In T. Margaria B. Steffen (Eds.), Leveraging Applications of Formal Methods, Verification and Validation: Discussion, Dissemination, Applications. ISoLA 2016, Proceedings, Part II (pp. 333–338). Springer.
- Kong, H., Bartocci, E., Bogomolov, S., Grosu, R., Henzinger, T. A., Jiang, Y., Schilling, C. (2016). Discrete Abstraction of Multiaffine Systems. In Hybrid Systems Biology (pp. 128–144). Springer International Publishing. Peer-reviewed.
- Kalajdzic, K., Jegourel, C., Lukina, A., Bartocci, E., Legay, A., Smolka, S. A., Grosu, R. (2016). Feedback Control for Statistical Model Checking of Cyber-Physical Systems. In T. Margaria B. Steffen (Eds.), Leveraging Applications of Formal Methods, Verification and Validation: Foundational Techniques (ISoLA 2016), Proceedings, Part I (pp. 46–61). Springer. Peer-reviewed.
- Selyunin, K., Nguyen, T., Bartocci, E., Nickovic, D., Grosu, R. (2016). Monitoring of MTL Specifications With IBM’s Spiking-Neuron Model. In Proc. of the 2016 Design, Automation Test in Europe Conference Exhibition (pp. 924–929). IEEE Computer Society. Peer-reviewed.HDL: 20.500.12708/56706
- Rodionova, A., Bartocci, E., Nickovic, D., Grosu, R. (2016). Temporal Logic as Filtering. In Proceedings of the 19th International Conference on Hybrid Systems: Computation and Control. Proceeding HSCC ’16 - the 19th International Conference on Hybrid Systems: Computation and Control, Vienna, Austria. ACM. Peer-reviewed.
- Bartocci, E., Bortolussi, L., Brazdil, T., Milos, D., Sanguinetti, G. (2016). Policy Learning for Time-Bounded Reachability in Continuous-Time Markov Decision Processes via Doubly-Stochastic Gradient Ascent. In Quantitative Evaluation of Systems (pp. 244–259). Springer International Publishing. Peer-reviewed.
- Jakšić, S., Bartocci, E., Grosu, R., Ničković, D. (2016). Quantitative Monitoring of STL with Edit Distance. In Runtime Verification (pp. 201–218). Springer International Publishing. Peer-reviewed.
- Bartocci, E., Lio, P., Paoletti, N. (Eds.). (2016). Computational Methods in Systems Biology. Springer International Publishing. Peer-reviewed.
2015
- Rajarshi, R., Amit, G., Binayak, D., Bartocci, E., Bogomolov, S., Grosu, R. (2015). XSpeed: Accelerating Reachability Analysis on Multi-core Processors. In N. Piterman (Ed.), Hardware and Software: Verification and Testing - 11th International Haifa Verification Conference, HVC 2015, Haifa, Israel, November 17-19, 2015, Proceedings (pp. 3–18). LNCS / Springer. Peer-reviewed.
- Bartocci, E., Bortolussi, L., Nenzi, L., Sanguinetti, G. (2015). System Design of Stochastic Models using Robustness of Temporal Properties. Theoretical Computer Science, 587, 3–25. Peer-reviewed.
- Ariful Islam, Md., Murthy, A., Bartocci, E., Cherry, E. M., Fenton, F. H., Glimm, J., Smolka, S. A., Grosu, R. (2015). Model-Order Reduction of Ion Channel Dynamics Using Approximate Bisimulation. Theoretical Computer Science, 599, 34–46. Peer-reviewed.
- Selyunin, K., Ratasich, D., Bartocci, E., Islam, M. A., Smolka, S. A., Grosu, R. (2015). Neural Programming: Towards adaptive control in Cyber-Physical Systems. In 2015 54th IEEE Conference on Decision and Control (CDC). 54th IEEE Conference on Decision and Control, Osaka, Japan. IEEE Computer Society. Peer-reviewed.
- Jaksic, S., Bartocci, E., Grosu, R., Kloibhofer, R., Nguyen, T., Nickovic, D. (2015). From signal temporal logic to FPGA monitors. In 2015 ACM/IEEE International Conference on Formal Methods and Models for Codesign (MEMOCODE). 13th ACM-IEEE International Conference on Formal Methods and Models for System Design, Austin, United States of America (the). IEEE. Peer-reviewed.
- Bogomolov, S., Schilling, C., Bartocci, E., Batt, G., Kong, H., Grosu, R. (2015). Abstraction-Based Parameter Synthesis for Multiaffine Systems. In Hardware and Software: Verification and Testing (pp. 19–35). LNCS / Springer. Peer-reviewed.
- Bartocci, E., Bortolussi, L., Milos, D., Nenzi, L., Sanguinetti, G. (2015). Studying Emergent Behaviours in Morphogenesis using Signal Spatio-Temporal Logic. In Proc. of HSB 15: the 4th International Workshop on Hybrid Systems Biology (pp. 1–17). LNCS / LNBI / Springer. Peer-reviewed.HDL: 20.500.12708/56256
- Weissenbacher, G. (2015). Explaining Heisenbugs. In E. Bartocci R. Majumdar (Eds.), Runtime Verification (p. XV). Lecture Notes in Computer Science/Springer.HDL: 20.500.12708/56231
- Haghighi, I., Jones, A., Kong, Z., Bartocci, E., Gros, R., Belta, C. (2015). SpaTeL: a novel spatial-temporal logic and its applications to networked systems. In Proceedings of the 18th International Conference on Hybrid Systems: Computation and Control. 18th International Conference on Hybrid Systems: Computation and Control (HSCC), Seattle, United States of America (the). ACM. Peer-reviewed.
- Bartocci, E., Majumdar, R. (Eds.). (2015). Runtime Verification : 6th International Conference, RV 2015, Vienna, Austria, September 22-25, 2015. Proceedings. Springer International Publishing. Peer-reviewed.
2014
- Bartocci, E., Höftberger, O., Grosu, R. (2014). Cyber-Physical Systems: Theoretical and Practical Challenges. ERCIM NEWS, 2014(97), 8–9. Invited.HDL: 20.500.12708/157429
- Bartocci, E., Bortolussi, L., Smolka, S. A. (2014). Hybrid Systems and Biology. Information and Computation, 236, 1–2.
- Ariful, I., Deshpande, T., Murthy, A., Bartocci, E., Smolka, S. A., Stoller, S. D., Grosu, R. (2014). Tracking Action Potentials of Nonlinear Excitable Cells using Model Predictive Control. In Proc. of BIOTECHNO 2014: The Sixth International Conference on Bioinformatics, Biocomputational Systems and Biotechnologies (pp. 52–58). IARIA. Peer-reviewed.HDL: 20.500.12708/55802
- Bartocci, E., DeFrancisco, R., Smolka, S. A. (2014). Towards a GPGPU-parallel SPIN model checker. In Proceedings of the 2014 International SPIN Symposium on Model Checking of Software. 21th International SPIN Symposium on Model Checking of Software, San Jose, California, United States of America (the). ACM. Peer-reviewed.
- Bartocci, E., Gao, S., Smolka, S. A. (2014). Medical Cyber-Physical Systems. In Leveraging Applications of Formal Methods, Verification and Validation. Specialized Techniques and Applications. ISoLA 2014, Proceedings, Part II (pp. 353–355). Springer.
- Bufo, S., Bartocci, E., Sanguinetti, G., Borelli, M., LUCANGELO, U., Bortolussi, L. (2014). Temporal Logic Based Monitoring of Assisted Ventilation in Intensive Care Patients. In T. Margaria B. Steffen (Eds.), Leveraging Applications of Formal Methods, Verification and Validation. Specialized Techniques and Applications. ISoLA 2014, Proceedings, Part II (pp. 391–403). Springer.
- Bartocci, E., Bortolussi, L., Sanguinetti, G. (2014). Data-Driven Statistical Learning of Temporal Logic Properties. In Formal Modeling and Analysis of Timed Systems 12th International Conference, FORMATS 2014, Florence, Italy, September 8-10, 2014, Proceedings (pp. 23–37). LNCS/Springer. Peer-reviewed.
- Aydin Gol, E., Bartocci, E., Belta, C. (2014). A Formal Methods Approach to Pattern Synthesis in Reaction Diffusion Systems. In Proc. of CDC 2014: the IEEE 53rd Annual Conference on Decision and Control (pp. 108–113). IEEE. Peer-reviewed.HDL: 20.500.12708/55797
- Bartocci, E., Bonakdarpour, B., Falcone, Y. (2014). First International Competition of Software for Runtime Verification. In Runtime Verification 5th International Conference, RV 2014, Toronto, ON, Canada, September 22-25, 2014. Proceedings. 14th International Conference on Runtime Verification, Canada.
2013
- Murthy, A., Bartocci, E., Fenton, F. H., Glimm, J., Gray, R. A., Cherry, E. M., Smolka, S. A., Grosu, R. (2013). Curvature Analysis of Cardiac Excitation Wavefronts. IEEE-ACM TRANSACTIONS ON COMPUTATIONAL BIOLOGY AND BIOINFORMATICS, 10(2), 323–336. Peer-reviewed.
- Bartocci, E., Ramakrishnan, C. R. (Eds.). (2013). Model Checking Software : 20th International Symposium, SPIN 2013, Stony Brook, NY, USA, July 8-9, 2013, Proceedings. Springer-Verlag Berlin Heidelberg. Peer-reviewed.
- Bartocci, E., Bortolussi, L., Nenzi, L. (2013). A Temporal Logic Approach to Modular Design of Synthetic Biological Circuits. In Computational Methods in Systems Biology (pp. 164–177). LNCS/Springer. Peer-reviewed.
- Kalajdzic, K., Bartocci, E., Stoller, S. D., Smolka, S. A., Grosu, R. (2013). Runtime Verification with Particle Filtering. In Runtime Verification (pp. 149–166). LNCS/Springer. Peer-reviewed.
- Bartocci, E., Bortolussi, L., Nenzi, L., Sanguinetti, G. (2013). On the Robustness of Temporal Properties for Stochastic Models. In Electronic Proceedings in Theoretical Computer Science (pp. 3–19). Electronic Proceedings on Theoretical Computer Science. Peer-reviewed.DOI: 10.4204/eptcs.125.1
- Bartocci, E., Grosu, R. (2013). Monitoring with uncertainty. In Electronic Proceedings in Theoretical Computer Science (pp. 1–4). Electronic Proceedings in Theoretical Computer Science.DOI: 10.4204/eptcs.124.1
- Bartocci, E. (2013). Sampling-based Decentralized Monitoring for Networked Embedded Systems. In Electronic Proceedings in Theoretical Computer Science (pp. 85–99). Electronic Proceedings in Theoretical Computer Science. Peer-reviewed.DOI: 10.4204/eptcs.124.9
2012
- Bartocci, E., Liò, P., Merelli, E., Paoletti, N. (2012). Multiple Verification in Complex Biological Systems: The Bone Remodelling Case Study. In Transactions on Computational Systems Biology XIV : Special Issue on Computational Models for Cell Processes (pp. 53–76). IEEE. Peer-reviewed.
- Bartocci, E., Cacciagrano, D., Di Berardini, M. R., Merelli, E., Vito, L. (2012). UBioLab: a web-LABoratory for Ubiquitous in-silico experiments. Journal of Integrative Bioinformatics: JIB, 9(1), Article 192. Peer-reviewed.
- Donzé, A., Maler, O., Bartocci, E., Nickovic, D., Grosu, R., Smolka, S. (2012). On Temporal Logic and Signal Processing. In Automated Technology for Verification and Analysis (pp. 92–106). LNCS/Springer. Peer-reviewed.
- Murthy, A., Ariful, I., Bartocci, E., Cherry, E., Fenton, F. H., Glimm, J., Smolka, S. A., Grosu, R. (2012). Approximate Bisimulations for Sodium Channel Dynamics. In Computational Methods in Systems Biology (pp. 267–287). LNCS / Springer. Peer-reviewed.
- Bartocci, E., Grosu, R., Karmarkar, A., Smolka, S. A., Stoller, S. D., Seyster, J. (2012). Adaptive Runtime Verification. In Runtime Verification (pp. 168–182). LNCS / Springer. Peer-reviewed.
- Stoller, S. D., Bartocci, E., Seyster, J., Grosu, R., Havelund, K., Smolka, S. A., Zadok, E. (2012). Runtime Verification with State Estimation. In Runtime Verification (pp. 193–207). LNCS / Springer Berlin Heidelberg. Peer-reviewed.
- Bartocci, E., Bortolussi, L. (Eds.). (2012). Proceedings First International Workshop on Hybrid Systems and Biology. Electronic Proceedings in Theoretical Computer Science.DOI: 10.4204/EPTCS.92
2011
- Alfieri, R., Bartocci, E., Merelli, E., Milanesi, L. (2011). Modeling the cell cycle: From deterministic models to hybrid systems. BioSystems, 105(1), 34–40. Peer-reviewed.
- Grosu, R., Batt, G., Fenton, F. H., Glimm, J., Le Guernic, C., Smolka, S. A., Bartocci, E. (2011). From Cardiac Cells to Genetic Regulatory Networks. In Computer Aided Verification (pp. 396–411). LNCS / Springer. Peer-reviewed.
- Bartocci, E., Cherry, E., Glimm, J., Grosu, R., Smolka, S. A. (2011). Toward real-time simulation of cardiac dynamics. In Proceedings of the 9th International Conference on Computational Methods in Systems Biology - CMSB ’11. CMSB 2011: the 9th ACM International Conference on Computational Methods in Systems Biology, Paris, France. ACM. Peer-reviewed.
- Murthy, A., Bartocci, E., Fenton, F. H., Glimm, J., Gray, R., Smolka, S. A., Grosu, R. (2011). Curvature analysis of cardiac excitation wavefronts. In Proceedings of the 9th International Conference on Computational Methods in Systems Biology - CMSB ’11. CMSB 2011: the 9th ACM International Conference on Computational Methods in Systems Biology, Paris, France. ACM. Peer-reviewed.
- Bartocci, E., Grosu, R., Katsaros, P., Ramakrishnan, C. R., Smolka, S. A. (2011). Model Repair for Probabilistic Systems. In Tools and Algorithms for the Construction and Analysis of Systems (pp. 326–340). LNCS / Springer. Peer-reviewed.
Presentations
- Kofnov, A., Kapla, D. B., Bartocci, E., Bura, E. (2025, December 17). Exact Upper and Lower Bounds for the Output Distribution of Neural Networks with Random Inputs [Conference Presentation]. 2025 IMS International Conference on Statistics and Data Science (ICSDS), Sevilla, Spain.HDL: 20.500.12708/225179
- Bartocci, E., Kovacs, L., Bura, E. (2020). ProbInG: Distribution Recovery for Invariant Generation of Probabilistic Programs. Vienna Science, Research and Technology Fund - ProbInG, online, Austria.HDL: 20.500.12708/123229
Theses
- Tepaev, A. (2026). Comparative evaluation of TLA+ and R-CHECK specifications [Diploma Thesis, Technische Universität Wien]. reposiTUm.DOI: 10.34726/hss.2026.132821 / Download: PDF
- Nesterini, E. (2025). Specification mining for cyber-physical systems [Dissertation, Technische Universität Wien]. reposiTUm.DOI: 10.34726/hss.2025.134080 / Download: PDF
- Gigler, F. N. (2025). Uniform sampling of timed regular expressions [Diploma Thesis, Technische Universität Wien]. reposiTUm.DOI: 10.34726/hss.2025.129120 / Download: PDF
- Yadav, D. (2024). Enhancing fault diagnosis in safety-critical cyber-physical systems [Dissertation, Technische Universität Wien]. reposiTUm.DOI: 10.34726/hss.2025.125790 / Download: PDF
- Oliveira Da Costa, A. A. (2024). Design and verification of information flows [Dissertation, Technische Universität Wien]. reposiTUm.DOI: 10.34726/hss.2024.124622 / Download: PDF
- Moosbrugger, M. (2024). Automated analysis of probabilistic loops [Dissertation, Technische Universität Wien]. reposiTUm.DOI: 10.34726/hss.2024.123240 / Download: PDF
- Kiesel, R. P. D. (2023). Streaming and quantitative extensions of answer set programming [Dissertation, Technische Universität Wien]. reposiTUm.DOI: 10.34726/hss.2024.119341 / Download: PDF
- Schiehl, B. (2023). Normative compliance in lexicographic multi-objective reinforcement learning agents [Diploma Thesis, Technische Universität Wien]. reposiTUm.DOI: 10.34726/hss.2023.113064 / Download: PDF
- Stankovic, M. (2023). Moment-based loop analysis [Dissertation, Technische Universität Wien]. reposiTUm.DOI: 10.34726/hss.2023.113863 / Download: PDF
- Neufeld, E. A. (2023). Norm compliance for reinforcement learning agents [Dissertation, Technische Universität Wien]. reposiTUm.DOI: 10.34726/hss.2023.112881 / Download: PDF
- Isakovic, H. (2022). Towards dependable CPS/IoT ecosystems [Dissertation, Technische Universität Wien]. reposiTUm.DOI: 10.34726/hss.2022.103104 / Download: PDF
- Manjunath, N. (2021). Fault-based analysis of cyber physical systems [Dissertation, Technische Universität Wien]. reposiTUm.DOI: 10.34726/hss.2021.88181 / Download: PDF
- Exenberger, F. (2019). Fault analysis in reactive systems using log data [Diploma Thesis, Technische Universität Wien]. reposiTUm.DOI: 10.34726/hss.2019.63176 / Download: PDF
- Ratasich, D. (2019). Self-healing cyber-physical systems [Dissertation, Technische Universität Wien]. reposiTUm.DOI: 10.34726/hss.2019.64761 / Download: PDF
- Beck, H. (2018). Expressive rule-based stream reasoning [Dissertation, Technische Universität Wien]. reposiTUm.DOI: 10.34726/hss.2018.61225 / Download: PDF
- Treml, L. M. (2018). Simulating cardiac dynamics using Maxeler dataflow super-computing [Diploma Thesis, Technische Universität Wien]. reposiTUm.DOI: 10.34726/hss.2018.41907 / Download: PDF
- Bartocci, E. (2018). Formal analysis of cyber-physical systems [Professorial Dissertation, Technische Universität]. reposiTUm.HDL: 20.500.12708/159429
- Wang, G. (2018). Neural computation methods for industrial data processing [Dissertation, Technische Universität Wien]. reposiTUm.DOI: 10.34726/hss.2018.62942 / Download: PDF
- Wimmer, B. (2017). Motion planning for a six-legged robot [Diploma Thesis, Technische Universität Wien]. reposiTUm.DOI: 10.34726/hss.2017.37185 / Download: PDF
- Selyunin, K. (2017). Neural models for monitoring and control with applications in automotive domain [Dissertation, Technische Universität Wien]. reposiTUm.DOI: 10.34726/hss.2017.50304 / Download: PDF
- Vaczula, C. (2016). The Hobel algorithm : SAT Lösung mit GPU über DPLL [Diploma Thesis, Technische Universität Wien]. reposiTUm.DOI: 10.34726/hss.2016.35995 / Download: PDF
Awards
- Best Paper Award of EMSOFT 2025
2025 / Embedded Systems Week (ESWEEK) 2025 (EMSOFT) / Taiwan - Radhia Cousot Young Researcher Best Paper Award
2022 / The Static Analysis Symposia / New Zealand / Website - Best Paper of QEST 2022 International Conference
2022 / 19th International Conference on Quantitative Evaluation of SysTems / Poland - Best Software Science Paper of the European Joint Conferences on Theory and Practice of Software (ETAPS) 2022
2022 / European Association of Software Science and Technology (EASST) / Germany / Website - Honorable mention for the Best Student Paper Award at HSCC 2016
2016 / 19th International Conference on Hybrid Systems: Computation and Control / Austria - Best Paper Award 2011
2011 / Runtime Verification Conference / USA / Website
And more…
Soon, this page will include additional information such as reference projects, activities as journal reviewer and editor, memberships in councils and committees, and other research activities.
Until then, please visit Ezio’s research profile in TISS.