TU Wien Informatics

Overview Professors Scientific Staff Administrative Staff Student Staff External Lecturers By Responsibilities By Committee By Name
Related
Guest Professors Honoraries Alumni (LinkedIn) #5qw

Ezio Bartocci

Univ.Prof. Dr.

Research Focus

  • Computer Engineering: 100%
Ezio Bartocci

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. The primary focus of my research is to develop formal methods, computational tools and techniques that support the modeling and the automated analysis of complex computational systems, including software systems, cyber-physical systems and biological systems.

Roles

  • Full Professor
    Cyber-Physical Systems, E191-01
  • Faculty Council
    Principal Member
  • Curriculum Commission for Computer Engineering
    Substitute Member

Contact

2022W

2023S

 

Note: Due to the rollout of TU Wien’s new publication database, the list below may be slightly outdated. Once the migration is complete, everything will be up to date again.

2022

  • Search-based Testing for Accurate Fault Localization in CPS / 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). https://doi.org/10.1109/ISSRE55969.2022.00024
  • FIM: fault injection and mutation for Simulink / 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). https://doi.org/10.1145/3540250.3558932
  • Survey on mining signal temporal logic specifications / Bartocci, E., Mateis, C., Nesterini, E., & Nickovic, D. (2022). Survey on mining signal temporal logic specifications. Information and Computation, 289(Part A), Article 104957. https://doi.org/10.1016/j.ic.2022.104957
  • This Is the Moment for Probabilistic Loops / 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. https://doi.org/10.1145/3563341
  • Probabilistic Hyperproperties with Rewards / Dobe, O., Wilke, L., Ábrahám, E., Bartocci, E., & Bonakdarpour, B. (2022). Probabilistic Hyperproperties with Rewards. In NASA Formal Methods (pp. 656–673). Springer Nature Switzerland AG. https://doi.org/10.1007/978-3-031-06773-0_35
  • Information-flow Interfaces / 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. https://doi.org/10.1007/978-3-030-99429-7_1
  • Enforcing ethical goals over reinforcement-learning policies / 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. https://doi.org/10.1007/s10676-022-09665-8 / Project: RTD-Indian
  • Model checking hyperproperties for Markov decision processes / 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. https://doi.org/10.1016/j.ic.2022.104978
  • 25th ACM International Conference on Hybrid Systems: Computation and Control / Bartocci, E., & Putot, S. (Eds.). (2022). 25th ACM International Conference on Hybrid Systems: Computation and Control. https://doi.org/10.1145/3501710
  • DeepSTL / He, J., Bartocci, E., Ničković, D., Isakovic, H., & Grosu, R. (2022). DeepSTL. In ICSE ’22: Proceedings of the 44th International Conference on Software Engineering (pp. 610–622). Association for Computing Machinery. https://doi.org/10.1145/3510003.3510171
  • A Logic for Monitoring Dynamic Networks of Spatially-distributed Cyber-Physical Systems / 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. https://doi.org/10.46298/lmcs-18(1:4)2022
  • On Normative Reinforcement Learning via Safe Reinforcement Learning / 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). https://doi.org/10.1007/978-3-031-21203-1_5 / Project: RTD-Indian
  • Moment-Based Invariants for Probabilistic Loops with Non-polynomial Assignments / 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. https://doi.org/10.1007/978-3-031-16336-4_1 / Projects: ARTIST, ProbInG
  • Solving Invariant Generation for Unsolvable Loops / 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). https://doi.org/10.1007/978-3-031-22308-2_3
  • Probabilistic Hyperproperties with Rewards / Wilke, L., Dobe, O., Abraham, E., Bartocci, E., & Bonakdarpour, B. (2022). Probabilistic Hyperproperties with Rewards. In Lecture Notes in Computer Science (pp. 656–673). https://doi.org/10.1007/978-3-031-06773-0_35
  • Moment-based analysis of Bayesian network properties / Stankovič, M., Bartocci, E., & Kovács, L. (2022). Moment-based analysis of Bayesian network properties. Theoretical Computer Science, 903, 113–133. https://doi.org/10.1016/j.tcs.2021.12.021
  • Flavors of Sequential Information Flow / Bartocci, E., Ferrère, T., Henzinger, T. A., Nickovic, D., & da Costa, A. O. (2022). Flavors of Sequential Information Flow. In Lecture Notes in Computer Science (pp. 1–19). https://doi.org/10.1007/978-3-030-94583-1_1

