[{"day":"01","publication":"Acta Informatica","has_accepted_license":"1","isi":1,"year":"2017","doi":"10.1007/s00236-016-0278-x","date_published":"2017-12-01T00:00:00Z","date_created":"2018-12-11T11:51:32Z","page":"765 - 787","quality_controlled":"1","publisher":"Springer","oa":1,"user_id":"c635000d-4b10-11ee-a964-aac5a93f6ac1","citation":{"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","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","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.","short":"M. Giacobbe, C.C. Guet, A. Gupta, T.A. Henzinger, T. Paixao, T. Petrov, Acta Informatica 54 (2017) 765–787.","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.","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.","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."},"title":"Model checking the evolution of gene regulatory networks","publist_id":"5898","author":[{"id":"3444EA5E-F248-11E8-B48F-1D18A9856A87","first_name":"Mirco","last_name":"Giacobbe","full_name":"Giacobbe, Mirco","orcid":"0000-0001-8180-0904"},{"first_name":"Calin C","id":"47F8433E-F248-11E8-B48F-1D18A9856A87","full_name":"Guet, Calin C","orcid":"0000-0001-6220-2052","last_name":"Guet"},{"id":"335E5684-F248-11E8-B48F-1D18A9856A87","first_name":"Ashutosh","last_name":"Gupta","full_name":"Gupta, Ashutosh"},{"last_name":"Henzinger","orcid":"0000−0002−2985−7724","full_name":"Henzinger, Thomas A","first_name":"Thomas A","id":"40876CD8-F248-11E8-B48F-1D18A9856A87"},{"id":"2C5658E6-F248-11E8-B48F-1D18A9856A87","first_name":"Tiago","full_name":"Paixao, Tiago","orcid":"0000-0003-2361-3953","last_name":"Paixao"},{"last_name":"Petrov","full_name":"Petrov, Tatjana","orcid":"0000-0002-9041-0905","first_name":"Tatjana","id":"3D5811FC-F248-11E8-B48F-1D18A9856A87"}],"external_id":{"isi":["000414343200003"]},"article_processing_charge":"No","project":[{"grant_number":"267989","name":"Quantitative Reactive Modeling","call_identifier":"FP7","_id":"25EE3708-B435-11E9-9278-68D0E5697425"},{"call_identifier":"FWF","_id":"25832EC2-B435-11E9-9278-68D0E5697425","grant_number":"S 11407_N23","name":"Rigorous Systems Engineering"},{"_id":"25F42A32-B435-11E9-9278-68D0E5697425","call_identifier":"FWF","grant_number":"Z211","name":"The Wittgenstein Prize"},{"_id":"25B1EC9E-B435-11E9-9278-68D0E5697425","call_identifier":"FP7","grant_number":"618091","name":"Speed of Adaptation in Population Genetics and Evolutionary Computation"},{"_id":"25681D80-B435-11E9-9278-68D0E5697425","call_identifier":"FP7","name":"International IST Postdoc Fellowship Programme","grant_number":"291734"},{"name":"Limits to selection in biology and in evolutionary computation","grant_number":"250152","call_identifier":"FP7","_id":"25B07788-B435-11E9-9278-68D0E5697425"}],"file":[{"creator":"dernst","date_updated":"2020-07-14T12:44:46Z","file_size":755241,"date_created":"2019-01-17T15:57:29Z","file_name":"2017_ActaInformatica_Giacobbe.pdf","access_level":"open_access","relation":"main_file","content_type":"application/pdf","checksum":"4e661d9135d7f8c342e8e258dee76f3e","file_id":"5841"}],"language":[{"iso":"eng"}],"publication_identifier":{"issn":["00015903"]},"publication_status":"published","volume":54,"related_material":{"record":[{"id":"1835","status":"public","relation":"earlier_version"}]},"issue":"8","ec_funded":1,"license":"https://creativecommons.org/licenses/by/4.0/","oa_version":"Published Version","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"}],"month":"12","intvolume":" 54","scopus_import":"1","ddc":["006","576"],"date_updated":"2023-09-20T11:06:03Z","department":[{"_id":"ToHe"},{"_id":"CaGu"},{"_id":"NiBa"}],"file_date_updated":"2020-07-14T12:44:46Z","_id":"1351","status":"public","pubrep_id":"649","type":"journal_article","tmp":{"legal_code_url":"https://creativecommons.org/licenses/by/4.0/legalcode","image":"/images/cc_by.png","name":"Creative Commons Attribution 4.0 International Public License (CC-BY 4.0)","short":"CC BY (4.0)"}},{"oa":1,"publisher":"Springer","quality_controlled":"1","acknowledgement":"We thank Andrey Kupriyanov for feedback on the manuscript,\r\nand Michael Tautschnig for help with preparing the experiments. This research was supported in part by the European Research Council (ERC) under grant 267989 (QUAREM) and by the Austrian Science Fund (FWF) under grants S11402-N23 (RiSE) and Z211-N23 (Wittgenstein Award).","date_created":"2018-12-11T11:50:50Z","doi":"10.1007/978-3-662-49122-5_16","date_published":"2016-01-01T00:00:00Z","page":"328 - 347","day":"01","year":"2016","project":[{"name":"Quantitative Reactive Modeling","grant_number":"267989","_id":"25EE3708-B435-11E9-9278-68D0E5697425","call_identifier":"FP7"},{"name":"The Wittgenstein Prize","grant_number":"Z211","_id":"25F42A32-B435-11E9-9278-68D0E5697425","call_identifier":"FWF"},{"_id":"25832EC2-B435-11E9-9278-68D0E5697425","call_identifier":"FWF","grant_number":"S 11407_N23","name":"Rigorous Systems Engineering"}],"title":"Abstraction-driven concolic testing","author":[{"full_name":"Daca, Przemyslaw","last_name":"Daca","first_name":"Przemyslaw","id":"49351290-F248-11E8-B48F-1D18A9856A87"},{"id":"335E5684-F248-11E8-B48F-1D18A9856A87","first_name":"Ashutosh","full_name":"Gupta, Ashutosh","last_name":"Gupta"},{"orcid":"0000−0002−2985−7724","full_name":"Henzinger, Thomas A","last_name":"Henzinger","id":"40876CD8-F248-11E8-B48F-1D18A9856A87","first_name":"Thomas A"}],"publist_id":"6104","user_id":"2DF688A6-F248-11E8-B48F-1D18A9856A87","citation":{"mla":"Daca, Przemyslaw, et al. Abstraction-Driven Concolic Testing. Vol. 9583, Springer, 2016, pp. 328–47, doi:10.1007/978-3-662-49122-5_16.","apa":"Daca, P., Gupta, A., & Henzinger, T. A. (2016). Abstraction-driven concolic testing (Vol. 9583, pp. 328–347). Presented at the VMCAI: Verification, Model Checking and Abstract Interpretation, St. Petersburg, FL, USA: Springer. https://doi.org/10.1007/978-3-662-49122-5_16","ama":"Daca P, Gupta A, Henzinger TA. Abstraction-driven concolic testing. In: Vol 9583. Springer; 2016:328-347. doi:10.1007/978-3-662-49122-5_16","short":"P. Daca, A. Gupta, T.A. Henzinger, in:, Springer, 2016, pp. 328–347.","ieee":"P. Daca, A. Gupta, and T. A. Henzinger, “Abstraction-driven concolic testing,” presented at the VMCAI: Verification, Model Checking and Abstract Interpretation, St. Petersburg, FL, USA, 2016, vol. 9583, pp. 328–347.","chicago":"Daca, Przemyslaw, Ashutosh Gupta, and Thomas A Henzinger. “Abstraction-Driven Concolic Testing,” 9583:328–47. Springer, 2016. https://doi.org/10.1007/978-3-662-49122-5_16.","ista":"Daca P, Gupta A, Henzinger TA. 2016. Abstraction-driven concolic testing. VMCAI: Verification, Model Checking and Abstract Interpretation, LNCS, vol. 9583, 328–347."},"intvolume":" 9583","month":"01","main_file_link":[{"open_access":"1","url":"https://arxiv.org/abs/1511.02615"}],"alternative_title":["LNCS"],"scopus_import":1,"oa_version":"Preprint","abstract":[{"text":"Concolic testing is a promising method for generating test suites for large programs. However, it suffers from the path-explosion problem and often fails to find tests that cover difficult-to-reach parts of programs. In contrast, model checkers based on counterexample-guided abstraction refinement explore programs exhaustively, while failing to scale on large programs with precision. In this paper, we present a novel method that iteratively combines concolic testing and model checking to find a test suite for a given coverage criterion. If concolic testing fails to cover some test goals, then the model checker refines its program abstraction to prove more paths infeasible, which reduces the search space for concolic testing. We have implemented our method on top of the concolictesting tool Crest and the model checker CpaChecker. We evaluated our tool on a collection of programs and a category of SvComp benchmarks. In our experiments, we observed an improvement in branch coverage compared to Crest from 48% to 63% in the best case, and from 66% to 71% on average.","lang":"eng"}],"ec_funded":1,"related_material":{"record":[{"id":"1155","status":"public","relation":"dissertation_contains"}]},"volume":9583,"language":[{"iso":"eng"}],"publication_status":"published","status":"public","conference":{"name":"VMCAI: Verification, Model Checking and Abstract Interpretation","end_date":"2016-01-19","location":"St. Petersburg, FL, USA","start_date":"2016-01-17"},"type":"conference","_id":"1230","department":[{"_id":"ToHe"}],"date_updated":"2023-09-07T11:58:33Z"},{"date_updated":"2021-01-12T06:53:20Z","citation":{"ista":"Gupta A, Henzinger TA. 2015. Guest editors’ introduction to special issue on computational methods in systems biology. ACM Transactions on Modeling and Computer Simulation. 25(2), 7.","chicago":"Gupta, Ashutosh, and Thomas A Henzinger. “Guest Editors’ Introduction to Special Issue on Computational Methods in Systems Biology.” ACM Transactions on Modeling and Computer Simulation. ACM, 2015. https://doi.org/10.1145/2745799.","short":"A. Gupta, T.A. Henzinger, ACM Transactions on Modeling and Computer Simulation 25 (2015).","ieee":"A. Gupta and T. A. Henzinger, “Guest editors’ introduction to special issue on computational methods in systems biology,” ACM Transactions on Modeling and Computer Simulation, vol. 25, no. 2. ACM, 2015.","apa":"Gupta, A., & Henzinger, T. A. (2015). Guest editors’ introduction to special issue on computational methods in systems biology. ACM Transactions on Modeling and Computer Simulation. ACM. https://doi.org/10.1145/2745799","ama":"Gupta A, Henzinger TA. Guest editors’ introduction to special issue on computational methods in systems biology. ACM Transactions on Modeling and Computer Simulation. 2015;25(2). doi:10.1145/2745799","mla":"Gupta, Ashutosh, and Thomas A. Henzinger. “Guest Editors’ Introduction to Special Issue on Computational Methods in Systems Biology.” ACM Transactions on Modeling and Computer Simulation, vol. 25, no. 2, 7, ACM, 2015, doi:10.1145/2745799."},"user_id":"2DF688A6-F248-11E8-B48F-1D18A9856A87","publist_id":"5302","author":[{"full_name":"Gupta, Ashutosh","last_name":"Gupta","first_name":"Ashutosh","id":"335E5684-F248-11E8-B48F-1D18A9856A87"},{"last_name":"Henzinger","orcid":"0000−0002−2985−7724","full_name":"Henzinger, Thomas A","id":"40876CD8-F248-11E8-B48F-1D18A9856A87","first_name":"Thomas A"}],"department":[{"_id":"ToHe"}],"title":"Guest editors' introduction to special issue on computational methods in systems biology","_id":"1808","article_number":"7","type":"journal_article","status":"public","year":"2015","publication_status":"published","language":[{"iso":"eng"}],"publication":"ACM Transactions on Modeling and Computer Simulation","day":"01","date_created":"2018-12-11T11:54:07Z","doi":"10.1145/2745799","date_published":"2015-05-01T00:00:00Z","volume":25,"issue":"2","oa_version":"None","publisher":"ACM","quality_controlled":"1","intvolume":" 25","month":"05"},{"publist_id":"5091","author":[{"first_name":"Ashutosh","id":"335E5684-F248-11E8-B48F-1D18A9856A87","full_name":"Gupta, Ashutosh","last_name":"Gupta"},{"id":"40876CD8-F248-11E8-B48F-1D18A9856A87","first_name":"Thomas A","last_name":"Henzinger","full_name":"Henzinger, Thomas A","orcid":"0000−0002−2985−7724"},{"id":"3B51CAC4-F248-11E8-B48F-1D18A9856A87","first_name":"Arjun","full_name":"Radhakrishna, Arjun","last_name":"Radhakrishna"},{"full_name":"Samanta, Roopsha","last_name":"Samanta","id":"3D2AAC08-F248-11E8-B48F-1D18A9856A87","first_name":"Roopsha"},{"first_name":"Thorsten","id":"3D6E8F2C-F248-11E8-B48F-1D18A9856A87","last_name":"Tarrach","orcid":"0000-0003-4409-8487","full_name":"Tarrach, Thorsten"}],"title":"Succinct representation of concurrent trace sets","citation":{"ista":"Gupta A, Henzinger TA, Radhakrishna A, Samanta R, Tarrach T. 2015. Succinct representation of concurrent trace sets. POPL: Principles of Programming Languages, 433–444.","chicago":"Gupta, Ashutosh, Thomas A Henzinger, Arjun Radhakrishna, Roopsha Samanta, and Thorsten Tarrach. “Succinct Representation of Concurrent Trace Sets,” 433–44. ACM, 2015. https://doi.org/10.1145/2676726.2677008.","ieee":"A. Gupta, T. A. Henzinger, A. Radhakrishna, R. Samanta, and T. Tarrach, “Succinct representation of concurrent trace sets,” presented at the POPL: Principles of Programming Languages, Mumbai, India, 2015, pp. 433–444.","short":"A. Gupta, T.A. Henzinger, A. Radhakrishna, R. Samanta, T. Tarrach, in:, ACM, 2015, pp. 433–444.","apa":"Gupta, A., Henzinger, T. A., Radhakrishna, A., Samanta, R., & Tarrach, T. (2015). Succinct representation of concurrent trace sets (pp. 433–444). Presented at the POPL: Principles of Programming Languages, Mumbai, India: ACM. https://doi.org/10.1145/2676726.2677008","ama":"Gupta A, Henzinger TA, Radhakrishna A, Samanta R, Tarrach T. Succinct representation of concurrent trace sets. In: ACM; 2015:433-444. doi:10.1145/2676726.2677008","mla":"Gupta, Ashutosh, et al. Succinct Representation of Concurrent Trace Sets. ACM, 2015, pp. 433–44, doi:10.1145/2676726.2677008."},"user_id":"2DF688A6-F248-11E8-B48F-1D18A9856A87","page":"433 - 444","doi":"10.1145/2676726.2677008","date_published":"2015-01-15T00:00:00Z","date_created":"2018-12-11T11:55:05Z","has_accepted_license":"1","year":"2015","day":"15","publisher":"ACM","quality_controlled":"1","oa":1,"file_date_updated":"2020-07-14T12:45:22Z","department":[{"_id":"ToHe"}],"date_updated":"2021-01-12T06:54:33Z","ddc":["005"],"type":"conference","conference":{"start_date":"2015-01-15","location":"Mumbai, India","end_date":"2015-01-17","name":"POPL: Principles of Programming Languages"},"status":"public","pubrep_id":"317","_id":"1992","publication_identifier":{"isbn":["978-1-4503-3300-9"]},"publication_status":"published","file":[{"date_created":"2018-12-12T10:17:56Z","file_name":"IST-2015-317-v1+1_author_version.pdf","date_updated":"2020-07-14T12:45:22Z","file_size":399462,"creator":"system","checksum":"f0d4395b600f410a191256ac0b73af32","file_id":"5314","content_type":"application/pdf","access_level":"open_access","relation":"main_file"}],"language":[{"iso":"eng"}],"scopus_import":1,"month":"01","abstract":[{"text":"We present a method and a tool for generating succinct representations of sets of concurrent traces. We focus on trace sets that contain all correct or all incorrect permutations of events from a given trace. We represent trace sets as HB-Formulas that are Boolean combinations of happens-before constraints between events. To generate a representation of incorrect interleavings, our method iteratively explores interleavings that violate the specification and gathers generalizations of the discovered interleavings into an HB-Formula; its complement yields a representation of correct interleavings.\r\n\r\nWe claim that our trace set representations can drive diverse verification, fault localization, repair, and synthesis techniques for concurrent programs. We demonstrate this by using our tool in three case studies involving synchronization synthesis, bug summarization, and abstraction refinement based verification. In each case study, our initial experimental results have been promising.\r\n\r\nIn the first case study, we present an algorithm for inferring missing synchronization from an HB-Formula representing correct interleavings of a given trace. The algorithm applies rules to rewrite specific patterns in the HB-Formula into locks, barriers, and wait-notify constructs. In the second case study, we use an HB-Formula representing incorrect interleavings for bug summarization. While the HB-Formula itself is a concise counterexample summary, we present additional inference rules to help identify specific concurrency bugs such as data races, define-use order violations, and two-stage access bugs. In the final case study, we present a novel predicate learning procedure that uses HB-Formulas representing abstract counterexamples to accelerate counterexample-guided abstraction refinement (CEGAR). In each iteration of the CEGAR loop, the procedure refines the abstraction to eliminate multiple spurious abstract counterexamples drawn from the HB-Formula.","lang":"eng"}],"oa_version":"Submitted Version"},{"language":[{"iso":"eng"}],"publication_status":"published","ec_funded":1,"related_material":{"record":[{"relation":"later_version","id":"1351","status":"public"}]},"volume":9035,"oa_version":"Preprint","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."}],"intvolume":" 9035","month":"04","main_file_link":[{"open_access":"1","url":"http://arxiv.org/abs/1410.7704"}],"scopus_import":1,"alternative_title":["LNCS"],"date_updated":"2023-09-20T11:06:03Z","department":[{"_id":"ToHe"},{"_id":"CaGu"},{"_id":"NiBa"}],"series_title":"Lecture Notes in Computer Science","_id":"1835","status":"public","conference":{"name":"TACAS: Tools and Algorithms for the Construction and Analysis of Systems","end_date":"2015-04-18","location":"London, United Kingdom","start_date":"2015-04-11"},"type":"conference","day":"01","year":"2015","date_created":"2018-12-11T11:54:16Z","doi":"10.1007/978-3-662-46681-0_47","date_published":"2015-04-01T00:00:00Z","page":"469 - 483","acknowledgement":"SNSF Early Postdoc.Mobility Fellowship, the grant number P2EZP2 148797.\r\n","oa":1,"publisher":"Springer","quality_controlled":"1","user_id":"2DF688A6-F248-11E8-B48F-1D18A9856A87","citation":{"ista":"Giacobbe M, Guet CC, Gupta A, Henzinger TA, Paixao T, Petrov T. 2015. Model checking gene regulatory networks. 9035, 469–483.","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.","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","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","short":"M. Giacobbe, C.C. Guet, A. Gupta, T.A. Henzinger, T. Paixao, T. Petrov, 9035 (2015) 469–483.","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.","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."},"title":"Model checking gene regulatory networks","author":[{"orcid":"0000-0001-8180-0904","full_name":"Giacobbe, Mirco","last_name":"Giacobbe","first_name":"Mirco","id":"3444EA5E-F248-11E8-B48F-1D18A9856A87"},{"orcid":"0000-0001-6220-2052","full_name":"Guet, Calin C","last_name":"Guet","first_name":"Calin C","id":"47F8433E-F248-11E8-B48F-1D18A9856A87"},{"id":"335E5684-F248-11E8-B48F-1D18A9856A87","first_name":"Ashutosh","full_name":"Gupta, Ashutosh","last_name":"Gupta"},{"last_name":"Henzinger","full_name":"Henzinger, Thomas A","orcid":"0000−0002−2985−7724","first_name":"Thomas A","id":"40876CD8-F248-11E8-B48F-1D18A9856A87"},{"id":"2C5658E6-F248-11E8-B48F-1D18A9856A87","first_name":"Tiago","last_name":"Paixao","full_name":"Paixao, Tiago","orcid":"0000-0003-2361-3953"},{"first_name":"Tatjana","id":"3D5811FC-F248-11E8-B48F-1D18A9856A87","full_name":"Petrov, Tatjana","orcid":"0000-0002-9041-0905","last_name":"Petrov"}],"publist_id":"5267","project":[{"_id":"25EE3708-B435-11E9-9278-68D0E5697425","call_identifier":"FP7","name":"Quantitative Reactive Modeling","grant_number":"267989"},{"grant_number":"S 11407_N23","name":"Rigorous Systems Engineering","_id":"25832EC2-B435-11E9-9278-68D0E5697425","call_identifier":"FWF"},{"grant_number":"Z211","name":"The Wittgenstein Prize","call_identifier":"FWF","_id":"25F42A32-B435-11E9-9278-68D0E5697425"},{"name":"Speed of Adaptation in Population Genetics and Evolutionary Computation","grant_number":"618091","call_identifier":"FP7","_id":"25B1EC9E-B435-11E9-9278-68D0E5697425"},{"call_identifier":"FP7","_id":"25B07788-B435-11E9-9278-68D0E5697425","grant_number":"250152","name":"Limits to selection in biology and in evolutionary computation"},{"call_identifier":"FP7","_id":"25681D80-B435-11E9-9278-68D0E5697425","name":"International IST Postdoc Fellowship Programme","grant_number":"291734"}]},{"publisher":"Open Publishing","quality_controlled":"1","alternative_title":["EPTCS"],"oa":1,"main_file_link":[{"url":"http://arxiv.org/abs/1303.7378v2","open_access":"1"}],"month":"12","intvolume":" 169","abstract":[{"lang":"eng","text":"In this paper we present INTERHORN, a solver for recursion-free Horn clauses. The main application domain of INTERHORN lies in solving interpolation problems arising in software verification. We show how a range of interpolation problems, including path, transition, nested, state/transition and well-founded interpolation can be handled directly by INTERHORN. By detailing these interpolation problems and their Horn clause representations, we hope to encourage the emergence of a common back-end interpolation interface useful for diverse verification tools."}],"oa_version":"Submitted Version","page":"31 - 38","date_published":"2014-12-02T00:00:00Z","volume":169,"doi":"10.4204/EPTCS.169.5","date_created":"2018-12-11T11:53:33Z","publication_status":"published","year":"2014","day":"02","language":[{"iso":"eng"}],"publication":"Electronic Proceedings in Theoretical Computer Science, EPTCS","type":"conference","conference":{"end_date":"2014-07-17","location":"Vienna, Austria","start_date":"2014-07-17","name":"HCVS: Horn Clauses for Verification and Synthesis"},"status":"public","_id":"1702","publist_id":"5435","author":[{"last_name":"Gupta","full_name":"Gupta, Ashutosh","first_name":"Ashutosh","id":"335E5684-F248-11E8-B48F-1D18A9856A87"},{"first_name":"Corneliu","last_name":"Popeea","full_name":"Popeea, Corneliu"},{"first_name":"Andrey","full_name":"Rybalchenko, Andrey","last_name":"Rybalchenko"}],"title":"Generalised interpolation by solving recursion free-horn clauses","department":[{"_id":"ToHe"}],"date_updated":"2021-01-12T06:52:38Z","citation":{"ista":"Gupta A, Popeea C, Rybalchenko A. 2014. Generalised interpolation by solving recursion free-horn clauses. Electronic Proceedings in Theoretical Computer Science, EPTCS. HCVS: Horn Clauses for Verification and Synthesis, EPTCS, vol. 169, 31–38.","chicago":"Gupta, Ashutosh, Corneliu Popeea, and Andrey Rybalchenko. “Generalised Interpolation by Solving Recursion Free-Horn Clauses.” In Electronic Proceedings in Theoretical Computer Science, EPTCS, 169:31–38. Open Publishing, 2014. https://doi.org/10.4204/EPTCS.169.5.","apa":"Gupta, A., Popeea, C., & Rybalchenko, A. (2014). Generalised interpolation by solving recursion free-horn clauses. In Electronic Proceedings in Theoretical Computer Science, EPTCS (Vol. 169, pp. 31–38). Vienna, Austria: Open Publishing. https://doi.org/10.4204/EPTCS.169.5","ama":"Gupta A, Popeea C, Rybalchenko A. Generalised interpolation by solving recursion free-horn clauses. In: Electronic Proceedings in Theoretical Computer Science, EPTCS. Vol 169. Open Publishing; 2014:31-38. doi:10.4204/EPTCS.169.5","short":"A. Gupta, C. Popeea, A. Rybalchenko, in:, Electronic Proceedings in Theoretical Computer Science, EPTCS, Open Publishing, 2014, pp. 31–38.","ieee":"A. Gupta, C. Popeea, and A. Rybalchenko, “Generalised interpolation by solving recursion free-horn clauses,” in Electronic Proceedings in Theoretical Computer Science, EPTCS, Vienna, Austria, 2014, vol. 169, pp. 31–38.","mla":"Gupta, Ashutosh, et al. “Generalised Interpolation by Solving Recursion Free-Horn Clauses.” Electronic Proceedings in Theoretical Computer Science, EPTCS, vol. 169, Open Publishing, 2014, pp. 31–38, doi:10.4204/EPTCS.169.5."},"user_id":"4435EBFC-F248-11E8-B48F-1D18A9856A87"},{"project":[{"name":"Quantitative Reactive Modeling","grant_number":"267989","_id":"25EE3708-B435-11E9-9278-68D0E5697425","call_identifier":"FP7"},{"call_identifier":"FWF","_id":"25863FF4-B435-11E9-9278-68D0E5697425","name":"Game Theory","grant_number":"S11407"}],"publist_id":"5228","author":[{"full_name":"Hofferek, Georg","last_name":"Hofferek","first_name":"Georg"},{"first_name":"Ashutosh","id":"335E5684-F248-11E8-B48F-1D18A9856A87","last_name":"Gupta","full_name":"Gupta, Ashutosh"}],"title":"Suraq - a controller synthesis tool using uninterpreted functions","editor":[{"first_name":"Eran","full_name":"Yahav, Eran","last_name":"Yahav"}],"citation":{"chicago":"Hofferek, Georg, and Ashutosh Gupta. “Suraq - a Controller Synthesis Tool Using Uninterpreted Functions.” In HVC 2014, edited by Eran Yahav, 8855:68–74. Springer, 2014. https://doi.org/10.1007/978-3-319-13338-6_6.","ista":"Hofferek G, Gupta A. 2014. Suraq - a controller synthesis tool using uninterpreted functions. HVC 2014. HVC: Haifa Verification Conference, LNCS, vol. 8855, 68–74.","mla":"Hofferek, Georg, and Ashutosh Gupta. “Suraq - a Controller Synthesis Tool Using Uninterpreted Functions.” HVC 2014, edited by Eran Yahav, vol. 8855, Springer, 2014, pp. 68–74, doi:10.1007/978-3-319-13338-6_6.","short":"G. Hofferek, A. Gupta, in:, E. Yahav (Ed.), HVC 2014, Springer, 2014, pp. 68–74.","ieee":"G. Hofferek and A. Gupta, “Suraq - a controller synthesis tool using uninterpreted functions,” in HVC 2014, Haifa, Israel, 2014, vol. 8855, pp. 68–74.","apa":"Hofferek, G., & Gupta, A. (2014). Suraq - a controller synthesis tool using uninterpreted functions. In E. Yahav (Ed.), HVC 2014 (Vol. 8855, pp. 68–74). Haifa, Israel: Springer. https://doi.org/10.1007/978-3-319-13338-6_6","ama":"Hofferek G, Gupta A. Suraq - a controller synthesis tool using uninterpreted functions. In: Yahav E, ed. HVC 2014. Vol 8855. Springer; 2014:68-74. doi:10.1007/978-3-319-13338-6_6"},"user_id":"4435EBFC-F248-11E8-B48F-1D18A9856A87","quality_controlled":"1","publisher":"Springer","acknowledgement":"The work presented in this paper was supported in part by the European Research Council (ERC) under grant agreement QUAINT (I774-N23)","page":"68 - 74","date_created":"2018-12-11T11:54:27Z","date_published":"2014-01-01T00:00:00Z","doi":"10.1007/978-3-319-13338-6_6","year":"2014","publication":"HVC 2014","day":"01","conference":{"name":"HVC: Haifa Verification Conference","start_date":"2014-11-18","location":"Haifa, Israel","end_date":"2014-11-20"},"type":"conference","status":"public","_id":"1869","department":[{"_id":"ToHe"}],"date_updated":"2021-01-12T06:53:44Z","alternative_title":["LNCS"],"intvolume":" 8855","month":"01","abstract":[{"text":"Boolean controllers for systems with complex datapaths are often very difficult to implement correctly, in particular when concurrency is involved. Yet, in many instances it is easy to formally specify correctness. For example, the specification for the controller of a pipelined processor only has to state that the pipelined processor gives the same results as a non-pipelined reference design. This makes such controllers a good target for automated synthesis. However, an efficient abstraction for the complex datapath elements is needed, as a bit-precise description is often infeasible. We present Suraq, the first controller synthesis tool which uses uninterpreted functions for the abstraction. Quantified firstorder formulas (with specific quantifier structure) serve as the specification language from which Suraq synthesizes Boolean controllers. Suraq transforms the specification into an unsatisfiable SMT formula, and uses Craig interpolation to compute its results. Using Suraq, we were able to synthesize a controller (consisting of two Boolean signals) for a five-stage pipelined DLX processor in roughly one hour and 15 minutes.","lang":"eng"}],"oa_version":"None","ec_funded":1,"volume":8855,"publication_status":"published","language":[{"iso":"eng"}]},{"citation":{"ista":"Gupta A, Kovács L, Kragl B, Voronkov A. 2014. Extensional crisis and proving identity. ATVA 2014. ATVA: Automated Technology for Verification and Analysis, LNCS, vol. 8837, 185–200.","chicago":"Gupta, Ashutosh, Laura Kovács, Bernhard Kragl, and Andrei Voronkov. “Extensional Crisis and Proving Identity.” In ATVA 2014, edited by Franck Cassez and Jean-François Raskin, 8837:185–200. Springer, 2014. https://doi.org/10.1007/978-3-319-11936-6_14.","apa":"Gupta, A., Kovács, L., Kragl, B., & Voronkov, A. (2014). Extensional crisis and proving identity. In F. Cassez & J.-F. Raskin (Eds.), ATVA 2014 (Vol. 8837, pp. 185–200). Sydney, Australia: Springer. https://doi.org/10.1007/978-3-319-11936-6_14","ama":"Gupta A, Kovács L, Kragl B, Voronkov A. Extensional crisis and proving identity. In: Cassez F, Raskin J-F, eds. ATVA 2014. Vol 8837. Springer; 2014:185-200. doi:10.1007/978-3-319-11936-6_14","ieee":"A. Gupta, L. Kovács, B. Kragl, and A. Voronkov, “Extensional crisis and proving identity,” in ATVA 2014, Sydney, Australia, 2014, vol. 8837, pp. 185–200.","short":"A. Gupta, L. Kovács, B. Kragl, A. Voronkov, in:, F. Cassez, J.-F. Raskin (Eds.), ATVA 2014, Springer, 2014, pp. 185–200.","mla":"Gupta, Ashutosh, et al. “Extensional Crisis and Proving Identity.” ATVA 2014, edited by Franck Cassez and Jean-François Raskin, vol. 8837, Springer, 2014, pp. 185–200, doi:10.1007/978-3-319-11936-6_14."},"user_id":"4435EBFC-F248-11E8-B48F-1D18A9856A87","publist_id":"5226","author":[{"id":"335E5684-F248-11E8-B48F-1D18A9856A87","first_name":"Ashutosh","full_name":"Gupta, Ashutosh","last_name":"Gupta"},{"first_name":"Laura","last_name":"Kovács","full_name":"Kovács, Laura"},{"first_name":"Bernhard","id":"320FC952-F248-11E8-B48F-1D18A9856A87","last_name":"Kragl","orcid":"0000-0001-7745-9117","full_name":"Kragl, Bernhard"},{"full_name":"Voronkov, Andrei","last_name":"Voronkov","first_name":"Andrei"}],"editor":[{"first_name":"Franck","last_name":"Cassez","full_name":"Cassez, Franck"},{"full_name":"Raskin, Jean-François","last_name":"Raskin","first_name":"Jean-François"}],"title":"Extensional crisis and proving identity","project":[{"_id":"25EE3708-B435-11E9-9278-68D0E5697425","call_identifier":"FP7","name":"Quantitative Reactive Modeling","grant_number":"267989"},{"grant_number":"S11402-N23","name":"Moderne Concurrency Paradigms","_id":"25F5A88A-B435-11E9-9278-68D0E5697425","call_identifier":"FWF"}],"has_accepted_license":"1","year":"2014","day":"01","publication":"ATVA 2014","page":"185 - 200","doi":"10.1007/978-3-319-11936-6_14","date_published":"2014-01-01T00:00:00Z","date_created":"2018-12-11T11:54:28Z","acknowledgement":"This research was supported in part by the Austrian National Research Network RiSE (S11410-N23).","publisher":"Springer","quality_controlled":"1","oa":1,"date_updated":"2021-01-12T06:53:45Z","ddc":["000"],"file_date_updated":"2020-07-14T12:45:19Z","department":[{"_id":"ToHe"}],"_id":"1872","type":"conference","conference":{"start_date":"2014-11-03","end_date":"2014-11-07","location":"Sydney, Australia","name":"ATVA: Automated Technology for Verification and Analysis"},"status":"public","pubrep_id":"641","publication_status":"published","file":[{"content_type":"application/pdf","access_level":"open_access","relation":"main_file","checksum":"af4bd3fc1f4c93075e4dc5cbf625fe7b","file_id":"4801","date_updated":"2020-07-14T12:45:19Z","file_size":244294,"creator":"system","date_created":"2018-12-12T10:10:15Z","file_name":"IST-2016-641-v1+1_atva2014.pdf"}],"language":[{"iso":"eng"}],"volume":8837,"ec_funded":1,"abstract":[{"lang":"eng","text":"Extensionality axioms are common when reasoning about data collections, such as arrays and functions in program analysis, or sets in mathematics. An extensionality axiom asserts that two collections are equal if they consist of the same elements at the same indices. Using extensionality is often required to show that two collections are equal. A typical example is the set theory theorem (∀x)(∀y)x∪y = y ∪x. Interestingly, while humans have no problem with proving such set identities using extensionality, they are very hard for superposition theorem provers because of the calculi they use. In this paper we show how addition of a new inference rule, called extensionality resolution, allows first-order theorem provers to easily solve problems no modern first-order theorem prover can solve. We illustrate this by running the VAMPIRE theorem prover with extensionality resolution on a number of set theory and array problems. Extensionality resolution helps VAMPIRE to solve problems from the TPTP library of first-order problems that were never solved before by any prover."}],"oa_version":"Submitted Version","alternative_title":["LNCS"],"scopus_import":1,"month":"01","intvolume":" 8837"},{"date_updated":"2021-01-12T06:50:19Z","department":[{"_id":"ToHe"}],"_id":"1385","status":"public","conference":{"end_date":"2013-10-23","location":"Portland, OR, United States","start_date":"2013-10-20","name":"FMCAD: Formal Methods in Computer-Aided Design"},"type":"conference","language":[{"iso":"eng"}],"publication_status":"published","ec_funded":1,"oa_version":"Preprint","abstract":[{"lang":"eng","text":"It is often difficult to correctly implement a Boolean controller for a complex system, especially when concurrency is involved. Yet, it may be easy to formally specify a controller. For instance, for a pipelined processor it suffices to state that the visible behavior of the pipelined system should be identical to a non-pipelined reference system (Burch-Dill paradigm). We present a novel procedure to efficiently synthesize multiple Boolean control signals from a specification given as a quantified first-order formula (with a specific quantifier structure). Our approach uses uninterpreted functions to abstract details of the design. We construct an unsatisfiable SMT formula from the given specification. Then, from just one proof of unsatisfiability, we use a variant of Craig interpolation to compute multiple coordinated interpolants that implement the Boolean control signals. Our method avoids iterative learning and back-substitution of the control functions. We applied our approach to synthesize a controller for a simple two-stage pipelined processor, and present first experimental results."}],"month":"12","main_file_link":[{"open_access":"1","url":"http://arxiv.org/abs/1308.4767"}],"user_id":"2DF688A6-F248-11E8-B48F-1D18A9856A87","citation":{"ista":"Hofferek G, Gupta A, Könighofer B, Jiang J, Bloem R. 2013. Synthesizing multiple boolean functions using interpolation on a single proof. 2013 Formal Methods in Computer-Aided Design. FMCAD: Formal Methods in Computer-Aided Design, 77–84.","chicago":"Hofferek, Georg, Ashutosh Gupta, Bettina Könighofer, Jie Jiang, and Roderick Bloem. “Synthesizing Multiple Boolean Functions Using Interpolation on a Single Proof.” In 2013 Formal Methods in Computer-Aided Design, 77–84. IEEE, 2013. https://doi.org/10.1109/FMCAD.2013.6679394.","ama":"Hofferek G, Gupta A, Könighofer B, Jiang J, Bloem R. Synthesizing multiple boolean functions using interpolation on a single proof. In: 2013 Formal Methods in Computer-Aided Design. IEEE; 2013:77-84. doi:10.1109/FMCAD.2013.6679394","apa":"Hofferek, G., Gupta, A., Könighofer, B., Jiang, J., & Bloem, R. (2013). Synthesizing multiple boolean functions using interpolation on a single proof. In 2013 Formal Methods in Computer-Aided Design (pp. 77–84). Portland, OR, United States: IEEE. https://doi.org/10.1109/FMCAD.2013.6679394","ieee":"G. Hofferek, A. Gupta, B. Könighofer, J. Jiang, and R. Bloem, “Synthesizing multiple boolean functions using interpolation on a single proof,” in 2013 Formal Methods in Computer-Aided Design, Portland, OR, United States, 2013, pp. 77–84.","short":"G. Hofferek, A. Gupta, B. Könighofer, J. Jiang, R. Bloem, in:, 2013 Formal Methods in Computer-Aided Design, IEEE, 2013, pp. 77–84.","mla":"Hofferek, Georg, et al. “Synthesizing Multiple Boolean Functions Using Interpolation on a Single Proof.” 2013 Formal Methods in Computer-Aided Design, IEEE, 2013, pp. 77–84, doi:10.1109/FMCAD.2013.6679394."},"title":"Synthesizing multiple boolean functions using interpolation on a single proof","external_id":{"arxiv":["1308.4767"]},"publist_id":"5825","author":[{"first_name":"Georg","last_name":"Hofferek","full_name":"Hofferek, Georg"},{"full_name":"Gupta, Ashutosh","last_name":"Gupta","first_name":"Ashutosh","id":"335E5684-F248-11E8-B48F-1D18A9856A87"},{"first_name":"Bettina","full_name":"Könighofer, Bettina","last_name":"Könighofer"},{"first_name":"Jie","last_name":"Jiang","full_name":"Jiang, Jie"},{"first_name":"Roderick","full_name":"Bloem, Roderick","last_name":"Bloem"}],"project":[{"call_identifier":"FWF","_id":"25832EC2-B435-11E9-9278-68D0E5697425","name":"Rigorous Systems Engineering","grant_number":"S 11407_N23"},{"grant_number":"267989","name":"Quantitative Reactive Modeling","call_identifier":"FP7","_id":"25EE3708-B435-11E9-9278-68D0E5697425"}],"publication":"2013 Formal Methods in Computer-Aided Design","day":"11","year":"2013","date_created":"2018-12-11T11:51:43Z","doi":"10.1109/FMCAD.2013.6679394","date_published":"2013-12-11T00:00:00Z","page":"77 - 84","acknowledgement":"This research was supported by the European Commission through project\r\nDIAMOND (FP7-2009-IST-4-248613), and QUAINT (I774-N23), ","oa":1,"publisher":"IEEE","quality_controlled":"1"},{"volume":8312,"file":[{"content_type":"application/pdf","access_level":"open_access","relation":"main_file","file_id":"7858","checksum":"9cebaafca032e6769d273f393305c705","date_updated":"2020-07-14T12:45:34Z","file_size":279206,"creator":"dernst","date_created":"2020-05-15T11:10:40Z","file_name":"2013_LPAR_Blanc.pdf"}],"language":[{"iso":"eng"}],"publication_status":"published","month":"01","intvolume":" 8312","scopus_import":1,"alternative_title":["LNCS"],"oa_version":"Submitted Version","abstract":[{"text":"We describe new extensions of the Vampire theorem prover for computing tree interpolants. These extensions generalize Craig interpolation in Vampire, and can also be used to derive sequence interpolants. We evaluated our implementation on a large number of examples over the theory of linear integer arithmetic and integer-indexed arrays, with and without quantifiers. When compared to other methods, our experiments show that some examples could only be solved by our implementation.","lang":"eng"}],"department":[{"_id":"ToHe"}],"file_date_updated":"2020-07-14T12:45:34Z","ddc":["000"],"date_updated":"2020-08-11T10:09:42Z","status":"public","type":"conference","conference":{"name":"LPAR: Logic for Programming, Artificial Intelligence, and Reasoning","start_date":"2013-12-14","location":"Stellenbosch, South Africa","end_date":"2013-12-19"},"series_title":"Lecture Notes in Computer Science","_id":"2237","doi":"10.1007/978-3-642-45221-5_13","date_published":"2013-01-14T00:00:00Z","date_created":"2018-12-11T11:56:29Z","page":"173 - 181","day":"14","has_accepted_license":"1","year":"2013","quality_controlled":"1","publisher":"Springer","oa":1,"title":"Tree interpolation in Vampire","author":[{"full_name":"Blanc, Régis","last_name":"Blanc","first_name":"Régis"},{"first_name":"Ashutosh","id":"335E5684-F248-11E8-B48F-1D18A9856A87","full_name":"Gupta, Ashutosh","last_name":"Gupta"},{"last_name":"Kovács","full_name":"Kovács, Laura","first_name":"Laura"},{"orcid":"0000-0001-7745-9117","full_name":"Kragl, Bernhard","last_name":"Kragl","id":"320FC952-F248-11E8-B48F-1D18A9856A87","first_name":"Bernhard"}],"publist_id":"4724","article_processing_charge":"No","user_id":"2DF688A6-F248-11E8-B48F-1D18A9856A87","citation":{"mla":"Blanc, Régis, et al. Tree Interpolation in Vampire. Vol. 8312, Springer, 2013, pp. 173–81, doi:10.1007/978-3-642-45221-5_13.","short":"R. Blanc, A. Gupta, L. Kovács, B. Kragl, 8312 (2013) 173–181.","ieee":"R. Blanc, A. Gupta, L. Kovács, and B. Kragl, “Tree interpolation in Vampire,” vol. 8312. Springer, pp. 173–181, 2013.","ama":"Blanc R, Gupta A, Kovács L, Kragl B. Tree interpolation in Vampire. 2013;8312:173-181. doi:10.1007/978-3-642-45221-5_13","apa":"Blanc, R., Gupta, A., Kovács, L., & Kragl, B. (2013). Tree interpolation in Vampire. Presented at the LPAR: Logic for Programming, Artificial Intelligence, and Reasoning, Stellenbosch, South Africa: Springer. https://doi.org/10.1007/978-3-642-45221-5_13","chicago":"Blanc, Régis, Ashutosh Gupta, Laura Kovács, and Bernhard Kragl. “Tree Interpolation in Vampire.” Lecture Notes in Computer Science. Springer, 2013. https://doi.org/10.1007/978-3-642-45221-5_13.","ista":"Blanc R, Gupta A, Kovács L, Kragl B. 2013. Tree interpolation in Vampire. 8312, 173–181."},"project":[{"grant_number":"S 11407_N23","name":"Rigorous Systems Engineering","_id":"25832EC2-B435-11E9-9278-68D0E5697425","call_identifier":"FWF"}]},{"citation":{"short":"A. Gupta, T.A. Henzinger, eds., Computational Methods in Systems Biology, Springer, 2013.","ieee":"A. Gupta and T. A. Henzinger, Eds., Computational Methods in Systems Biology, vol. 8130. Springer, 2013.","ama":"Gupta A, Henzinger TA, eds. Computational Methods in Systems Biology. Vol 8130. Springer; 2013. doi:10.1007/978-3-642-40708-6","apa":"Gupta, A., & Henzinger, T. A. (Eds.). (2013). Computational Methods in Systems Biology (Vol. 8130). Presented at the CMSB: Computational Methods in Systems Biology, Klosterneuburg, Austria: Springer. https://doi.org/10.1007/978-3-642-40708-6","mla":"Gupta, Ashutosh, and Thomas A. Henzinger, editors. Computational Methods in Systems Biology. Vol. 8130, Springer, 2013, doi:10.1007/978-3-642-40708-6.","ista":"Gupta A, Henzinger TA eds. 2013. Computational Methods in Systems Biology, Springer,p.","chicago":"Gupta, Ashutosh, and Thomas A Henzinger, eds. Computational Methods in Systems Biology. Vol. 8130. Springer, 2013. https://doi.org/10.1007/978-3-642-40708-6."},"date_updated":"2019-08-02T12:37:44Z","user_id":"2DF688A6-F248-11E8-B48F-1D18A9856A87","publist_id":"4643","title":"Computational Methods in Systems Biology","department":[{"_id":"ToHe"}],"editor":[{"id":"335E5684-F248-11E8-B48F-1D18A9856A87","first_name":"Ashutosh","last_name":"Gupta","full_name":"Gupta, Ashutosh"},{"first_name":"Thomas A","id":"40876CD8-F248-11E8-B48F-1D18A9856A87","last_name":"Henzinger","full_name":"Henzinger, Thomas A","orcid":"0000−0002−2985−7724"}],"_id":"2288","type":"conference_editor","conference":{"location":"Klosterneuburg, Austria","end_date":"2013-09-24","start_date":"2013-09-22","name":"CMSB: Computational Methods in Systems Biology"},"status":"public","publication_identifier":{"isbn":["978-3-642-40707-9"]},"year":"2013","publication_status":"published","day":"01","language":[{"iso":"eng"}],"volume":8130,"date_published":"2013-07-01T00:00:00Z","doi":"10.1007/978-3-642-40708-6","date_created":"2018-12-11T11:56:47Z","abstract":[{"text":"This book constitutes the proceedings of the 11th International Conference on Computational Methods in Systems Biology, CMSB 2013, held in Klosterneuburg, Austria, in September 2013. The 15 regular papers included in this volume were carefully reviewed and selected from 27 submissions. They deal with computational models for all levels, from molecular and cellular, to organs and entire organisms.","lang":"eng"}],"oa_version":"None","quality_controlled":"1","publisher":"Springer","alternative_title":["LNCS"],"month":"07","intvolume":" 8130"},{"project":[{"name":"Quantitative Reactive Modeling","grant_number":"267989","call_identifier":"FP7","_id":"25EE3708-B435-11E9-9278-68D0E5697425"},{"name":"Rigorous Systems Engineering","grant_number":"S 11407_N23","call_identifier":"FWF","_id":"25832EC2-B435-11E9-9278-68D0E5697425"}],"user_id":"c635000d-4b10-11ee-a964-aac5a93f6ac1","citation":{"mla":"Dragoi, Cezara, et al. “Automatic Linearizability Proofs of Concurrent Objects with Cooperating Updates.” Computer Aided Verification, vol. 8044, Springer Berlin Heidelberg, 2013, pp. 174–90, doi:10.1007/978-3-642-39799-8_11.","apa":"Dragoi, C., Gupta, A., & Henzinger, T. A. (2013). Automatic Linearizability Proofs of Concurrent Objects with Cooperating Updates. In Computer Aided Verification (Vol. 8044, pp. 174–190). Berlin, Heidelberg: Springer Berlin Heidelberg. https://doi.org/10.1007/978-3-642-39799-8_11","ama":"Dragoi C, Gupta A, Henzinger TA. Automatic Linearizability Proofs of Concurrent Objects with Cooperating Updates. In: Computer Aided Verification. Vol 8044. CAV. Berlin, Heidelberg: Springer Berlin Heidelberg; 2013:174-190. doi:10.1007/978-3-642-39799-8_11","ieee":"C. Dragoi, A. Gupta, and T. A. Henzinger, “Automatic Linearizability Proofs of Concurrent Objects with Cooperating Updates,” in Computer Aided Verification, vol. 8044, Berlin, Heidelberg: Springer Berlin Heidelberg, 2013, pp. 174–190.","short":"C. Dragoi, A. Gupta, T.A. Henzinger, in:, Computer Aided Verification, Springer Berlin Heidelberg, Berlin, Heidelberg, 2013, pp. 174–190.","chicago":"Dragoi, Cezara, Ashutosh Gupta, and Thomas A Henzinger. “Automatic Linearizability Proofs of Concurrent Objects with Cooperating Updates.” In Computer Aided Verification, 8044:174–90. CAV. Berlin, Heidelberg: Springer Berlin Heidelberg, 2013. https://doi.org/10.1007/978-3-642-39799-8_11.","ista":"Dragoi C, Gupta A, Henzinger TA. 2013.Automatic Linearizability Proofs of Concurrent Objects with Cooperating Updates. In: Computer Aided Verification. vol. 8044, 174–190."},"title":"Automatic Linearizability Proofs of Concurrent Objects with Cooperating Updates","article_processing_charge":"No","author":[{"last_name":"Dragoi","full_name":"Dragoi, Cezara","id":"2B2B5ED0-F248-11E8-B48F-1D18A9856A87","first_name":"Cezara"},{"full_name":"Gupta, Ashutosh","last_name":"Gupta","first_name":"Ashutosh","id":"335E5684-F248-11E8-B48F-1D18A9856A87"},{"orcid":"0000−0002−2985−7724","full_name":"Henzinger, Thomas A","last_name":"Henzinger","id":"40876CD8-F248-11E8-B48F-1D18A9856A87","first_name":"Thomas A"}],"oa":1,"publisher":"Springer Berlin Heidelberg","quality_controlled":"1","publication":"Computer Aided Verification","year":"2013","has_accepted_license":"1","date_created":"2018-12-18T13:10:21Z","date_published":"2013-01-01T00:00:00Z","doi":"10.1007/978-3-642-39799-8_11","page":"174-190","series_title":"CAV","_id":"5747","pubrep_id":"195","status":"public","conference":{"name":"CAV 2013","end_date":"2013-07-19","location":"Saint Petersburg, Russia","start_date":"2013-07-13"},"type":"book_chapter","ddc":["005"],"date_updated":"2023-09-05T14:16:07Z","file_date_updated":"2020-07-14T12:47:10Z","department":[{"_id":"ToHe"}],"oa_version":"None","intvolume":" 8044","place":"Berlin, Heidelberg","scopus_import":"1","language":[{"iso":"eng"}],"file":[{"date_updated":"2020-07-14T12:47:10Z","file_size":236480,"creator":"dernst","date_created":"2018-12-18T13:13:33Z","file_name":"2013_CAV_Dragoi.pdf","content_type":"application/pdf","access_level":"open_access","relation":"main_file","checksum":"a901cc6b71db08b61c0d4c0cbacc6287","file_id":"5748"}],"publication_status":"published","publication_identifier":{"eissn":["1611-3349"],"isbn":["9783642397981","9783642397998"],"issn":["0302-9743"]},"ec_funded":1,"volume":8044},{"abstract":[{"text":"Continuous-time Markov chains (CTMC) with their rich theory and efficient simulation algorithms have been successfully used in modeling stochastic processes in diverse areas such as computer science, physics, and biology. However, systems that comprise non-instantaneous events cannot be accurately and efficiently modeled with CTMCs. In this paper we define delayed CTMCs, an extension of CTMCs that allows for the specification of a lower bound on the time interval between an event's initiation and its completion, and we propose an algorithm for the computation of their behavior. Our algorithm effectively decomposes the computation into two stages: a pure CTMC governs event initiations while a deterministic process guarantees lower bounds on event completion times. Furthermore, from the nature of delayed CTMCs, we obtain a parallelized version of our algorithm. We use our formalism to model genetic regulatory circuits (biological systems where delayed events are common) and report on the results of our numerical algorithm as run on a cluster. We compare performance and accuracy of our results with results obtained by using pure CTMCs. © 2012 Springer-Verlag.","lang":"eng"}],"acknowledgement":"This work was supported by the ERC Advanced Investigator grant on Quantitative Reactive Modeling (QUAREM) and by the Swiss National Science Foundation.","oa_version":"None","publisher":"Springer","scopus_import":1,"alternative_title":["LNCS"],"quality_controlled":"1","month":"07","year":"2012","publication_status":"published","language":[{"iso":"eng"}],"day":"01","page":"294 - 309","ec_funded":1,"date_created":"2018-12-11T12:01:36Z","volume":"7358 ","date_published":"2012-07-01T00:00:00Z","doi":"10.1007/978-3-642-31424-7_24","_id":"3136","conference":{"name":"CAV: Computer Aided Verification","end_date":"2012-07-13","location":"Berkeley, CA, USA","start_date":"2012-07-07"},"type":"conference","status":"public","project":[{"grant_number":"267989","name":"Quantitative Reactive Modeling","_id":"25EE3708-B435-11E9-9278-68D0E5697425","call_identifier":"FP7"}],"citation":{"mla":"Guet, Calin C., et al. Delayed Continuous Time Markov Chains for Genetic Regulatory Circuits. Vol. 7358, Springer, 2012, pp. 294–309, doi:10.1007/978-3-642-31424-7_24.","apa":"Guet, C. C., Gupta, A., Henzinger, T. A., Mateescu, M., & Sezgin, A. (2012). Delayed continuous time Markov chains for genetic regulatory circuits (Vol. 7358, pp. 294–309). Presented at the CAV: Computer Aided Verification, Berkeley, CA, USA: Springer. https://doi.org/10.1007/978-3-642-31424-7_24","ama":"Guet CC, Gupta A, Henzinger TA, Mateescu M, Sezgin A. Delayed continuous time Markov chains for genetic regulatory circuits. In: Vol 7358. Springer; 2012:294-309. doi:10.1007/978-3-642-31424-7_24","short":"C.C. Guet, A. Gupta, T.A. Henzinger, M. Mateescu, A. Sezgin, in:, Springer, 2012, pp. 294–309.","ieee":"C. C. Guet, A. Gupta, T. A. Henzinger, M. Mateescu, and A. Sezgin, “Delayed continuous time Markov chains for genetic regulatory circuits,” presented at the CAV: Computer Aided Verification, Berkeley, CA, USA, 2012, vol. 7358, pp. 294–309.","chicago":"Guet, Calin C, Ashutosh Gupta, Thomas A Henzinger, Maria Mateescu, and Ali Sezgin. “Delayed Continuous Time Markov Chains for Genetic Regulatory Circuits,” 7358:294–309. Springer, 2012. https://doi.org/10.1007/978-3-642-31424-7_24.","ista":"Guet CC, Gupta A, Henzinger TA, Mateescu M, Sezgin A. 2012. Delayed continuous time Markov chains for genetic regulatory circuits. CAV: Computer Aided Verification, LNCS, vol. 7358, 294–309."},"date_updated":"2021-01-12T07:41:18Z","user_id":"3E5EF7F0-F248-11E8-B48F-1D18A9856A87","publist_id":"3561","author":[{"last_name":"Guet","full_name":"Guet, Calin C","orcid":"0000-0001-6220-2052","first_name":"Calin C","id":"47F8433E-F248-11E8-B48F-1D18A9856A87"},{"id":"335E5684-F248-11E8-B48F-1D18A9856A87","first_name":"Ashutosh","last_name":"Gupta","full_name":"Gupta, Ashutosh"},{"first_name":"Thomas A","id":"40876CD8-F248-11E8-B48F-1D18A9856A87","last_name":"Henzinger","orcid":"0000−0002−2985−7724","full_name":"Henzinger, Thomas A"},{"last_name":"Mateescu","full_name":"Mateescu, Maria","id":"3B43276C-F248-11E8-B48F-1D18A9856A87","first_name":"Maria"},{"first_name":"Ali","id":"4C7638DA-F248-11E8-B48F-1D18A9856A87","last_name":"Sezgin","full_name":"Sezgin, Ali"}],"department":[{"_id":"CaGu"},{"_id":"ToHe"}],"title":"Delayed continuous time Markov chains for genetic regulatory circuits"},{"volume":7214,"publication_identifier":{"eisbn":["9783642287565"],"issn":["0302-9743"],"isbn":["9783642287558"],"eissn":["1611-3349"]},"publication_status":"published","language":[{"iso":"eng"}],"scopus_import":"1","alternative_title":["LNCS"],"main_file_link":[{"open_access":"1","url":"https://doi.org/10.1007/978-3-642-28756-5_46"}],"place":"Berlin, Heidelberg","month":"04","intvolume":" 7214","abstract":[{"lang":"eng","text":"HSF(C) is a tool that automates verification of safety and liveness properties for C programs. This paper describes the verification approach taken by HSF(C) and provides instructions on how to install and use the tool."}],"oa_version":"Published Version","department":[{"_id":"ToHe"}],"date_updated":"2023-09-05T14:09:54Z","type":"conference","conference":{"name":"TACAS: Tools and Algorithms for the Construction and Analysis of Systems","location":"Tallinn, Estonia","end_date":"2012-04-01","start_date":"2012-03-24"},"status":"public","_id":"10906","series_title":"LNCS","page":"549-551","doi":"10.1007/978-3-642-28756-5_46","date_published":"2012-04-01T00:00:00Z","date_created":"2022-03-21T08:03:30Z","year":"2012","day":"01","publication":"Tools and Algorithms for the Construction and Analysis of Systems","publisher":"Springer","quality_controlled":"1","oa":1,"author":[{"last_name":"Grebenshchikov","full_name":"Grebenshchikov, Sergey","first_name":"Sergey"},{"first_name":"Ashutosh","id":"335E5684-F248-11E8-B48F-1D18A9856A87","last_name":"Gupta","full_name":"Gupta, Ashutosh"},{"full_name":"Lopes, Nuno P.","last_name":"Lopes","first_name":"Nuno P."},{"first_name":"Corneliu","last_name":"Popeea","full_name":"Popeea, Corneliu"},{"last_name":"Rybalchenko","full_name":"Rybalchenko, Andrey","first_name":"Andrey"}],"article_processing_charge":"No","editor":[{"first_name":"Cormac","full_name":"Flanagan, Cormac","last_name":"Flanagan"},{"last_name":"König","full_name":"König, Barbara","first_name":"Barbara"}],"title":"HSF(C): A software verifier based on Horn clauses","citation":{"ista":"Grebenshchikov S, Gupta A, Lopes NP, Popeea C, Rybalchenko A. 2012. HSF(C): A software verifier based on Horn clauses. Tools and Algorithms for the Construction and Analysis of Systems. TACAS: Tools and Algorithms for the Construction and Analysis of SystemsLNCS, LNCS, vol. 7214, 549–551.","chicago":"Grebenshchikov, Sergey, Ashutosh Gupta, Nuno P. Lopes, Corneliu Popeea, and Andrey Rybalchenko. “HSF(C): A Software Verifier Based on Horn Clauses.” In Tools and Algorithms for the Construction and Analysis of Systems, edited by Cormac Flanagan and Barbara König, 7214:549–51. LNCS. Berlin, Heidelberg: Springer, 2012. https://doi.org/10.1007/978-3-642-28756-5_46.","ieee":"S. Grebenshchikov, A. Gupta, N. P. Lopes, C. Popeea, and A. Rybalchenko, “HSF(C): A software verifier based on Horn clauses,” in Tools and Algorithms for the Construction and Analysis of Systems, Tallinn, Estonia, 2012, vol. 7214, pp. 549–551.","short":"S. Grebenshchikov, A. Gupta, N.P. Lopes, C. Popeea, A. Rybalchenko, in:, C. Flanagan, B. König (Eds.), Tools and Algorithms for the Construction and Analysis of Systems, Springer, Berlin, Heidelberg, 2012, pp. 549–551.","ama":"Grebenshchikov S, Gupta A, Lopes NP, Popeea C, Rybalchenko A. HSF(C): A software verifier based on Horn clauses. In: Flanagan C, König B, eds. Tools and Algorithms for the Construction and Analysis of Systems. Vol 7214. LNCS. Berlin, Heidelberg: Springer; 2012:549-551. doi:10.1007/978-3-642-28756-5_46","apa":"Grebenshchikov, S., Gupta, A., Lopes, N. P., Popeea, C., & Rybalchenko, A. (2012). HSF(C): A software verifier based on Horn clauses. In C. Flanagan & B. König (Eds.), Tools and Algorithms for the Construction and Analysis of Systems (Vol. 7214, pp. 549–551). Berlin, Heidelberg: Springer. https://doi.org/10.1007/978-3-642-28756-5_46","mla":"Grebenshchikov, Sergey, et al. “HSF(C): A Software Verifier Based on Horn Clauses.” Tools and Algorithms for the Construction and Analysis of Systems, edited by Cormac Flanagan and Barbara König, vol. 7214, Springer, 2012, pp. 549–51, doi:10.1007/978-3-642-28756-5_46."},"user_id":"c635000d-4b10-11ee-a964-aac5a93f6ac1"},{"author":[{"full_name":"Gupta, Ashutosh","last_name":"Gupta","first_name":"Ashutosh","id":"335E5684-F248-11E8-B48F-1D18A9856A87"},{"last_name":"Popeea","full_name":"Popeea, Corneliu","first_name":"Corneliu"},{"first_name":"Andrey","last_name":"Rybalchenko","full_name":"Rybalchenko, Andrey"}],"publist_id":"3383","department":[{"_id":"ToHe"}],"editor":[{"last_name":"Yang","full_name":"Yang, Hongseok","first_name":"Hongseok"}],"title":"Solving recursion-free Horn clauses over LI+UIF","citation":{"mla":"Gupta, Ashutosh, et al. Solving Recursion-Free Horn Clauses over LI+UIF. Edited by Hongseok Yang, vol. 7078, Springer, 2011, pp. 188–203, doi:10.1007/978-3-642-25318-8_16.","short":"A. Gupta, C. Popeea, A. Rybalchenko, in:, H. Yang (Ed.), Springer, 2011, pp. 188–203.","ieee":"A. Gupta, C. Popeea, and A. Rybalchenko, “Solving recursion-free Horn clauses over LI+UIF,” presented at the APLAS: Asian Symposium on Programming Languages and Systems, Kenting, Taiwan, 2011, vol. 7078, pp. 188–203.","apa":"Gupta, A., Popeea, C., & Rybalchenko, A. (2011). Solving recursion-free Horn clauses over LI+UIF. In H. Yang (Ed.) (Vol. 7078, pp. 188–203). Presented at the APLAS: Asian Symposium on Programming Languages and Systems, Kenting, Taiwan: Springer. https://doi.org/10.1007/978-3-642-25318-8_16","ama":"Gupta A, Popeea C, Rybalchenko A. Solving recursion-free Horn clauses over LI+UIF. In: Yang H, ed. Vol 7078. Springer; 2011:188-203. doi:10.1007/978-3-642-25318-8_16","chicago":"Gupta, Ashutosh, Corneliu Popeea, and Andrey Rybalchenko. “Solving Recursion-Free Horn Clauses over LI+UIF.” edited by Hongseok Yang, 7078:188–203. Springer, 2011. https://doi.org/10.1007/978-3-642-25318-8_16.","ista":"Gupta A, Popeea C, Rybalchenko A. 2011. Solving recursion-free Horn clauses over LI+UIF. APLAS: Asian Symposium on Programming Languages and Systems, LNCS, vol. 7078, 188–203."},"date_updated":"2021-01-12T07:42:15Z","user_id":"4435EBFC-F248-11E8-B48F-1D18A9856A87","conference":{"name":"APLAS: Asian Symposium on Programming Languages and Systems","start_date":"2011-12-05","location":"Kenting, Taiwan","end_date":"2011-12-07"},"type":"conference","status":"public","project":[{"name":"Rigorous Systems Engineering","grant_number":"S 11407_N23","_id":"25832EC2-B435-11E9-9278-68D0E5697425","call_identifier":"FWF"},{"call_identifier":"FP7","_id":"25EE3708-B435-11E9-9278-68D0E5697425","grant_number":"267989","name":"Quantitative Reactive Modeling"}],"_id":"3264","page":"188 - 203","date_created":"2018-12-11T12:02:20Z","ec_funded":1,"doi":"10.1007/978-3-642-25318-8_16","volume":7078,"date_published":"2011-12-05T00:00:00Z","year":"2011","publication_status":"published","language":[{"iso":"eng"}],"day":"05","publisher":"Springer","quality_controlled":"1","alternative_title":["LNCS"],"intvolume":" 7078","month":"12","abstract":[{"text":"Verification of programs with procedures, multi-threaded programs, and higher-order functional programs can be effectively au- tomated using abstraction and refinement schemes that rely on spurious counterexamples for abstraction discovery. The analysis of counterexam- ples can be automated by a series of interpolation queries, or, alterna- tively, as a constraint solving query expressed by a set of recursion free Horn clauses. (A set of interpolation queries can be formulated as a single constraint over Horn clauses with linear dependency structure between the unknown relations.) In this paper we present an algorithm for solving recursion free Horn clauses over a combined theory of linear real/rational arithmetic and uninterpreted functions. Our algorithm performs resolu- tion to deal with the clausal structure and relies on partial solutions to deal with (non-local) instances of functionality axioms.","lang":"eng"}],"oa_version":"None"},{"publication_status":"published","year":"2008","day":"01","page":"147 - 158","doi":"10.1145/1328438.1328459","date_published":"2008-01-01T00:00:00Z","date_created":"2018-12-11T12:09:17Z","abstract":[{"lang":"eng","text":"The search for proof and the search for counterexamples (bugs) are complementary activities that need to be pursued concurrently in order to maximize the practical success rate of verification tools.While this is well-understood in safety verification, the current focus of liveness verification has been almost exclusively on the search for termination proofs. A counterexample to termination is an infinite programexecution. In this paper, we propose a method to search for such counterexamples. The search proceeds in two phases. We first dynamically enumerate lasso-shaped candidate paths for counterexamples, and then statically prove their feasibility. We illustrate the utility of our nontermination prover, called TNT, on several nontrivial examples, some of which require bit-level reasoning about integer representations."}],"quality_controlled":0,"publisher":"ACM","main_file_link":[{"url":"http://pub.ist.ac.at/%7Etah/Publications/proving_non-termination.pdf","open_access":"0"}],"month":"01","date_updated":"2021-01-12T07:59:25Z","citation":{"chicago":"Gupta, Ashutosh, Thomas A Henzinger, Ritankar Majumdar, Andrey Rybalchenko, and Ru Xu. “Proving Non-Termination,” 147–58. ACM, 2008. https://doi.org/10.1145/1328438.1328459.","ista":"Gupta A, Henzinger TA, Majumdar R, Rybalchenko A, Xu R. 2008. Proving non-termination. POPL: Principles of Programming Languages, 147–158.","mla":"Gupta, Ashutosh, et al. Proving Non-Termination. ACM, 2008, pp. 147–58, doi:10.1145/1328438.1328459.","short":"A. Gupta, T.A. Henzinger, R. Majumdar, A. Rybalchenko, R. Xu, in:, ACM, 2008, pp. 147–158.","ieee":"A. Gupta, T. A. Henzinger, R. Majumdar, A. Rybalchenko, and R. Xu, “Proving non-termination,” presented at the POPL: Principles of Programming Languages, 2008, pp. 147–158.","apa":"Gupta, A., Henzinger, T. A., Majumdar, R., Rybalchenko, A., & Xu, R. (2008). Proving non-termination (pp. 147–158). Presented at the POPL: Principles of Programming Languages, ACM. https://doi.org/10.1145/1328438.1328459","ama":"Gupta A, Henzinger TA, Majumdar R, Rybalchenko A, Xu R. Proving non-termination. In: ACM; 2008:147-158. doi:10.1145/1328438.1328459"},"extern":1,"author":[{"id":"335E5684-F248-11E8-B48F-1D18A9856A87","first_name":"Ashutosh","full_name":"Ashutosh Gupta","last_name":"Gupta"},{"first_name":"Thomas A","id":"40876CD8-F248-11E8-B48F-1D18A9856A87","orcid":"0000−0002−2985−7724","full_name":"Thomas Henzinger","last_name":"Henzinger"},{"first_name":"Ritankar","full_name":"Majumdar, Ritankar S","last_name":"Majumdar"},{"last_name":"Rybalchenko","full_name":"Rybalchenko, Andrey","first_name":"Andrey"},{"full_name":"Xu, Ru-Gang","last_name":"Xu","first_name":"Ru"}],"publist_id":"208","title":"Proving non-termination","_id":"4521","type":"conference","conference":{"name":"POPL: Principles of Programming Languages"},"status":"public"}]