TU Wien Informatics

20 Years
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.

Roles

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

Contact

2024W

2025S

 

2024

  • Exact and Approximate Moment Derivation for Probabilistic Loops With Non-Polynomial Assignments / 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. https://doi.org/10.1145/3641545
    Download: PDF (2.59 MB)
    Projects: ARTIST (2021–2026) / ProbInG (2020–2025)
  • Distillation based Robustness Verification with PAC Guarantees / 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 Volume 235: International Conference on Machine Learning, 21-27 July 2024, Vienna, Austria. 41st International Conference on Machine Learning (ICML 2024), Vienna, Austria.
  • (Un)Solvable loop analysis / Amrollahi, D., Bartocci, E., Kenison, G. J., Kovacs, L., Moosbrugger, M., & Stankovic, M. (2024). (Un)Solvable loop analysis. Formal Methods in System Design. https://doi.org/10.1007/s10703-024-00455-0
    Projects: ARTIST (2021–2026) / ProbInG (2020–2025)
  • Information-flow interfaces / Bartocci, E., Ferrère, T., Henzinger, T., Nickovic, D., & Oliveira da Costa, A. (2024). Information-flow interfaces. Formal Methods in System Design. https://doi.org/10.1007/s10703-024-00447-0
  • Adaptable Configuration of Decentralized Monitors / 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. https://doi.org/10.1007/978-3-031-62645-6_11
    Projects: TAIGER (2023–2027) / ZK 35-G (2019–2024)
  • Verifying Global Two-Safety Properties in Neural Networks with Confidence / 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. https://doi.org/10.1007/978-3-031-65630-9_17
    Projects: Browsec (2018–2024) / ForSmart (2023–2027) / ProbInG (2020–2025) / SFB SPyCoDe (2023–2026) / TAIGER (2023–2027)
  • Quantifying Uncertainty in Probabilistic Loops Without Sampling: A Fully Automated Approach / 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. https://doi.org/10.1007/978-3-031-72621-7_1
    Project: ProbInG (2020–2025)
  • Probabilistic Loop Synthesis from Sequences of Moments / 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). https://doi.org/10.1007/978-3-031-68416-6_14
    Projects: ProbInG (2020–2025) / TAIGER (2023–2027)

2023

  • An Energy-Aware Approach to Design Self-Adaptive AI-based Applications on the Edge / 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. https://doi.org/10.1109/ASE56229.2023.00046
    Projects: Intrasafed 5G (2020–2021) / RUCON (2016–2023) / SWAIN (2021–2024) / TRITON FWF (2023–2027)
  • Lightweight Verification of Hyperproperties / 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. https://doi.org/10.1007/978-3-031-45332-8_1
    Project: ZK 35-G (2019–2024)
  • Mining Specification Parameters for Multi-class Classification / 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. https://doi.org/10.1007/978-3-031-44267-4_5
    Project: ProbInG (2020–2025)
  • Introducing Asynchronicity to Probabilistic Hyperproperties / 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. https://doi.org/10.1007/978-3-031-43835-6_4
    Project: ProbInG (2020–2025)
  • TD-Magic: From Pictures of Timing Diagrams To Formal Specifications / 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. https://doi.org/10.1109/DAC56929.2023.10247685
    Project: ADEX (2020–2024)
  • Deductive Controller Synthesis for Probabilistic Hyperproperties / 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. https://doi.org/10.1007/978-3-031-43835-6_20
    Project: ProbInG (2020–2025)
  • Hypernode Automata / 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. https://doi.org/10.4230/LIPIcs.CONCUR.2023.21
    Project: ZK 35-G (2019–2024)
  • Mining Hyperproperties using Temporal Logics / Bartocci, E., Mateis, C., Nesterini, E., & Nickovic, D. (2023). Mining Hyperproperties using Temporal Logics. ACM Transactions on Embedded Computing Systems, 22(5s), 1–26. https://doi.org/10.1145/3609394
  • MoonLight: a lightweight tool for monitoring spatio-temporal properties / 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. https://doi.org/10.1007/s10009-023-00710-5
    Project: ZK 35-G (2019–2024)
  • Provable Correct and Adaptive Simplex Architecture for Bounded-Liveness Properties / 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. https://doi.org/10.1007/978-3-031-32157-3_8
    Project: ZK 35-G (2019–2024)
  • Property-Based Mutation Testing / 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. https://doi.org/10.1109/ICST57152.2023.00029
  • Progression for Monitoring in Temporal ASP / 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. https://doi.org/10.3233/FAIA230513
    Download: PDF (343 KB)
    Project: TAIGER (2023–2027)

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
    Download: FIM: Fault Injection and Mutation for Simulink (212 KB)
  • 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
  • Distribution Estimation for Probabilistic Loops / 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. https://doi.org/10.1007/978-3-031-16336-4_2
    Projects: ARTIST (2021–2026) / ProbInG (2020–2025)
  • The probabilistic termination tool amber / Moosbrugger, M., Bartocci, E., Katoen, J.-P., & Kovacs, L. (2022). The probabilistic termination tool amber. Formal Methods in System Design, 61(1), 90–109. https://doi.org/10.1007/s10703-023-00424-z
    Projects: ARTIST (2021–2026) / ProbInG (2020–2025)
  • 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
  • Probabilistic Hyperproperties with Rewards / 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. https://doi.org/10.1007/978-3-031-06773-0_35
  • 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
  • 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
  • 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 (2021–2026) / ProbInG (2020–2025)
  • 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
    Download: PDF (1.62 MB)
    Project: RTD-Indian (2017–2022)
  • 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 Verification, Model Checking, and Abstract Interpretation : 23rd International Conference, VMCAI 2022, Philadelphia, PA, USA, January 16–18, 2022, Proceedings (pp. 1–19). Springer. https://doi.org/10.1007/978-3-030-94583-1_1
  • 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
  • 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 (2017–2022)
  • 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
  • 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