2021

  • The Probabilistic Termination Tool Amber / Marcel Moosbrugger, Ezio Bartocci, Katoen, J.-P., & Laura Kovács. (2021). The Probabilistic Termination Tool Amber. In Formal Methods. FM 2021 (pp. 667–675). https://doi.org/10.1007/978-3-030-90870-6_36
  • Modeling and Analysis of Cardiac Hybrid Cellular Automata via GPU-accelerated Monte Carlo Simulation / 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. https://doi.org/10.3390/math9020164
  • CPSDebug: Automatic Failure Explanation in CPS Models / 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. https://doi.org/10.1007/s10009-020-00599-4
  • A Novel Spatial-Temporal Specification-Based Monitoring System for Smart Cities / 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. https://doi.org/10.1109/jiot.2021.3069943
  • Predictive Monitoring with Logic-Calibrated Uncertainty for Cyber-Physical Systems / 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. https://doi.org/10.1145/3477032
  • Preface / 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. http://hdl.handle.net/20.500.12708/55665
  • A Perspective on "CCS Expressions, Finite State Processes, and Three Problems of Equivalence" / 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. https://doi.org/10.1145/3510382.3510394
  • Mining Shape Expressions with ShapeIt / 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. https://doi.org/10.1007/978-3-030-92124-8_7
  • Online monitoring of spatio-temporal properties for imprecise signals / 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), International. https://doi.org/10.1145/3487212.3487344
  • Neural Network-based Control for Multi-Agent Systems from Spatio-Temporal Specifications / 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, Non-EU. https://doi.org/10.1109/cdc45484.2021.9682921
  • HyperProb: A Model Checker for Probabilistic Hyperproperties / Dobe, O., Ábrahám, E., Bartocci, E., & Bonakdarpour, B. (2021). HyperProb: A Model Checker for Probabilistic Hyperproperties. In Formal Methods (pp. 657–666). https://doi.org/10.1007/978-3-030-90870-6_35
  • A Normative Supervisor for Reinforcement Learning Agents / Neufeld, E., Bartocci, E., Ciabattoni, A., & Governatori, G. (2021). A Normative Supervisor for Reinforcement Learning Agents. In Automated Deduction – CADE 28 (pp. 565–576). https://doi.org/10.1007/978-3-030-79876-5_32
  • Adaptive Testing for Specification Coverage in CPS Models / Bartocci, E., Bloem, R., Maderbacher, B., Manjunath, N., & Ničković, D. (2021). Adaptive Testing for Specification Coverage in CPS Models. In IFAC-PapersOnLine (pp. 229–234). 54. https://doi.org/10.1016/j.ifacol.2021.08.503
  • Automated Termination Analysis of Polynomial Probabilistic Programs / 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. https://doi.org/10.1007/978-3-030-72019-3_18
  • Cardiac Hybrid Cellular Automata Simulation For 2d Cardiac Dynamics / Treml, L. M., Gizzi, A., & Bartocci, E. (2021). Cardiac Hybrid Cellular Automata Simulation For 2d Cardiac Dynamics. In Book Of Abstracts (p. 201). http://hdl.handle.net/20.500.12708/55675

