[{"ddc":["000"],"status":"public","title":"How many bits does it take to quantize your neural network?","intvolume":" 12079","_id":"7808","user_id":"2DF688A6-F248-11E8-B48F-1D18A9856A87","file":[{"file_id":"7893","relation":"main_file","date_created":"2020-05-26T12:48:15Z","date_updated":"2020-07-14T12:48:03Z","checksum":"f19905a42891fe5ce93d69143fa3f6fb","file_name":"2020_TACAS_Giacobbe.pdf","access_level":"open_access","creator":"dernst","file_size":2744030,"content_type":"application/pdf"}],"oa_version":"Published Version","alternative_title":["LNCS"],"type":"conference","abstract":[{"lang":"eng","text":"Quantization converts neural networks into low-bit fixed-point computations which can be carried out by efficient integer-only hardware, and is standard practice for the deployment of neural networks on real-time embedded devices. However, like their real-numbered counterpart, quantized networks are not immune to malicious misclassification caused by adversarial attacks. We investigate how quantization affects a network’s robustness to adversarial attacks, which is a formal verification question. We show that neither robustness nor non-robustness are monotonic with changing the number of bits for the representation and, also, neither are preserved by quantization from a real-numbered network. For this reason, we introduce a verification method for quantized neural networks which, using SMT solving over bit-vectors, accounts for their exact, bit-precise semantics. We built a tool and analyzed the effect of quantization on a classifier for the MNIST dataset. We demonstrate that, compared to our method, existing methods for the analysis of real-numbered networks often derive false conclusions about their quantizations, both when determining robustness and when detecting attacks, and that existing methods for quantized networks often miss attacks. Furthermore, we applied our method beyond robustness, showing how the number of bits in quantization enlarges the gender bias of a predictor for students’ grades."}],"page":"79-97","publication":"International Conference on Tools and Algorithms for the Construction and Analysis of Systems","citation":{"chicago":"Giacobbe, Mirco, Thomas A Henzinger, and Mathias Lechner. “How Many Bits Does It Take to Quantize Your Neural Network?” In International Conference on Tools and Algorithms for the Construction and Analysis of Systems, 12079:79–97. Springer Nature, 2020. https://doi.org/10.1007/978-3-030-45237-7_5.","mla":"Giacobbe, Mirco, et al. “How Many Bits Does It Take to Quantize Your Neural Network?” International Conference on Tools and Algorithms for the Construction and Analysis of Systems, vol. 12079, Springer Nature, 2020, pp. 79–97, doi:10.1007/978-3-030-45237-7_5.","short":"M. Giacobbe, T.A. Henzinger, M. Lechner, in:, International Conference on Tools and Algorithms for the Construction and Analysis of Systems, Springer Nature, 2020, pp. 79–97.","ista":"Giacobbe M, Henzinger TA, Lechner M. 2020. How many bits does it take to quantize your neural network? International Conference on Tools and Algorithms for the Construction and Analysis of Systems. TACAS: Tools and Algorithms for the Construction and Analysis of Systems, LNCS, vol. 12079, 79–97.","apa":"Giacobbe, M., Henzinger, T. A., & Lechner, M. (2020). How many bits does it take to quantize your neural network? In International Conference on Tools and Algorithms for the Construction and Analysis of Systems (Vol. 12079, pp. 79–97). Dublin, Ireland: Springer Nature. https://doi.org/10.1007/978-3-030-45237-7_5","ieee":"M. Giacobbe, T. A. Henzinger, and M. Lechner, “How many bits does it take to quantize your neural network?,” in International Conference on Tools and Algorithms for the Construction and Analysis of Systems, Dublin, Ireland, 2020, vol. 12079, pp. 79–97.","ama":"Giacobbe M, Henzinger TA, Lechner M. How many bits does it take to quantize your neural network? In: International Conference on Tools and Algorithms for the Construction and Analysis of Systems. Vol 12079. Springer Nature; 2020:79-97. doi:10.1007/978-3-030-45237-7_5"},"date_published":"2020-04-17T00:00:00Z","scopus_import":1,"day":"17","article_processing_charge":"No","has_accepted_license":"1","publication_status":"published","department":[{"_id":"ToHe"}],"publisher":"Springer Nature","year":"2020","date_updated":"2023-06-23T07:01:11Z","date_created":"2020-05-10T22:00:49Z","volume":12079,"author":[{"full_name":"Giacobbe, Mirco","first_name":"Mirco","last_name":"Giacobbe","id":"3444EA5E-F248-11E8-B48F-1D18A9856A87","orcid":"0000-0001-8180-0904"},{"id":"40876CD8-F248-11E8-B48F-1D18A9856A87","orcid":"0000-0002-2985-7724","first_name":"Thomas A","last_name":"Henzinger","full_name":"Henzinger, Thomas A"},{"full_name":"Lechner, Mathias","id":"3DC22916-F248-11E8-B48F-1D18A9856A87","first_name":"Mathias","last_name":"Lechner"}],"related_material":{"record":[{"relation":"dissertation_contains","status":"public","id":"11362"}]},"license":"https://creativecommons.org/licenses/by/4.0/","file_date_updated":"2020-07-14T12:48:03Z","quality_controlled":"1","project":[{"call_identifier":"FWF","name":"Rigorous Systems Engineering","_id":"25832EC2-B435-11E9-9278-68D0E5697425","grant_number":"S 11407_N23"},{"grant_number":"Z211","_id":"25F42A32-B435-11E9-9278-68D0E5697425","call_identifier":"FWF","name":"The Wittgenstein Prize"}],"oa":1,"tmp":{"name":"Creative Commons Attribution 4.0 International Public License (CC-BY 4.0)","legal_code_url":"https://creativecommons.org/licenses/by/4.0/legalcode","short":"CC BY (4.0)","image":"/images/cc_by.png"},"language":[{"iso":"eng"}],"conference":{"location":"Dublin, Ireland","start_date":"2020-04-25","end_date":"2020-04-30","name":"TACAS: Tools and Algorithms for the Construction and Analysis of Systems"},"doi":"10.1007/978-3-030-45237-7_5","month":"04","publication_identifier":{"issn":["03029743"],"isbn":["9783030452360"],"eissn":["16113349"]}},{"oa_version":"Published Version","file":[{"checksum":"4b92e333db7b4e2349501a804dfede69","success":1,"date_created":"2022-05-17T06:55:49Z","date_updated":"2022-05-17T06:55:49Z","relation":"main_file","file_id":"11391","file_size":346415,"content_type":"application/pdf","creator":"dernst","access_level":"open_access","file_name":"2019_EPiCs_Frehse.pdf"}],"title":"ARCH-COMP19 Category Report: Hybrid systems with piecewise constant dynamics","ddc":["000"],"status":"public","intvolume":" 61","user_id":"2DF688A6-F248-11E8-B48F-1D18A9856A87","_id":"10877","abstract":[{"lang":"eng","text":"This report presents the results of a friendly competition for formal verification of continuous and hybrid systems with piecewise constant dynamics. The friendly competition took place as part of the workshop Applied Verification for Continuous and Hybrid Systems (ARCH) in 2019. In this third edition, six tools have been applied to solve five different benchmark problems in the category for piecewise constant dynamics: BACH, Lyse, Hy- COMP, PHAVer/SX, PHAVerLite, and VeriSiMPL. Compared to last year, a new tool has participated (HyCOMP) and PHAVerLite has replaced PHAVer-lite. The result is a snap- shot of the current landscape of tools and the types of benchmarks they are particularly suited for. Due to the diversity of problems, we are not ranking tools, yet the presented results probably provide the most complete assessment of tools for the safety verification of continuous and hybrid systems with piecewise constant dynamics up to this date."}],"alternative_title":["EPiC Series in Computing"],"type":"conference","date_published":"2019-05-25T00:00:00Z","page":"1-13","publication":"ARCH19. 6th International Workshop on Applied Verification of Continuous and Hybrid Systems","citation":{"chicago":"Frehse, Goran, Alessandro Abate, Dieky Adzkiya, Anna Becchi, Lei Bu, Alessandro Cimatti, Mirco Giacobbe, et al. “ARCH-COMP19 Category Report: Hybrid Systems with Piecewise Constant Dynamics.” In ARCH19. 6th International Workshop on Applied Verification of Continuous and Hybrid Systems, edited by Goran Frehse and Matthias Althoff, 61:1–13. EasyChair, 2019. https://doi.org/10.29007/rjwn.","mla":"Frehse, Goran, et al. “ARCH-COMP19 Category Report: Hybrid Systems with Piecewise Constant Dynamics.” ARCH19. 6th International Workshop on Applied Verification of Continuous and Hybrid Systems, edited by Goran Frehse and Matthias Althoff, vol. 61, EasyChair, 2019, pp. 1–13, doi:10.29007/rjwn.","short":"G. Frehse, A. Abate, D. Adzkiya, A. Becchi, L. Bu, A. Cimatti, M. Giacobbe, A. Griggio, S. Mover, M.S. Mufid, I. Riouak, S. Tonetta, E. Zaffanella, in:, G. Frehse, M. Althoff (Eds.), ARCH19. 6th International Workshop on Applied Verification of Continuous and Hybrid Systems, EasyChair, 2019, pp. 1–13.","ista":"Frehse G, Abate A, Adzkiya D, Becchi A, Bu L, Cimatti A, Giacobbe M, Griggio A, Mover S, Mufid MS, Riouak I, Tonetta S, Zaffanella E. 2019. ARCH-COMP19 Category Report: Hybrid systems with piecewise constant dynamics. ARCH19. 6th International Workshop on Applied Verification of Continuous and Hybrid Systems. ARCH: International Workshop on Applied Verification on Continuous and Hybrid Systems, EPiC Series in Computing, vol. 61, 1–13.","ieee":"G. Frehse et al., “ARCH-COMP19 Category Report: Hybrid systems with piecewise constant dynamics,” in ARCH19. 6th International Workshop on Applied Verification of Continuous and Hybrid Systems, Montreal, Canada, 2019, vol. 61, pp. 1–13.","apa":"Frehse, G., Abate, A., Adzkiya, D., Becchi, A., Bu, L., Cimatti, A., … Zaffanella, E. (2019). ARCH-COMP19 Category Report: Hybrid systems with piecewise constant dynamics. In G. Frehse & M. Althoff (Eds.), ARCH19. 6th International Workshop on Applied Verification of Continuous and Hybrid Systems (Vol. 61, pp. 1–13). Montreal, Canada: EasyChair. https://doi.org/10.29007/rjwn","ama":"Frehse G, Abate A, Adzkiya D, et al. ARCH-COMP19 Category Report: Hybrid systems with piecewise constant dynamics. In: Frehse G, Althoff M, eds. ARCH19. 6th International Workshop on Applied Verification of Continuous and Hybrid Systems. Vol 61. EasyChair; 2019:1-13. doi:10.29007/rjwn"},"day":"25","article_processing_charge":"No","has_accepted_license":"1","scopus_import":"1","date_updated":"2022-05-17T07:09:47Z","date_created":"2022-03-18T12:29:23Z","volume":61,"author":[{"last_name":"Frehse","first_name":"Goran","full_name":"Frehse, Goran"},{"first_name":"Alessandro","last_name":"Abate","full_name":"Abate, Alessandro"},{"full_name":"Adzkiya, Dieky","first_name":"Dieky","last_name":"Adzkiya"},{"full_name":"Becchi, Anna","first_name":"Anna","last_name":"Becchi"},{"last_name":"Bu","first_name":"Lei","full_name":"Bu, Lei"},{"last_name":"Cimatti","first_name":"Alessandro","full_name":"Cimatti, Alessandro"},{"full_name":"Giacobbe, Mirco","orcid":"0000-0001-8180-0904","id":"3444EA5E-F248-11E8-B48F-1D18A9856A87","last_name":"Giacobbe","first_name":"Mirco"},{"first_name":"Alberto","last_name":"Griggio","full_name":"Griggio, Alberto"},{"first_name":"Sergio","last_name":"Mover","full_name":"Mover, Sergio"},{"last_name":"Mufid","first_name":"Muhammad Syifa'ul","full_name":"Mufid, Muhammad Syifa'ul"},{"first_name":"Idriss","last_name":"Riouak","full_name":"Riouak, Idriss"},{"full_name":"Tonetta, Stefano","first_name":"Stefano","last_name":"Tonetta"},{"first_name":"Enea","last_name":"Zaffanella","full_name":"Zaffanella, Enea"}],"publication_status":"published","editor":[{"first_name":"Goran","last_name":"Frehse","full_name":"Frehse, Goran"},{"full_name":"Althoff, Matthias","first_name":"Matthias","last_name":"Althoff"}],"department":[{"_id":"ToHe"}],"publisher":"EasyChair","acknowledgement":"The authors gratefully acknowledge \fnancial support by the European Commission project\r\nUnCoVerCPS under grant number 643921. Lei Bu is supported by the National Natural Science\r\nFoundation of China (No.61572249).","year":"2019","file_date_updated":"2022-05-17T06:55:49Z","language":[{"iso":"eng"}],"conference":{"end_date":"2019-04-15","location":"Montreal, Canada","start_date":"2019-04-15","name":"ARCH: International Workshop on Applied Verification on Continuous and Hybrid Systems"},"doi":"10.29007/rjwn","quality_controlled":"1","oa":1,"month":"05","publication_identifier":{"issn":["2398-7340"]}},{"citation":{"mla":"Alur, Rajeev, et al. “Continuous-Time Models for System Design and Analysis.” Computing and Software Science, edited by Bernhard Steffen and Gerhard Woeginger, vol. 10000, Springer Nature, 2019, pp. 452–77, doi:10.1007/978-3-319-91908-9_22.","short":"R. Alur, M. Giacobbe, T.A. Henzinger, K.G. Larsen, M. Mikučionis, in:, B. Steffen, G. Woeginger (Eds.), Computing and Software Science, Springer Nature, 2019, pp. 452–477.","chicago":"Alur, Rajeev, Mirco Giacobbe, Thomas A Henzinger, Kim G. Larsen, and Marius Mikučionis. “Continuous-Time Models for System Design and Analysis.” In Computing and Software Science, edited by Bernhard Steffen and Gerhard Woeginger, 10000:452–77. LNCS. Springer Nature, 2019. https://doi.org/10.1007/978-3-319-91908-9_22.","ama":"Alur R, Giacobbe M, Henzinger TA, Larsen KG, Mikučionis M. Continuous-time models for system design and analysis. In: Steffen B, Woeginger G, eds. Computing and Software Science. Vol 10000. LNCS. Springer Nature; 2019:452-477. doi:10.1007/978-3-319-91908-9_22","ista":"Alur R, Giacobbe M, Henzinger TA, Larsen KG, Mikučionis M. 2019.Continuous-time models for system design and analysis. In: Computing and Software Science. Lecture Notes in Computer Science, vol. 10000, 452–477.","ieee":"R. Alur, M. Giacobbe, T. A. Henzinger, K. G. Larsen, and M. Mikučionis, “Continuous-time models for system design and analysis,” in Computing and Software Science, vol. 10000, B. Steffen and G. Woeginger, Eds. Springer Nature, 2019, pp. 452–477.","apa":"Alur, R., Giacobbe, M., Henzinger, T. A., Larsen, K. G., & Mikučionis, M. (2019). Continuous-time models for system design and analysis. In B. Steffen & G. Woeginger (Eds.), Computing and Software Science (Vol. 10000, pp. 452–477). Springer Nature. https://doi.org/10.1007/978-3-319-91908-9_22"},"publication":"Computing and Software Science","page":"452-477","date_published":"2019-10-05T00:00:00Z","scopus_import":"1","series_title":"LNCS","article_processing_charge":"No","day":"05","_id":"7453","user_id":"2DF688A6-F248-11E8-B48F-1D18A9856A87","intvolume":" 10000","status":"public","title":"Continuous-time models for system design and analysis","oa_version":"Published Version","type":"book_chapter","alternative_title":["Lecture Notes in Computer Science"],"abstract":[{"lang":"eng","text":"We illustrate the ingredients of the state-of-the-art of model-based approach for the formal design and verification of cyber-physical systems. To capture the interaction between a discrete controller and its continuously evolving environment, we use the formal models of timed and hybrid automata. We explain the steps of modeling and verification in the tools Uppaal and SpaceEx using a case study based on a dual-chamber implantable pacemaker monitoring a human heart. We show how to design a model as a composition of components, how to construct models at varying levels of detail, how to establish that one model is an abstraction of another, how to specify correctness requirements using temporal logic, and how to verify that a model satisfies a logical requirement."}],"oa":1,"main_file_link":[{"open_access":"1","url":"https://doi.org/10.1007/978-3-319-91908-9_22"}],"project":[{"grant_number":"S11402-N23","_id":"25F2ACDE-B435-11E9-9278-68D0E5697425","name":"Rigorous Systems Engineering","call_identifier":"FWF"},{"call_identifier":"FWF","name":"The Wittgenstein Prize","_id":"25F42A32-B435-11E9-9278-68D0E5697425","grant_number":"Z211"}],"quality_controlled":"1","doi":"10.1007/978-3-319-91908-9_22","language":[{"iso":"eng"}],"publication_identifier":{"eisbn":["9783319919089"],"issn":["1611-3349"],"isbn":["9783319919072"],"eissn":["0302-9743"]},"month":"10","year":"2019","acknowledgement":"This research was supported in part by the Austrian Science Fund (FWF) under grants S11402-N23(RiSE/SHiNE) and Z211-N23 (Wittgenstein Award). This research has received funding from the Sino-Danish Basic Research Centre, IDEA4CPS, funded by the Danish National Research Foundation and the National Science Foundation, China, the Innovation Fund Denmark centre DiCyPS, as well as the ERC Advanced Grant LASSO.","department":[{"_id":"ToHe"}],"editor":[{"last_name":"Steffen","first_name":"Bernhard","full_name":"Steffen, Bernhard"},{"last_name":"Woeginger","first_name":"Gerhard","full_name":"Woeginger, Gerhard"}],"publisher":"Springer Nature","publication_status":"published","author":[{"full_name":"Alur, Rajeev","first_name":"Rajeev","last_name":"Alur"},{"orcid":"0000-0001-8180-0904","id":"3444EA5E-F248-11E8-B48F-1D18A9856A87","last_name":"Giacobbe","first_name":"Mirco","full_name":"Giacobbe, Mirco"},{"full_name":"Henzinger, Thomas A","id":"40876CD8-F248-11E8-B48F-1D18A9856A87","orcid":"0000−0002−2985−7724","first_name":"Thomas A","last_name":"Henzinger"},{"full_name":"Larsen, Kim G.","last_name":"Larsen","first_name":"Kim G."},{"full_name":"Mikučionis, Marius","first_name":"Marius","last_name":"Mikučionis"}],"volume":10000,"date_created":"2020-02-05T10:51:44Z","date_updated":"2022-09-06T08:25:52Z"},{"date_published":"2019-09-30T00:00:00Z","page":"132","citation":{"chicago":"Giacobbe, Mirco. “Automatic Time-Unbounded Reachability Analysis of Hybrid Systems.” Institute of Science and Technology Austria, 2019. https://doi.org/10.15479/AT:ISTA:6894.","mla":"Giacobbe, Mirco. Automatic Time-Unbounded Reachability Analysis of Hybrid Systems. Institute of Science and Technology Austria, 2019, doi:10.15479/AT:ISTA:6894.","short":"M. Giacobbe, Automatic Time-Unbounded Reachability Analysis of Hybrid Systems, Institute of Science and Technology Austria, 2019.","ista":"Giacobbe M. 2019. Automatic time-unbounded reachability analysis of hybrid systems. Institute of Science and Technology Austria.","ieee":"M. Giacobbe, “Automatic time-unbounded reachability analysis of hybrid systems,” Institute of Science and Technology Austria, 2019.","apa":"Giacobbe, M. (2019). Automatic time-unbounded reachability analysis of hybrid systems. Institute of Science and Technology Austria. https://doi.org/10.15479/AT:ISTA:6894","ama":"Giacobbe M. Automatic time-unbounded reachability analysis of hybrid systems. 2019. doi:10.15479/AT:ISTA:6894"},"has_accepted_license":"1","article_processing_charge":"No","day":"30","file":[{"file_id":"6916","relation":"main_file","checksum":"773beaf4a85dc2acc2c12b578fbe1965","date_created":"2019-09-27T14:15:05Z","date_updated":"2020-07-14T12:47:43Z","access_level":"open_access","file_name":"giacobbe_thesis.pdf","creator":"mgiacobbe","file_size":4100685,"content_type":"application/pdf"},{"creator":"mgiacobbe","content_type":"application/gzip","file_size":7959732,"file_name":"giacobbe_thesis_src.tar.gz","access_level":"closed","date_created":"2019-09-27T14:22:04Z","date_updated":"2020-07-14T12:47:43Z","checksum":"97f1c3da71feefd27e6e625d32b4c75b","file_id":"6917","relation":"source_file"}],"oa_version":"Published Version","ddc":["000"],"title":"Automatic time-unbounded reachability analysis of hybrid systems","status":"public","user_id":"c635000d-4b10-11ee-a964-aac5a93f6ac1","_id":"6894","abstract":[{"text":"Hybrid automata combine finite automata and dynamical systems, and model the interaction of digital with physical systems. Formal analysis that can guarantee the safety of all behaviors or rigorously witness failures, while unsolvable in general, has been tackled algorithmically using, e.g., abstraction, bounded model-checking, assisted theorem proving.\r\nNevertheless, very few methods have addressed the time-unbounded reachability analysis of hybrid automata and, for current sound and automatic tools, scalability remains critical. We develop methods for the polyhedral abstraction of hybrid automata, which construct coarse overapproximations and tightens them incrementally, in a CEGAR fashion. We use template polyhedra, i.e., polyhedra whose facets are normal to a given set of directions.\r\nWhile, previously, directions were given by the user, we introduce (1) the first method\r\nfor computing template directions from spurious counterexamples, so as to generalize and\r\neliminate them. The method applies naturally to convex hybrid automata, i.e., hybrid\r\nautomata with (possibly non-linear) convex constraints on derivatives only, while for linear\r\nODE requires further abstraction. Specifically, we introduce (2) the conic abstractions,\r\nwhich, partitioning the state space into appropriate (possibly non-uniform) cones, divide\r\ncurvy trajectories into relatively straight sections, suitable for polyhedral abstractions.\r\nFinally, we introduce (3) space-time interpolation, which, combining interval arithmetic\r\nand template refinement, computes appropriate (possibly non-uniform) time partitioning\r\nand template directions along spurious trajectories, so as to eliminate them.\r\nWe obtain sound and automatic methods for the reachability analysis over dense\r\nand unbounded time of convex hybrid automata and hybrid automata with linear ODE.\r\nWe build prototype tools and compare—favorably—our methods against the respective\r\nstate-of-the-art tools, on several benchmarks.","lang":"eng"}],"alternative_title":["ISTA Thesis"],"type":"dissertation","language":[{"iso":"eng"}],"degree_awarded":"PhD","supervisor":[{"full_name":"Henzinger, Thomas A","first_name":"Thomas A","last_name":"Henzinger","id":"40876CD8-F248-11E8-B48F-1D18A9856A87","orcid":"0000−0002−2985−7724"}],"doi":"10.15479/AT:ISTA:6894","oa":1,"tmp":{"name":"Creative Commons Attribution 4.0 International Public License (CC-BY 4.0)","legal_code_url":"https://creativecommons.org/licenses/by/4.0/legalcode","short":"CC BY (4.0)","image":"/images/cc_by.png"},"publication_identifier":{"eissn":["2663-337X"]},"month":"09","date_created":"2019-09-22T14:08:44Z","date_updated":"2023-09-19T09:30:43Z","related_material":{"record":[{"status":"public","relation":"part_of_dissertation","id":"631"},{"status":"public","relation":"part_of_dissertation","id":"647"},{"relation":"part_of_dissertation","status":"public","id":"140"}]},"author":[{"full_name":"Giacobbe, Mirco","last_name":"Giacobbe","first_name":"Mirco","orcid":"0000-0001-8180-0904","id":"3444EA5E-F248-11E8-B48F-1D18A9856A87"}],"publisher":"Institute of Science and Technology Austria","department":[{"_id":"ToHe"}],"publication_status":"published","year":"2019","file_date_updated":"2020-07-14T12:47:43Z"},{"alternative_title":["LNCS"],"type":"conference","abstract":[{"text":"Reachability analysis is difficult for hybrid automata with affine differential equations, because the reach set needs to be approximated. Promising abstraction techniques usually employ interval methods or template polyhedra. Interval methods account for dense time and guarantee soundness, and there are interval-based tools that overapproximate affine flowpipes. But interval methods impose bounded and rigid shapes, which make refinement expensive and fixpoint detection difficult. Template polyhedra, on the other hand, can be adapted flexibly and can be unbounded, but sound template refinement for unbounded reachability analysis has been implemented only for systems with piecewise constant dynamics. We capitalize on the advantages of both techniques, combining interval arithmetic and template polyhedra, using the former to abstract time and the latter to abstract space. During a CEGAR loop, whenever a spurious error trajectory is found, we compute additional space constraints and split time intervals, and use these space-time interpolants to eliminate the counterexample. Space-time interpolation offers a lazy, flexible framework for increasing precision while guaranteeing soundness, both for error avoidance and fixpoint detection. To the best of out knowledge, this is the first abstraction refinement scheme for the reachability analysis over unbounded and dense time of affine hybrid systems, which is both sound and automatic. We demonstrate the effectiveness of our algorithm with several benchmark examples, which cannot be handled by other tools.","lang":"eng"}],"intvolume":" 10981","status":"public","title":"Space-time interpolants","ddc":["005"],"user_id":"c635000d-4b10-11ee-a964-aac5a93f6ac1","_id":"140","file":[{"file_id":"5310","relation":"main_file","checksum":"6dca832f575d6b3f0ea9dff56f579142","date_created":"2018-12-12T10:17:53Z","date_updated":"2020-07-14T12:44:50Z","access_level":"open_access","file_name":"IST-2018-1010-v1+1_space-time_interpolants.pdf","creator":"system","content_type":"application/pdf","file_size":563710}],"oa_version":"Published Version","pubrep_id":"1010","scopus_import":"1","article_processing_charge":"No","has_accepted_license":"1","day":"18","page":"468 - 486","citation":{"chicago":"Frehse, Goran, Mirco Giacobbe, and Thomas A Henzinger. “Space-Time Interpolants,” 10981:468–86. Springer, 2018. https://doi.org/10.1007/978-3-319-96145-3_25.","mla":"Frehse, Goran, et al. Space-Time Interpolants. Vol. 10981, Springer, 2018, pp. 468–86, doi:10.1007/978-3-319-96145-3_25.","short":"G. Frehse, M. Giacobbe, T.A. Henzinger, in:, Springer, 2018, pp. 468–486.","ista":"Frehse G, Giacobbe M, Henzinger TA. 2018. Space-time interpolants. CAV: Computer Aided Verification, LNCS, vol. 10981, 468–486.","ieee":"G. Frehse, M. Giacobbe, and T. A. Henzinger, “Space-time interpolants,” presented at the CAV: Computer Aided Verification, Oxford, United Kingdom, 2018, vol. 10981, pp. 468–486.","apa":"Frehse, G., Giacobbe, M., & Henzinger, T. A. (2018). Space-time interpolants (Vol. 10981, pp. 468–486). Presented at the CAV: Computer Aided Verification, Oxford, United Kingdom: Springer. https://doi.org/10.1007/978-3-319-96145-3_25","ama":"Frehse G, Giacobbe M, Henzinger TA. Space-time interpolants. In: Vol 10981. Springer; 2018:468-486. doi:10.1007/978-3-319-96145-3_25"},"date_published":"2018-07-18T00:00:00Z","publist_id":"7783","file_date_updated":"2020-07-14T12:44:50Z","department":[{"_id":"ToHe"}],"publisher":"Springer","publication_status":"published","year":"2018","volume":10981,"date_created":"2018-12-11T11:44:50Z","date_updated":"2023-09-19T09:30:43Z","related_material":{"record":[{"id":"6894","status":"public","relation":"dissertation_contains"}]},"author":[{"full_name":"Frehse, Goran","last_name":"Frehse","first_name":"Goran"},{"full_name":"Giacobbe, Mirco","id":"3444EA5E-F248-11E8-B48F-1D18A9856A87","orcid":"0000-0001-8180-0904","first_name":"Mirco","last_name":"Giacobbe"},{"last_name":"Henzinger","first_name":"Thomas A","orcid":"0000−0002−2985−7724","id":"40876CD8-F248-11E8-B48F-1D18A9856A87","full_name":"Henzinger, Thomas A"}],"publication_identifier":{"issn":["03029743"]},"month":"07","project":[{"_id":"25832EC2-B435-11E9-9278-68D0E5697425","grant_number":"S 11407_N23","call_identifier":"FWF","name":"Rigorous Systems Engineering"},{"_id":"25F5A88A-B435-11E9-9278-68D0E5697425","grant_number":"S11402-N23","call_identifier":"FWF","name":"Moderne Concurrency Paradigms"}],"quality_controlled":"1","isi":1,"oa":1,"tmp":{"name":"Creative Commons Attribution 4.0 International Public License (CC-BY 4.0)","legal_code_url":"https://creativecommons.org/licenses/by/4.0/legalcode","short":"CC BY (4.0)","image":"/images/cc_by.png"},"external_id":{"isi":["000491481600025"]},"language":[{"iso":"eng"}],"doi":"10.1007/978-3-319-96145-3_25","conference":{"name":"CAV: Computer Aided Verification","end_date":"2018-07-17","start_date":"2018-07-14","location":"Oxford, United Kingdom"}},{"abstract":[{"text":"Despite researchers’ efforts in the last couple of decades, reachability analysis is still a challenging problem even for linear hybrid systems. Among the existing approaches, the most practical ones are mainly based on bounded-time reachable set over-approximations. For the purpose of unbounded-time analysis, one important strategy is to abstract the original system and find an invariant for the abstraction. In this paper, we propose an approach to constructing a new kind of abstraction called conic abstraction for affine hybrid systems, and to computing reachable sets based on this abstraction. The essential feature of a conic abstraction is that it partitions the state space of a system into a set of convex polyhedral cones which is derived from a uniform conic partition of the derivative space. Such a set of polyhedral cones is able to cut all trajectories of the system into almost straight segments so that every segment of a reach pipe in a polyhedral cone tends to be straight as well, and hence can be over-approximated tightly by polyhedra using similar techniques as HyTech or PHAVer. In particular, for diagonalizable affine systems, our approach can guarantee to find an invariant for unbounded reachable sets, which is beyond the capability of bounded-time reachability analysis tools. We implemented the approach in a tool and experiments on benchmarks show that our approach is more powerful than SpaceEx and PHAVer in dealing with diagonalizable systems.","lang":"eng"}],"alternative_title":["LNCS"],"type":"conference","file":[{"file_id":"4956","relation":"main_file","date_created":"2018-12-12T10:12:38Z","date_updated":"2020-07-14T12:47:31Z","checksum":"faf546914ba29bcf9974ee36b6b16750","file_name":"IST-2017-831-v1+1_main.pdf","access_level":"open_access","creator":"system","file_size":3806864,"content_type":"application/pdf"}],"oa_version":"Submitted Version","pubrep_id":"831","ddc":["005"],"title":"Conic abstractions for hybrid systems","status":"public","_id":"647","user_id":"2DF688A6-F248-11E8-B48F-1D18A9856A87","day":"01","has_accepted_license":"1","scopus_import":1,"date_published":"2017-09-01T00:00:00Z","page":"116 - 132","citation":{"apa":"Bogomolov, S., Giacobbe, M., Henzinger, T. A., & Kong, H. (2017). Conic abstractions for hybrid systems (Vol. 10419, pp. 116–132). Presented at the FORMATS: Formal Modelling and Analysis of Timed Systems, Berlin, Germany: Springer. https://doi.org/10.1007/978-3-319-65765-3_7","ieee":"S. Bogomolov, M. Giacobbe, T. A. Henzinger, and H. Kong, “Conic abstractions for hybrid systems,” presented at the FORMATS: Formal Modelling and Analysis of Timed Systems, Berlin, Germany, 2017, vol. 10419, pp. 116–132.","ista":"Bogomolov S, Giacobbe M, Henzinger TA, Kong H. 2017. Conic abstractions for hybrid systems. FORMATS: Formal Modelling and Analysis of Timed Systems, LNCS, vol. 10419, 116–132.","ama":"Bogomolov S, Giacobbe M, Henzinger TA, Kong H. Conic abstractions for hybrid systems. In: Vol 10419. Springer; 2017:116-132. doi:10.1007/978-3-319-65765-3_7","chicago":"Bogomolov, Sergiy, Mirco Giacobbe, Thomas A Henzinger, and Hui Kong. “Conic Abstractions for Hybrid Systems,” 10419:116–32. Springer, 2017. https://doi.org/10.1007/978-3-319-65765-3_7.","short":"S. Bogomolov, M. Giacobbe, T.A. Henzinger, H. Kong, in:, Springer, 2017, pp. 116–132.","mla":"Bogomolov, Sergiy, et al. Conic Abstractions for Hybrid Systems. Vol. 10419, Springer, 2017, pp. 116–32, doi:10.1007/978-3-319-65765-3_7."},"file_date_updated":"2020-07-14T12:47:31Z","publist_id":"7129","date_updated":"2023-09-07T12:53:00Z","date_created":"2018-12-11T11:47:41Z","volume":"10419 ","author":[{"full_name":"Bogomolov, Sergiy","orcid":"0000-0002-0686-0365","id":"369D9A44-F248-11E8-B48F-1D18A9856A87","last_name":"Bogomolov","first_name":"Sergiy"},{"orcid":"0000-0001-8180-0904","id":"3444EA5E-F248-11E8-B48F-1D18A9856A87","last_name":"Giacobbe","first_name":"Mirco","full_name":"Giacobbe, Mirco"},{"last_name":"Henzinger","first_name":"Thomas A","orcid":"0000−0002−2985−7724","id":"40876CD8-F248-11E8-B48F-1D18A9856A87","full_name":"Henzinger, Thomas A"},{"last_name":"Kong","first_name":"Hui","orcid":"0000-0002-3066-6941","id":"3BDE25AA-F248-11E8-B48F-1D18A9856A87","full_name":"Kong, Hui"}],"related_material":{"record":[{"relation":"dissertation_contains","status":"public","id":"6894"}]},"publication_status":"published","publisher":"Springer","department":[{"_id":"ToHe"}],"year":"2017","month":"09","publication_identifier":{"isbn":["978-331965764-6"]},"language":[{"iso":"eng"}],"conference":{"end_date":"2017-09-07","location":"Berlin, Germany","start_date":"2017-09-05","name":"FORMATS: Formal Modelling and Analysis of Timed Systems"},"doi":"10.1007/978-3-319-65765-3_7","quality_controlled":"1","project":[{"grant_number":"S11402-N23","_id":"25F5A88A-B435-11E9-9278-68D0E5697425","call_identifier":"FWF","name":"Moderne Concurrency Paradigms"},{"_id":"25F42A32-B435-11E9-9278-68D0E5697425","grant_number":"Z211","call_identifier":"FWF","name":"The Wittgenstein Prize"}],"oa":1},{"scopus_import":1,"day":"31","has_accepted_license":"1","citation":{"ista":"Bogomolov S, Frehse G, Giacobbe M, Henzinger TA. 2017. Counterexample guided refinement of template polyhedra. TACAS: Tools and Algorithms for the Construction and Analysis of Systems, LNCS, vol. 10205, 589–606.","apa":"Bogomolov, S., Frehse, G., Giacobbe, M., & Henzinger, T. A. (2017). Counterexample guided refinement of template polyhedra (Vol. 10205, pp. 589–606). Presented at the TACAS: Tools and Algorithms for the Construction and Analysis of Systems, Uppsala, Sweden: Springer. https://doi.org/10.1007/978-3-662-54577-5_34","ieee":"S. Bogomolov, G. Frehse, M. Giacobbe, and T. A. Henzinger, “Counterexample guided refinement of template polyhedra,” presented at the TACAS: Tools and Algorithms for the Construction and Analysis of Systems, Uppsala, Sweden, 2017, vol. 10205, pp. 589–606.","ama":"Bogomolov S, Frehse G, Giacobbe M, Henzinger TA. Counterexample guided refinement of template polyhedra. In: Vol 10205. Springer; 2017:589-606. doi:10.1007/978-3-662-54577-5_34","chicago":"Bogomolov, Sergiy, Goran Frehse, Mirco Giacobbe, and Thomas A Henzinger. “Counterexample Guided Refinement of Template Polyhedra,” 10205:589–606. Springer, 2017. https://doi.org/10.1007/978-3-662-54577-5_34.","mla":"Bogomolov, Sergiy, et al. Counterexample Guided Refinement of Template Polyhedra. Vol. 10205, Springer, 2017, pp. 589–606, doi:10.1007/978-3-662-54577-5_34.","short":"S. Bogomolov, G. Frehse, M. Giacobbe, T.A. Henzinger, in:, Springer, 2017, pp. 589–606."},"page":"589 - 606","date_published":"2017-03-31T00:00:00Z","type":"conference","alternative_title":["LNCS"],"abstract":[{"lang":"eng","text":"Template polyhedra generalize intervals and octagons to polyhedra whose facets are orthogonal to a given set of arbitrary directions. They have been employed in the abstract interpretation of programs and, with particular success, in the reachability analysis of hybrid automata. While previously, the choice of directions has been left to the user or a heuristic, we present a method for the automatic discovery of directions that generalize and eliminate spurious counterexamples. We show that for the class of convex hybrid automata, i.e., hybrid automata with (possibly nonlinear) convex constraints on derivatives, such directions always exist and can be found using convex optimization. We embed our method inside a CEGAR loop, thus enabling the time-unbounded reachability analysis of an important and richer class of hybrid automata than was previously possible. We evaluate our method on several benchmarks, demonstrating also its superior efficiency for the special case of linear hybrid automata."}],"user_id":"2DF688A6-F248-11E8-B48F-1D18A9856A87","_id":"631","title":"Counterexample guided refinement of template polyhedra","status":"public","ddc":["000"],"intvolume":" 10205","pubrep_id":"966","file":[{"creator":"system","file_size":569863,"content_type":"application/pdf","access_level":"open_access","file_name":"IST-2017-741-v1+1_main.pdf","checksum":"f395d0d20102b89aeaad8b4ef4f18f4f","date_updated":"2020-07-14T12:47:27Z","date_created":"2018-12-12T10:11:41Z","file_id":"4897","relation":"main_file"},{"date_updated":"2020-07-14T12:47:27Z","date_created":"2018-12-12T10:11:42Z","checksum":"f416ee1ae4497b23ecdf28b1f18bb8df","file_id":"4898","relation":"main_file","creator":"system","content_type":"application/pdf","file_size":563276,"file_name":"IST-2018-741-v2+2_main.pdf","access_level":"open_access"}],"oa_version":"Submitted Version","month":"03","publication_identifier":{"isbn":["978-366254576-8"]},"oa":1,"quality_controlled":"1","project":[{"_id":"25F5A88A-B435-11E9-9278-68D0E5697425","grant_number":"S11402-N23","name":"Moderne Concurrency Paradigms","call_identifier":"FWF"},{"name":"The Wittgenstein Prize","call_identifier":"FWF","grant_number":"Z211","_id":"25F42A32-B435-11E9-9278-68D0E5697425"}],"conference":{"name":"TACAS: Tools and Algorithms for the Construction and Analysis of Systems","end_date":"2017-04-29","start_date":"2017-04-22","location":"Uppsala, Sweden"},"doi":"10.1007/978-3-662-54577-5_34","language":[{"iso":"eng"}],"file_date_updated":"2020-07-14T12:47:27Z","publist_id":"7162","acknowledgement":"This research was supported in part by the Austrian Science Fund (FWF) under grants S11402-N23 (RiSE/SHiNE) and Z211-N23 (Wittgenstein Award), by the European Commission under grant 643921 (UnCoVerCPS), and by the ARC project DP140104219 (Robust AI Planning for Hybrid Systems).","year":"2017","publication_status":"published","department":[{"_id":"ToHe"}],"publisher":"Springer","author":[{"orcid":"0000-0002-0686-0365","id":"369D9A44-F248-11E8-B48F-1D18A9856A87","last_name":"Bogomolov","first_name":"Sergiy","full_name":"Bogomolov, Sergiy"},{"full_name":"Frehse, Goran","last_name":"Frehse","first_name":"Goran"},{"last_name":"Giacobbe","first_name":"Mirco","orcid":"0000-0001-8180-0904","id":"3444EA5E-F248-11E8-B48F-1D18A9856A87","full_name":"Giacobbe, Mirco"},{"id":"40876CD8-F248-11E8-B48F-1D18A9856A87","orcid":"0000−0002−2985−7724","first_name":"Thomas A","last_name":"Henzinger","full_name":"Henzinger, Thomas A"}],"related_material":{"record":[{"status":"public","relation":"dissertation_contains","id":"6894"}]},"date_updated":"2023-09-07T12:53:00Z","date_created":"2018-12-11T11:47:36Z","volume":10205},{"abstract":[{"text":"The behaviour of gene regulatory networks (GRNs) is typically analysed using simulation-based statistical testing-like methods. In this paper, we demonstrate that we can replace this approach by a formal verification-like method that gives higher assurance and scalability. We focus on Wagner’s weighted GRN model with varying weights, which is used in evolutionary biology. In the model, weight parameters represent the gene interaction strength that may change due to genetic mutations. For a property of interest, we synthesise the constraints over the parameter space that represent the set of GRNs satisfying the property. We experimentally show that our parameter synthesis procedure computes the mutational robustness of GRNs—an important problem of interest in evolutionary biology—more efficiently than the classical simulation method. We specify the property in linear temporal logic. We employ symbolic bounded model checking and SMT solving to compute the space of GRNs that satisfy the property, which amounts to synthesizing a set of linear constraints on the weights.","lang":"eng"}],"issue":"8","type":"journal_article","pubrep_id":"649","oa_version":"Published Version","file":[{"file_id":"5841","relation":"main_file","date_created":"2019-01-17T15:57:29Z","date_updated":"2020-07-14T12:44:46Z","checksum":"4e661d9135d7f8c342e8e258dee76f3e","file_name":"2017_ActaInformatica_Giacobbe.pdf","access_level":"open_access","creator":"dernst","content_type":"application/pdf","file_size":755241}],"_id":"1351","user_id":"c635000d-4b10-11ee-a964-aac5a93f6ac1","title":"Model checking the evolution of gene regulatory networks","ddc":["006","576"],"status":"public","intvolume":" 54","day":"01","has_accepted_license":"1","article_processing_charge":"No","scopus_import":"1","date_published":"2017-12-01T00:00:00Z","publication":"Acta Informatica","citation":{"mla":"Giacobbe, Mirco, et al. “Model Checking the Evolution of Gene Regulatory Networks.” Acta Informatica, vol. 54, no. 8, Springer, 2017, pp. 765–87, doi:10.1007/s00236-016-0278-x.","short":"M. Giacobbe, C.C. Guet, A. Gupta, T.A. Henzinger, T. Paixao, T. Petrov, Acta Informatica 54 (2017) 765–787.","chicago":"Giacobbe, Mirco, Calin C Guet, Ashutosh Gupta, Thomas A Henzinger, Tiago Paixao, and Tatjana Petrov. “Model Checking the Evolution of Gene Regulatory Networks.” Acta Informatica. Springer, 2017. https://doi.org/10.1007/s00236-016-0278-x.","ama":"Giacobbe M, Guet CC, Gupta A, Henzinger TA, Paixao T, Petrov T. Model checking the evolution of gene regulatory networks. Acta Informatica. 2017;54(8):765-787. doi:10.1007/s00236-016-0278-x","ista":"Giacobbe M, Guet CC, Gupta A, Henzinger TA, Paixao T, Petrov T. 2017. Model checking the evolution of gene regulatory networks. Acta Informatica. 54(8), 765–787.","apa":"Giacobbe, M., Guet, C. C., Gupta, A., Henzinger, T. A., Paixao, T., & Petrov, T. (2017). Model checking the evolution of gene regulatory networks. Acta Informatica. Springer. https://doi.org/10.1007/s00236-016-0278-x","ieee":"M. Giacobbe, C. C. Guet, A. Gupta, T. A. Henzinger, T. Paixao, and T. Petrov, “Model checking the evolution of gene regulatory networks,” Acta Informatica, vol. 54, no. 8. Springer, pp. 765–787, 2017."},"page":"765 - 787","file_date_updated":"2020-07-14T12:44:46Z","ec_funded":1,"publist_id":"5898","author":[{"orcid":"0000-0001-8180-0904","id":"3444EA5E-F248-11E8-B48F-1D18A9856A87","last_name":"Giacobbe","first_name":"Mirco","full_name":"Giacobbe, Mirco"},{"last_name":"Guet","first_name":"Calin C","orcid":"0000-0001-6220-2052","id":"47F8433E-F248-11E8-B48F-1D18A9856A87","full_name":"Guet, Calin C"},{"first_name":"Ashutosh","last_name":"Gupta","id":"335E5684-F248-11E8-B48F-1D18A9856A87","full_name":"Gupta, Ashutosh"},{"full_name":"Henzinger, Thomas A","last_name":"Henzinger","first_name":"Thomas A","orcid":"0000−0002−2985−7724","id":"40876CD8-F248-11E8-B48F-1D18A9856A87"},{"orcid":"0000-0003-2361-3953","id":"2C5658E6-F248-11E8-B48F-1D18A9856A87","last_name":"Paixao","first_name":"Tiago","full_name":"Paixao, Tiago"},{"last_name":"Petrov","first_name":"Tatjana","orcid":"0000-0002-9041-0905","id":"3D5811FC-F248-11E8-B48F-1D18A9856A87","full_name":"Petrov, Tatjana"}],"related_material":{"record":[{"id":"1835","relation":"earlier_version","status":"public"}]},"date_created":"2018-12-11T11:51:32Z","date_updated":"2023-09-20T11:06:03Z","volume":54,"year":"2017","publication_status":"published","department":[{"_id":"ToHe"},{"_id":"CaGu"},{"_id":"NiBa"}],"publisher":"Springer","month":"12","publication_identifier":{"issn":["00015903"]},"doi":"10.1007/s00236-016-0278-x","language":[{"iso":"eng"}],"tmp":{"name":"Creative Commons Attribution 4.0 International Public License (CC-BY 4.0)","legal_code_url":"https://creativecommons.org/licenses/by/4.0/legalcode","short":"CC BY (4.0)","image":"/images/cc_by.png"},"external_id":{"isi":["000414343200003"]},"oa":1,"quality_controlled":"1","isi":1,"project":[{"name":"Quantitative Reactive Modeling","call_identifier":"FP7","_id":"25EE3708-B435-11E9-9278-68D0E5697425","grant_number":"267989"},{"_id":"25832EC2-B435-11E9-9278-68D0E5697425","grant_number":"S 11407_N23","call_identifier":"FWF","name":"Rigorous Systems Engineering"},{"_id":"25F42A32-B435-11E9-9278-68D0E5697425","grant_number":"Z211","name":"The Wittgenstein Prize","call_identifier":"FWF"},{"call_identifier":"FP7","name":"Speed of Adaptation in Population Genetics and Evolutionary Computation","grant_number":"618091","_id":"25B1EC9E-B435-11E9-9278-68D0E5697425"},{"call_identifier":"FP7","name":"International IST Postdoc Fellowship Programme","grant_number":"291734","_id":"25681D80-B435-11E9-9278-68D0E5697425"},{"grant_number":"250152","_id":"25B07788-B435-11E9-9278-68D0E5697425","call_identifier":"FP7","name":"Limits to selection in biology and in evolutionary computation"}]},{"publist_id":"5267","ec_funded":1,"publication_status":"published","publisher":"Springer","department":[{"_id":"ToHe"},{"_id":"CaGu"},{"_id":"NiBa"}],"year":"2015","acknowledgement":"SNSF Early Postdoc.Mobility Fellowship, the grant number P2EZP2 148797.\r\n","date_updated":"2023-09-20T11:06:03Z","date_created":"2018-12-11T11:54:16Z","volume":9035,"author":[{"last_name":"Giacobbe","first_name":"Mirco","orcid":"0000-0001-8180-0904","id":"3444EA5E-F248-11E8-B48F-1D18A9856A87","full_name":"Giacobbe, Mirco"},{"full_name":"Guet, Calin C","last_name":"Guet","first_name":"Calin C","orcid":"0000-0001-6220-2052","id":"47F8433E-F248-11E8-B48F-1D18A9856A87"},{"id":"335E5684-F248-11E8-B48F-1D18A9856A87","last_name":"Gupta","first_name":"Ashutosh","full_name":"Gupta, Ashutosh"},{"last_name":"Henzinger","first_name":"Thomas A","orcid":"0000−0002−2985−7724","id":"40876CD8-F248-11E8-B48F-1D18A9856A87","full_name":"Henzinger, Thomas A"},{"first_name":"Tiago","last_name":"Paixao","id":"2C5658E6-F248-11E8-B48F-1D18A9856A87","orcid":"0000-0003-2361-3953","full_name":"Paixao, Tiago"},{"full_name":"Petrov, Tatjana","orcid":"0000-0002-9041-0905","id":"3D5811FC-F248-11E8-B48F-1D18A9856A87","last_name":"Petrov","first_name":"Tatjana"}],"related_material":{"record":[{"id":"1351","status":"public","relation":"later_version"}]},"month":"04","quality_controlled":"1","project":[{"grant_number":"267989","_id":"25EE3708-B435-11E9-9278-68D0E5697425","name":"Quantitative Reactive Modeling","call_identifier":"FP7"},{"grant_number":"S 11407_N23","_id":"25832EC2-B435-11E9-9278-68D0E5697425","name":"Rigorous Systems Engineering","call_identifier":"FWF"},{"name":"The Wittgenstein Prize","call_identifier":"FWF","grant_number":"Z211","_id":"25F42A32-B435-11E9-9278-68D0E5697425"},{"grant_number":"618091","_id":"25B1EC9E-B435-11E9-9278-68D0E5697425","name":"Speed of Adaptation in Population Genetics and Evolutionary Computation","call_identifier":"FP7"},{"call_identifier":"FP7","name":"Limits to selection in biology and in evolutionary computation","_id":"25B07788-B435-11E9-9278-68D0E5697425","grant_number":"250152"},{"_id":"25681D80-B435-11E9-9278-68D0E5697425","grant_number":"291734","name":"International IST Postdoc Fellowship Programme","call_identifier":"FP7"}],"main_file_link":[{"url":"http://arxiv.org/abs/1410.7704","open_access":"1"}],"oa":1,"language":[{"iso":"eng"}],"conference":{"end_date":"2015-04-18","start_date":"2015-04-11","location":"London, United Kingdom","name":"TACAS: Tools and Algorithms for the Construction and Analysis of Systems"},"doi":"10.1007/978-3-662-46681-0_47","alternative_title":["LNCS"],"type":"conference","abstract":[{"lang":"eng","text":"The behaviour of gene regulatory networks (GRNs) is typically analysed using simulation-based statistical testing-like methods. In this paper, we demonstrate that we can replace this approach by a formal verification-like method that gives higher assurance and scalability. We focus on Wagner’s weighted GRN model with varying weights, which is used in evolutionary biology. In the model, weight parameters represent the gene interaction strength that may change due to genetic mutations. For a property of interest, we synthesise the constraints over the parameter space that represent the set of GRNs satisfying the property. We experimentally show that our parameter synthesis procedure computes the mutational robustness of GRNs –an important problem of interest in evolutionary biology– more efficiently than the classical simulation method. We specify the property in linear temporal logics. We employ symbolic bounded model checking and SMT solving to compute the space of GRNs that satisfy the property, which amounts to synthesizing a set of linear constraints on the weights."}],"title":"Model checking gene regulatory networks","status":"public","intvolume":" 9035","_id":"1835","user_id":"2DF688A6-F248-11E8-B48F-1D18A9856A87","oa_version":"Preprint","series_title":"Lecture Notes in Computer Science","scopus_import":1,"day":"01","page":"469 - 483","citation":{"ista":"Giacobbe M, Guet CC, Gupta A, Henzinger TA, Paixao T, Petrov T. 2015. Model checking gene regulatory networks. 9035, 469–483.","apa":"Giacobbe, M., Guet, C. C., Gupta, A., Henzinger, T. A., Paixao, T., & Petrov, T. (2015). Model checking gene regulatory networks. Presented at the TACAS: Tools and Algorithms for the Construction and Analysis of Systems, London, United Kingdom: Springer. https://doi.org/10.1007/978-3-662-46681-0_47","ieee":"M. Giacobbe, C. C. Guet, A. Gupta, T. A. Henzinger, T. Paixao, and T. Petrov, “Model checking gene regulatory networks,” vol. 9035. Springer, pp. 469–483, 2015.","ama":"Giacobbe M, Guet CC, Gupta A, Henzinger TA, Paixao T, Petrov T. Model checking gene regulatory networks. 2015;9035:469-483. doi:10.1007/978-3-662-46681-0_47","chicago":"Giacobbe, Mirco, Calin C Guet, Ashutosh Gupta, Thomas A Henzinger, Tiago Paixao, and Tatjana Petrov. “Model Checking Gene Regulatory Networks.” Lecture Notes in Computer Science. Springer, 2015. https://doi.org/10.1007/978-3-662-46681-0_47.","mla":"Giacobbe, Mirco, et al. Model Checking Gene Regulatory Networks. Vol. 9035, Springer, 2015, pp. 469–83, doi:10.1007/978-3-662-46681-0_47.","short":"M. Giacobbe, C.C. Guet, A. Gupta, T.A. Henzinger, T. Paixao, T. Petrov, 9035 (2015) 469–483."},"date_published":"2015-04-01T00:00:00Z"}]