2021

  • 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
    Download: PDF (1.88 MB)
    Project: IoT4CPS (2017–2020)
  • 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
  • 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
  • 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
  • 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
  • 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, United States of America (the). https://doi.org/10.1109/cdc45484.2021.9682921
  • 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), China. https://doi.org/10.1145/3487212.3487344
  • 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
  • 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
  • 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
  • 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

2020

  • Mining Shape Expressions from Positive Examples / 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. https://doi.org/10.1109/tcad.2020.3012240
  • Monitoring Spatio-Temporal Properties (Invited Tutorial) / 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. https://doi.org/10.1007/978-3-030-60508-7_2
  • 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. 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
  • 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
  • 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, United States of America (the). 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. IEEE. https://doi.org/10.1109/iccps48487.2020.00013
  • 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
  • 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 (Virtual due to covid19), Spain. https://doi.org/10.29007/37lf
  • 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

2019

  • 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
    Download: PDF (1.37 MB)
  • 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 Failure Explanation in CPS Models / 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. https://doi.org/10.1007/978-3-030-30446-1_4
  • 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 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. https://doi.org/10.1007/978-3-030-17502-3_1
  • 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 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. https://doi.org/10.1007/978-3-030-31304-3_7
  • 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, Italy. 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
  • 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. 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. IEEE. https://doi.org/10.1109/saso.2019.00013
  • 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
  • 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

2018

  • 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 (Vol. 10457, pp. 1–33). Springer-Verlag Berlin Heidelberg. https://doi.org/10.1007/978-3-319-75632-5_1
  • 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 T. Margaria & B. Steffen (Eds.), Leveraging Applications of Formal Methods, Verification and Validation. Industrial Practice. ISoLA 2018, Proceedings, Part IV (pp. 3–8). Springer. https://doi.org/10.1007/978-3-030-03427-6_1
  • 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 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, Beijing, China, Non-EU. https://doi.org/10.1007/978-3-319-99154-2_20
  • 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
  • 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
  • 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
  • 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
  • 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
  • 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
  • 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
  • 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
  • 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
  • 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

2017

  • Policy learning in Continuous-Time Markov Decision Processes using Gaussian Processes / 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. 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
  • 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
  • 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
  • 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
    Download: PDF (328 KB)
  • 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 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. https://doi.org/10.1007/978-3-319-47169-3_24
  • Feedback Control for Statistical Model Checking of Cyber-Physical Systems / 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. https://doi.org/10.1007/978-3-319-47166-2_4
  • 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 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. https://doi.org/10.1007/978-3-319-47169-3_28
  • 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
  • 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
  • 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
  • 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
  • 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
  • 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
  • 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
  • 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
  • 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
  • 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
  • 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

  • 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 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. https://doi.org/10.1007/978-3-662-45231-8_30
  • 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. ISoLA 2014, Proceedings, Part II (pp. 353–355). Springer. https://doi.org/10.1007/978-3-662-45231-8_25
  • Data-Driven Statistical Learning of Temporal Logic Properties / 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. 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 Runtime Verification 5th International Conference, RV 2014, Toronto, ON, Canada, September 22-25, 2014. Proceedings. 14th International Conference on Runtime Verification, Canada, Non-EU. https://doi.org/10.1007/978-3-319-11164-3_1
  • 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

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
  • 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
  • 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
  • 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
  • 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
  • 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
  • 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
  • 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

  • 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

 

  • 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 .