2020

  • Mining Shape Expressions from Positive Examples / Bartocci, E., Deshmukh, J., Gliger, 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. https://doi.org/10.1109/tcad.2020.3012240
  • Automated Synthesis of Safe Digital Controllers for Sampled-Data Stochastic Nonlinear Systems / 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. https://doi.org/10.1109/access.2020.3028476
  • ProbInG: Distribution Recovery for Invariant Generation of Probabilistic Programs / 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. http://hdl.handle.net/20.500.12708/123229
  • Predictive monitoring with uncertainty for deep learning enabled smart cities / Meiyi, M., Bartocci, E., Stankovic, J., & Feng, L. (2020). Predictive monitoring with uncertainty for deep learning enabled smart cities. 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, Non-EU. https://doi.org/10.1145/3384419.3430445
  • Analysis of Bayesian Networks via Prob-Solvable Loops / 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. https://doi.org/10.1007/978-3-030-64276-1_12
  • Mora - Automatic Generation of Moment-Based Invariants / 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. https://doi.org/10.1007/978-3-030-45190-5_28
  • MoonLight: A Lightweight Tool for Monitoring Spatio-Temporal Properties / 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. https://doi.org/10.1007/978-3-030-60508-7_23
  • Runtime Verification of Autonomous Driving Systems in CARLA / Zapridou, E., Bartocci, E., & Katsaros, P. (2020). Runtime Verification of Autonomous Driving Systems in CARLA. In Runtime Verification (pp. 172–183). Springer. https://doi.org/10.1007/978-3-030-60508-7_9
  • Parameter Synthesis for Probabilistic Hyperproperties / Abraham, E., Bartocci, E., Bonakdarpour, B., & Dobe, O. (2020). Parameter Synthesis for Probabilistic Hyperproperties. In EPiC Series in Computing. Proc. of LPAR 2020: the 23rd International Conference on Logic for Programming, Alicante, Spain (Virtual due to covid19), EU. https://doi.org/10.29007/37lf
  • CPSDebug: a tool for explanation of failures in cyber-physical systems / 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, USA, Non-EU. ACM. https://doi.org/10.1145/3395363.3404369
  • Probabilistic Hyperproperties with Nondeterminism / Ábrahám, E., Bartocci, E., Bonakdarpour, B., & Dobe, O. (2020). Probabilistic Hyperproperties with Nondeterminism. In Automated Technology for Verification and Analysis (pp. 518–534). https://doi.org/10.1007/978-3-030-59152-6_29
  • SaSTL: Spatial Aggregation Signal Temporal Logic for Runtime Monitoring in Smart Cities / 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, Australia, Non-EU. IEEE. https://doi.org/10.1109/iccps48487.2020.00013
  • Monitoring Spatio-Temporal Properties (Invited Tutorial) / Nenzi, L., Bartocci, E., Bortolussi, L., Loreti, M., & Visconti, E. (2020). Monitoring Spatio-Temporal Properties (Invited Tutorial). In Lecture Notes in Computer Science. Proc. of RV 2020: the 20th International Conference on Runtime Verification, Los Angeles, CA (Virtual), Non-EU. Springer. https://doi.org/10.1007/978-3-030-60508-7

2019

  • Quantitative Regular Expressions for Arrhythmia Detection / 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. https://doi.org/10.1109/tcbb.2018.2885274
  • A Roadmap Toward the Resilient Internet of Things for Cyber-Physical Systems / 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. https://doi.org/10.1109/access.2019.2891969
  • Parallel reachability analysis of hybrid systems in XSpeed / 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. https://doi.org/10.1007/s10009-018-0485-6
  • A survey of challenges for runtime verification from advanced application domains (beyond software) / 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. https://doi.org/10.1007/s10703-019-00337-w
  • Automatic Generation of Moment-Based Invariants for Prob-Solvable Loops / 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. https://doi.org/10.1007/978-3-030-31784-3_15
  • Piecewise Robust Barrier Tubes for Nonlinear Hybrid Systems with Uncertainty / 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. https://doi.org/10.1007/978-3-030-29662-9_8
  • Capacitive Soil Moisture Sensor Node for IoT in Agriculture and Home / 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, Italien, EU. https://doi.org/10.1109/isce.2019.8901012
  • International Competition on Runtime Verification (CRV) / 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). https://doi.org/10.1007/978-3-030-17502-3_3
  • Automatic Failure Explanation in CPS Models / Bartocci, E., Manjunath, N., Mariani, L., Mateis, C., & Nickovic, D. (2019). Automatic Failure Explanation in CPS Models. In Lecture Notes in Computer Science. 17th International Conference on Software Engineering and Formal Methods, Oslo, Norway, EU. https://doi.org/10.1007/978-3-030-30446-1
  • Control from Signal Temporal Logic Specifications with Smooth Cumulative Quantitative Semantics / 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, EU. IEEE. http://hdl.handle.net/20.500.12708/57866
  • Adaptive Fault Detection Exploiting Redundancy with Uncertainties in Space and Time / 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, EU. IEEE. https://doi.org/10.1109/saso.2019.00013
  • Extending a Hodgkin-Huxley Model for Larval Drosophila Muscle Excitability via Particle Swarm Fitting / 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 Lecture Notes in Computer Science. 17th International Conference on Computational Methods in Systems Biology, Trieste, EU. https://doi.org/10.1007/978-3-030-31304-3
  • TOOLympics 2019: An Overview of Competitions in Formal Methods / Bartocci, E., Beyer, D., & Black, P. (2019). TOOLympics 2019: An Overview of Competitions in Formal Methods. In Lecture Notes in Computer Science. Tools and Algorithms for the Construction and Analysis of Systems- 25 Years of TACAS, Prague, Czech Republic, EU. https://doi.org/10.1007/978-3-030-17502-3
  • From Reactive Systems to Cyber-Physical Systems / From Reactive Systems to Cyber-Physical Systems. (2019). In E. Bartocci, R. Cleaveland, R. Grosu, & O. Sokolsky (Eds.), Lecture Notes in Computer Science. Springer-Verlag Berlin Heidelberg. https://doi.org/10.1007/978-3-030-31514-6
  • First international Competition on Runtime Verification: rules, benchmarks, tools, and final results of CRV 2014 / 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. https://doi.org/10.1007/s10009-017-0454-5

2018

  • A Formal Methods Approach to Pattern Recognition and Synthesis in Reaction Diffusion Networks / 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. https://doi.org/10.1109/tcns.2016.2609138
  • Quantitative monitoring of STL with edit distance / 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. https://doi.org/10.1007/s10703-018-0319-x
  • An algebraic framework for runtime verification / 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. https://doi.org/10.1109/tcad.2018.2858460
  • Guest Editors' Introduction to the Special Section on the 14th International Conference on Computational Methods in Systems Biology (CMSB 2016) / 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. https://doi.org/10.1109/tcbb.2018.2816979
  • Formal analysis of cyber-physical systems / Bartocci, E. (2018). Formal analysis of cyber-physical systems [Professorial Dissertation, Technische Universität]. reposiTUm. http://hdl.handle.net/20.500.12708/159429
  • Localizing Faults in Simulink/Stateflow Models with {STL} / 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, EU. https://doi.org/10.1145/3178126.3178131
  • A Counting Semantics for Monitoring LTL Specifications over Finite Traces / 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. https://doi.org/10.1007/978-3-319-96145-3_29
  • Parameter-Independent Strategies for pMDPs via POMDPs / 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. https://doi.org/10.1007/978-3-319-99154-2_4
  • Reachable Set Over-Approximation for Nonlinear Systems Using Piecewise Barrier Tubes / 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. https://doi.org/10.1007/978-3-319-96145-3_24
  • Monitoring, Learning and Control of Cyber-Physical Systems with STL (Tutorial) / 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. https://doi.org/10.1007/978-3-030-03769-7_4
  • Introduction to Runtime Verification / 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 (pp. 1–33). Springer-Verlag Berlin Heidelberg. https://doi.org/10.1007/978-3-319-75632-5_1
  • Specification-Based Monitoring of Cyber-Physical Systems: A Survey on Theory, Tools and Applications / 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. https://doi.org/10.1007/978-3-319-75632-5_5
  • Lectures on Runtime Verification / Bartocci, E., & Falcone, Y. (Eds.). (2018). Lectures on Runtime Verification. Springer-Verlag. https://doi.org/10.1007/978-3-319-75632-5
  • RV-TheToP: Runtime Verification from Theory to the Industry Practice (Track Introduction) / Bartocci, E., & Falcone, Y. (2018). RV-TheToP: Runtime Verification from Theory to the Industry Practice (Track Introduction). In Lecture Notes in Computer Science (pp. 3–8). Springer International Publishing. https://doi.org/10.1007/978-3-030-03427-6_1
  • Signal Convolution Logic / Silvetti, S., Nenzi, L., Bartocci, E., & Bortolussi, L. (2018). Signal Convolution Logic. In Automated Technology for Verification and Analysis (pp. 267–283). https://doi.org/10.1007/978-3-030-01090-4_16
  • Verifying nonlinear analog and mixed-signal circuits with inputs / Fan, C., Meng, Y., Maier, J., Bartocci, E., Mitra, S., & Schmid, U. (2018). Verifying nonlinear analog and mixed-signal circuits with inputs. In IFAC-PapersOnLine (pp. 241–246). IFAC-PapersOnLine. https://doi.org/10.1016/j.ifacol.2018.08.041
  • A Robust Genetic Algorithm for Learning Temporal Specifications from Data / Nenzi, L., Silvetti, S., Bartocci, E., & Bortolussi, L. (2018). A Robust Genetic Algorithm for Learning Temporal Specifications from Data. In Lecture Notes in Computer Science. Proc. of QEST 2018: the 15th International Conference on Quantitative Evaluation of Systems, Beijing, China, Non-EU. https://doi.org/10.1007/978-3-319-99154-2

2017

  • Policy learning in Continuous-Time Markov Decision Processes using Gaussian Processes / Bartocci, E., Bortolussi, L., Brazdil, T., Milos, D., & Sanguinetti, G. (2017). Policy learning in Continuous-Time Markov Decision Processes using Gaussian Processes. Performance Evaluation, 116, 84–100. https://doi.org/10.1016/j.peva.2017.08.007
  • ARES: Adaptive Receding-Horizon Synthesis of Optimal Plans / 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. https://doi.org/10.1007/978-3-662-54580-5_17
  • Computing with Biophysical and Hardware-efficient Neural Models / 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. https://doi.org/10.1007/978-3-319-59153-7_46
  • Quantitative Regular Expressions for Arrhythmia Detection Algorithms / 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. https://doi.org/10.1007/978-3-319-67471-1_2
  • SEA-PARAM: Exploring Schedulers in Parametric MDPs / 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. https://doi.org/10.4204/eptcs.250.3
  • Runtime Monitoring with Recovery of the SENT Communication Protocol / 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. https://doi.org/10.1007/978-3-319-63387-9_17
  • Monitoring mobile and spatially distributed cyber-physical systems / 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, Vienna, Austria, EU. ACM. https://doi.org/10.1145/3127041.3127050
  • A Probabilistic Small Model Theorem to Assess Confidentiality of Dispersed Cloud Storage / 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. https://doi.org/10.1007/978-3-319-66335-7_8
  • A Linear Programming-based Iterative Approach to Stabilizing Polynomial Dynamics / Ben Sassi, M. A., Bartocci, E., & Sankaranarayanan, S. (2017). A Linear Programming-based Iterative Approach to Stabilizing Polynomial Dynamics. In IFAC-PapersOnLine (pp. 10462–10469). Elsevier. https://doi.org/10.1016/j.ifacol.2017.08.1976
  • SMT-based Synthesis of Safe and Robust PID Controllers for Stochastic Hybrid Systems / 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. https://doi.org/10.1007/978-3-319-70389-3_9

2016

  • Preface of the special issue on Model Checking of Software : Selected papers of the 20th International SPIN Symposium on Model Checking of Software / 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. https://doi.org/10.1007/s10009-016-0414-5
  • Computational modeling, formal analysis and tools for systems biology / Bartocci, E., & Lió, P. (2016). Computational modeling, formal analysis and tools for systems biology. PLoS Computational Biology, 12(1), e1004591. https://doi.org/10.1371/journal.pcbi.1004591
  • Computational Methods in Systems Biology / Bartocci, E., Lio, P., & Paoletti, N. (Eds.). (2016). Computational Methods in Systems Biology. Springer International Publishing. https://doi.org/10.1007/978-3-319-45177-0
  • Parallel reachability analysis for hybrid systems / 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, Non-EU. https://doi.org/10.1109/memcod.2016.7797741
  • Monitoring of MTL Specifications With IBM's Spiking-Neuron Model / 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. http://hdl.handle.net/20.500.12708/56706
  • Applying High-Level Synthesis for Synthesizing Hardware Runtime STL Monitors of Mission-Critical Properties / 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. http://hdl.handle.net/20.500.12708/56824
  • The HARMONIA Project: Hardware Monitoring for Automotive Systems-of-Systems / 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 Leveraging Applications of Formal Methods, Verification and Validation: Discussion, Dissemination, Applications (pp. 371–379). Springer International Publishing. https://doi.org/10.1007/978-3-319-47169-3_28
  • Runtime Verification and Enforcement, the (Industrial) Application Perspective (Track Introduction) / Bartocci, E., & Falcone, Y. (2016). Runtime Verification and Enforcement, the (Industrial) Application Perspective (Track Introduction). In Leveraging Applications of Formal Methods, Verification and Validation: Discussion, Dissemination, Applications (pp. 333–338). Springer International Publishing. https://doi.org/10.1007/978-3-319-47169-3_24
  • Discrete Abstraction of Multiaffine Systems / 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. https://doi.org/10.1007/978-3-319-47151-8_9
  • Feedback Control for Statistical Model Checking of Cyber-Physical Systems / Kalajdzic, K., Jegourel, C., Legay, A., Bartocci, E., Lukina, A., Smolka, S. A., & Grosu, R. (2016). Feedback Control for Statistical Model Checking of Cyber-Physical Systems. In Leveraging Applications of Formal Methods, Verification and Validation: Foundational Techniques (pp. 46–61). Springer International Publishing. https://doi.org/10.1007/978-3-319-47166-2_4
  • Temporal Logic as Filtering / 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. https://doi.org/10.1145/2883817.2883839
  • Policy Learning for Time-Bounded Reachability in Continuous-Time Markov Decision Processes via Doubly-Stochastic Gradient Ascent / 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. https://doi.org/10.1007/978-3-319-43425-4_17
  • Quantitative Monitoring of STL with Edit Distance / 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. https://doi.org/10.1007/978-3-319-46982-9_13
  • Applying Runtime Monitoring for Automotive Electronic Development / 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. https://doi.org/10.1007/978-3-319-46982-9_30

2015

  • XSpeed: Accelerating Reachability Analysis on Multi-core Processors / 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. https://doi.org/10.1007/978-3-319-26287-1_1
  • System Design of Stochastic Models using Robustness of Temporal Properties / 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. https://doi.org/10.1016/j.tcs.2015.02.046
  • Model-Order Reduction of Ion Channel Dynamics Using Approximate Bisimulation / 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. https://doi.org/10.1016/j.tcs.2014.03.018
  • Runtime Verification / Bartocci, E., & Majumdar, R. (Eds.). (2015). Runtime Verification. Springer International Publishing. https://doi.org/10.1007/978-3-319-23820-3
  • SpaTeL / Haghighi, I., Jones, A., Kong, Z., Bartocci, E., Gros, R., & Belta, C. (2015). SpaTeL. In Proceedings of the 18th International Conference on Hybrid Systems: Computation and Control. 18th International Conference on Hybrid Systems: Computation and Control (HSCC), Seattle, USA, Non-EU. ACM. https://doi.org/10.1145/2728606.2728633
  • Neural Programming: Towards adaptive control in Cyber-Physical Systems / 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, Non-EU. IEEE Computer Society. https://doi.org/10.1109/cdc.2015.7403319
  • Studying Emergent Behaviours in Morphogenesis using Signal Spatio-Temporal Logic / 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. http://hdl.handle.net/20.500.12708/56256
  • Explaining Heisenbugs / Weissenbacher, G. (2015). Explaining Heisenbugs. In E. Bartocci & R. Majumdar (Eds.), Runtime Verification (p. XV). Lecture Notes in Computer Science/Springer. http://hdl.handle.net/20.500.12708/56231
  • From signal temporal logic to FPGA monitors / 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, TX, USA, Non-EU. IEEE. https://doi.org/10.1109/memcod.2015.7340489
  • Abstraction-Based Parameter Synthesis for Multiaffine Systems / 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. https://doi.org/10.1007/978-3-319-26287-1_2

2014

  • Cyber-Physical Systems: Theoretical and Practical Challenges / Bartocci, E., Höftberger, O., & Grosu, R. (2014). Cyber-Physical Systems: Theoretical and Practical Challenges. ERCIM NEWS, 2014(97), 8–9. http://hdl.handle.net/20.500.12708/157429
  • Hybrid Systems and Biology / Bartocci, E., Bortolussi, L., & Smolka, S. A. (2014). Hybrid Systems and Biology. Information and Computation, 236, 1–2. https://doi.org/10.1016/j.ic.2014.01.008
  • Tracking Action Potentials of Nonlinear Excitable Cells using Model Predictive Control / 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. http://hdl.handle.net/20.500.12708/55802
  • A Formal Methods Approach to Pattern Synthesis in Reaction Diffusion Systems / 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. http://hdl.handle.net/20.500.12708/55797
  • Towards a GPGPU-parallel SPIN model checker / 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, Non-EU. ACM. https://doi.org/10.1145/2632362.2632379
  • Medical Cyber-Physical Systems / 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 (pp. 353–355). https://doi.org/10.1007/978-3-662-45231-8_25
  • Temporal Logic Based Monitoring of Assisted Ventilation in Intensive Care Patients / 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 Leveraging Applications of Formal Methods, Verification and Validation. Specialized Techniques and Applications (pp. 391–403). https://doi.org/10.1007/978-3-662-45231-8_30
  • Data-Driven Statistical Learning of Temporal Logic Properties / Bartocci, E., Bortolussi, L., & Sanguinetti, G. (2014). Data-Driven Statistical Learning of Temporal Logic Properties. In Lecture Notes in Computer Science (pp. 23–37). LNCS/Springer. https://doi.org/10.1007/978-3-319-10512-3_3
  • First International Competition of Software for Runtime Verification / Bartocci, E., Bonakdarpour, B., & Falcone, Y. (2014). First International Competition of Software for Runtime Verification. In Lecture Notes in Computer Science. 14th International Conference on Runtime Verification, Canada, Non-EU. https://doi.org/10.1007/978-3-319-11164-3

2013

  • Curvature Analysis of Cardiac Excitation Wavefronts / 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. https://doi.org/10.1109/tcbb.2012.125
  • Model Checking Software / Bartocci, E., & Ramakrishnan, C. R. (Eds.). (2013). Model Checking Software. Springer-Verlag Berlin Heidelberg. https://doi.org/10.1007/978-3-642-39176-7
  • Monitoring with uncertainty / Bartocci, E., & Grosu, R. (2013). Monitoring with uncertainty. In Electronic Proceedings in Theoretical Computer Science (pp. 1–4). Electronic Proceedings in Theoretical Computer Science. https://doi.org/10.4204/eptcs.124.1
  • Sampling-based Decentralized Monitoring for Networked Embedded Systems / 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. https://doi.org/10.4204/eptcs.124.9
  • On the Robustness of Temporal Properties for Stochastic Models / 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. https://doi.org/10.4204/eptcs.125.1
  • A Temporal Logic Approach to Modular Design of Synthetic Biological Circuits / 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. https://doi.org/10.1007/978-3-642-40708-6_13
  • Runtime Verification with Particle Filtering / 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. https://doi.org/10.1007/978-3-642-40787-1_9

2012

  • UBioLab: a web-LABoratory for Ubiquitous in-silico experiments / 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, 9(1), 1–20. https://doi.org/10.2390/biecoll-jib-2012-192
  • Multiple Verification in Complex Biological Systems: The Bone Remodelling Case Study / Bartocci, E., Liò, P., Merelli, E., & Paoletti, N. (2012). Multiple Verification in Complex Biological Systems: The Bone Remodelling Case Study. Lecture Notes in Computer Science, 53–76. https://doi.org/10.1007/978-3-642-35524-0_3
  • Proceedings First International Workshop on Hybrid Systems and Biology / Bartocci, E., & Bortolussi, L. (Eds.). (2012). Proceedings First International Workshop on Hybrid Systems and Biology. Electronic Proceedings in Theoretical Computer Science. https://doi.org/10.4204/EPTCS.92
  • On Temporal Logic and Signal Processing / 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. https://doi.org/10.1007/978-3-642-33386-6_9
  • Approximate Bisimulations for Sodium Channel Dynamics / 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. https://doi.org/10.1007/978-3-642-33636-2_16
  • Adaptive Runtime Verification / 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. https://doi.org/10.1007/978-3-642-35632-2_18
  • Runtime Verification with State Estimation / 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. https://doi.org/10.1007/978-3-642-29860-8_15

2011

  • Teaching cardiac electrophysiology modeling to undergraduate students: Laboratory exercises and GPU programming for the study of arrhythmias and spiral wave dynamics / Bartocci, E. (2011). Teaching cardiac electrophysiology modeling to undergraduate students: Laboratory exercises and GPU programming for the study of arrhythmias and spiral wave dynamics. Advances in Physiology Education, 35(4), 427–437. https://doi.org/10.1152/advan.00034.2011
  • Modeling the cell cycle: From deterministic models to hybrid systems / Alfieri, R., Bartocci, E., Merelli, E., & Milanesi, L. (2011). Modeling the cell cycle: From deterministic models to hybrid systems. BioSystems, 105(1), 34–40. https://doi.org/10.1016/j.biosystems.2011.03.002
  • Model Repair for Probabilistic Systems / 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. https://doi.org/10.1007/978-3-642-19835-9_30
  • Curvature analysis of cardiac excitation wavefronts / 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, EU. ACM. https://doi.org/10.1145/2037509.2037532
  • Toward real-time simulation of cardiac dynamics / 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, EU. ACM. https://doi.org/10.1145/2037509.2037525
  • From Cardiac Cells to Genetic Regulatory Networks / 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. https://doi.org/10.1007/978-3-642-22110-1_31

 

Note: Due to the rollout of TU Wien’s new publication database, the list below may be slightly outdated. Once the migration is complete, everything will be up to date again.

  • 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

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 Bartocci’s research profile in TISS .