[{"title":"Monitoring robustness and individual fairness","department":[{"_id":"ToHe"}],"type":"conference","oa_version":"Published Version","project":[{"_id":"62781420-2b32-11ec-9570-8d9b63373d4d","call_identifier":"H2020","name":"Vigilant Algorithmic Monitoring of Software","grant_number":"101020093"}],"ec_funded":1,"arxiv":1,"user_id":"2DF688A6-F248-11E8-B48F-1D18A9856A87","page":"790-801","status":"public","publication_status":"published","conference":{"start_date":"2025-08-03","location":"Toronto, Canada","end_date":"2025-08-07","name":"KDD: Conference on Knowledge Discovery and Data Mining"},"date_updated":"2025-09-08T08:54:24Z","intvolume":"         2","doi":"10.1145/3711896.3737054","scopus_import":"1","language":[{"iso":"eng"}],"article_processing_charge":"No","ddc":["000"],"_id":"20292","file":[{"content_type":"application/pdf","date_created":"2025-09-08T08:46:31Z","success":1,"file_name":"2025_KDD_Gupta.pdf","checksum":"81e18cdf9ca5f6dfa79425b326ea9725","access_level":"open_access","date_updated":"2025-09-08T08:46:31Z","relation":"main_file","file_size":7745940,"creator":"dernst","file_id":"20310"}],"volume":2,"date_created":"2025-09-07T22:01:33Z","day":"03","year":"2025","oa":1,"month":"08","quality_controlled":"1","related_material":{"link":[{"url":"https://github.com/ariez-xyz/clemont","relation":"software"}]},"author":[{"id":"335E5684-F248-11E8-B48F-1D18A9856A87","first_name":"Ashutosh","last_name":"Gupta","full_name":"Gupta, Ashutosh"},{"first_name":"Thomas A","last_name":"Henzinger","orcid":"0000-0002-2985-7724","id":"40876CD8-F248-11E8-B48F-1D18A9856A87","full_name":"Henzinger, Thomas A"},{"full_name":"Kueffner, Konstantin","id":"8121a2d0-dc85-11ea-9058-af578f3b4515","orcid":"0000-0001-8974-2542","first_name":"Konstantin","last_name":"Kueffner"},{"last_name":"Mallik","first_name":"Kaushik","orcid":"0000-0001-9864-7475","id":"0834ff3c-6d72-11ec-94e0-b5b0a4fb8598","full_name":"Mallik, Kaushik"},{"last_name":"Pape","first_name":"David","full_name":"Pape, David"}],"citation":{"ama":"Gupta A, Henzinger TA, Kueffner K, Mallik K, Pape D. Monitoring robustness and individual fairness. In: <i>Proceedings of the 31st ACM SIGKDD Conference on Knowledge Discovery and Data Mining</i>. Vol 2. Association for Computing Machinery; 2025:790-801. doi:<a href=\"https://doi.org/10.1145/3711896.3737054\">10.1145/3711896.3737054</a>","mla":"Gupta, Ashutosh, et al. “Monitoring Robustness and Individual Fairness.” <i>Proceedings of the 31st ACM SIGKDD Conference on Knowledge Discovery and Data Mining</i>, vol. 2, Association for Computing Machinery, 2025, pp. 790–801, doi:<a href=\"https://doi.org/10.1145/3711896.3737054\">10.1145/3711896.3737054</a>.","ista":"Gupta A, Henzinger TA, Kueffner K, Mallik K, Pape D. 2025. Monitoring robustness and individual fairness. Proceedings of the 31st ACM SIGKDD Conference on Knowledge Discovery and Data Mining. KDD: Conference on Knowledge Discovery and Data Mining vol. 2, 790–801.","ieee":"A. Gupta, T. A. Henzinger, K. Kueffner, K. Mallik, and D. Pape, “Monitoring robustness and individual fairness,” in <i>Proceedings of the 31st ACM SIGKDD Conference on Knowledge Discovery and Data Mining</i>, Toronto, Canada, 2025, vol. 2, pp. 790–801.","chicago":"Gupta, Ashutosh, Thomas A Henzinger, Konstantin Kueffner, Kaushik Mallik, and David Pape. “Monitoring Robustness and Individual Fairness.” In <i>Proceedings of the 31st ACM SIGKDD Conference on Knowledge Discovery and Data Mining</i>, 2:790–801. Association for Computing Machinery, 2025. <a href=\"https://doi.org/10.1145/3711896.3737054\">https://doi.org/10.1145/3711896.3737054</a>.","short":"A. Gupta, T.A. Henzinger, K. Kueffner, K. Mallik, D. Pape, in:, Proceedings of the 31st ACM SIGKDD Conference on Knowledge Discovery and Data Mining, Association for Computing Machinery, 2025, pp. 790–801.","apa":"Gupta, A., Henzinger, T. A., Kueffner, K., Mallik, K., &#38; Pape, D. (2025). Monitoring robustness and individual fairness. In <i>Proceedings of the 31st ACM SIGKDD Conference on Knowledge Discovery and Data Mining</i> (Vol. 2, pp. 790–801). Toronto, Canada: Association for Computing Machinery. <a href=\"https://doi.org/10.1145/3711896.3737054\">https://doi.org/10.1145/3711896.3737054</a>"},"abstract":[{"lang":"eng","text":"In automated decision-making, it is desirable that outputs of decision-makers be robust to slight perturbations in their inputs, a property that may be called input-output robustness. Input-output robustness appears in various different forms in the literature, such as robustness of AI models to adversarial or semantic perturbations and individual fairness of AI models that make decisions about humans. We propose runtime monitoring of input-output robustness of deployed, black-box AI models, where the goal is to design monitors that would observe one long execution sequence of the model, and would raise an alarm whenever it is detected that two similar inputs from the past led to dissimilar outputs. This way, monitoring will complement existing offline ''robustification'' approaches to increase the trustworthiness of AI decision-makers. We show that the monitoring problem can be cast as the fixed-radius nearest neighbor (FRNN) search problem, which, despite being well-studied, lacks suitable online solutions. We present our tool Clemont, which offers a number of lightweight monitors, some of which use upgraded online variants of existing FRNN algorithms, and one uses a novel algorithm based on binary decision diagrams--a data-structure commonly used in software and hardware verification. We have also developed an efficient parallelization technique that can substantially cut down the computation time of monitors for which the distance between input-output pairs is measured using the L∞norm. Using standard benchmarks from the literature of adversarial and semantic robustness and individual fairness, we perform a comparative study of different monitors in Clemont, and demonstrate their effectiveness in correctly detecting robustness violations at runtime."}],"corr_author":"1","publication":"Proceedings of the 31st ACM SIGKDD Conference on Knowledge Discovery and Data Mining","acknowledgement":"This work was supported in part by the ERC project ERC-2020-AdG 101020093 and the SBI Foundation Hub for Data Science &Analytics, IIT Bombay.","file_date_updated":"2025-09-08T08:46:31Z","date_published":"2025-08-03T00:00:00Z","external_id":{"arxiv":["2506.00496"]},"OA_place":"publisher","publication_identifier":{"issn":["2154-817X"],"isbn":["9798400714542"]},"has_accepted_license":"1","publisher":"Association for Computing Machinery","tmp":{"short":"CC BY (4.0)","legal_code_url":"https://creativecommons.org/licenses/by/4.0/legalcode","name":"Creative Commons Attribution 4.0 International Public License (CC-BY 4.0)","image":"/images/cc_by.png"}},{"date_created":"2018-12-11T11:51:32Z","day":"01","year":"2017","volume":54,"month":"12","quality_controlled":"1","related_material":{"record":[{"relation":"earlier_version","status":"public","id":"1835"}]},"author":[{"orcid":"0000-0001-8180-0904","id":"3444EA5E-F248-11E8-B48F-1D18A9856A87","last_name":"Giacobbe","first_name":"Mirco","full_name":"Giacobbe, Mirco"},{"id":"47F8433E-F248-11E8-B48F-1D18A9856A87","orcid":"0000-0001-6220-2052","first_name":"Calin C","last_name":"Guet","full_name":"Guet, Calin C"},{"first_name":"Ashutosh","last_name":"Gupta","id":"335E5684-F248-11E8-B48F-1D18A9856A87","full_name":"Gupta, Ashutosh"},{"id":"40876CD8-F248-11E8-B48F-1D18A9856A87","orcid":"0000−0002−2985−7724","first_name":"Thomas A","last_name":"Henzinger","full_name":"Henzinger, Thomas A"},{"id":"2C5658E6-F248-11E8-B48F-1D18A9856A87","orcid":"0000-0003-2361-3953","last_name":"Paixao","first_name":"Tiago","full_name":"Paixao, Tiago"},{"first_name":"Tatjana","last_name":"Petrov","orcid":"0000-0002-9041-0905","id":"3D5811FC-F248-11E8-B48F-1D18A9856A87","full_name":"Petrov, Tatjana"}],"oa":1,"publication":"Acta Informatica","citation":{"ieee":"M. Giacobbe, C. C. Guet, A. Gupta, T. A. Henzinger, T. Paixao, and T. Petrov, “Model checking the evolution of gene regulatory networks,” <i>Acta Informatica</i>, 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.","chicago":"Giacobbe, Mirco, Calin C Guet, Ashutosh Gupta, Thomas A Henzinger, Tiago Paixao, and Tatjana Petrov. “Model Checking the Evolution of Gene Regulatory Networks.” <i>Acta Informatica</i>. Springer, 2017. <a href=\"https://doi.org/10.1007/s00236-016-0278-x\">https://doi.org/10.1007/s00236-016-0278-x</a>.","apa":"Giacobbe, M., Guet, C. C., Gupta, A., Henzinger, T. A., Paixao, T., &#38; Petrov, T. (2017). Model checking the evolution of gene regulatory networks. <i>Acta Informatica</i>. Springer. <a href=\"https://doi.org/10.1007/s00236-016-0278-x\">https://doi.org/10.1007/s00236-016-0278-x</a>","ama":"Giacobbe M, Guet CC, Gupta A, Henzinger TA, Paixao T, Petrov T. Model checking the evolution of gene regulatory networks. <i>Acta Informatica</i>. 2017;54(8):765-787. doi:<a href=\"https://doi.org/10.1007/s00236-016-0278-x\">10.1007/s00236-016-0278-x</a>","mla":"Giacobbe, Mirco, et al. “Model Checking the Evolution of Gene Regulatory Networks.” <i>Acta Informatica</i>, vol. 54, no. 8, Springer, 2017, pp. 765–87, doi:<a href=\"https://doi.org/10.1007/s00236-016-0278-x\">10.1007/s00236-016-0278-x</a>.","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."},"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"}],"corr_author":"1","has_accepted_license":"1","isi":1,"publisher":"Springer","tmp":{"short":"CC BY (4.0)","legal_code_url":"https://creativecommons.org/licenses/by/4.0/legalcode","name":"Creative Commons Attribution 4.0 International Public License (CC-BY 4.0)","image":"/images/cc_by.png"},"external_id":{"isi":["000414343200003"]},"date_published":"2017-12-01T00:00:00Z","file_date_updated":"2020-07-14T12:44:46Z","publication_identifier":{"issn":["0001-5903"]},"publist_id":"5898","type":"journal_article","oa_version":"Published Version","title":"Model checking the evolution of gene regulatory networks","pubrep_id":"649","department":[{"_id":"ToHe"},{"_id":"CaGu"},{"_id":"NiBa"}],"user_id":"2DF688A6-F248-11E8-B48F-1D18A9856A87","page":"765 - 787","project":[{"name":"Quantitative Reactive Modeling","grant_number":"267989","call_identifier":"FP7","_id":"25EE3708-B435-11E9-9278-68D0E5697425"},{"_id":"25832EC2-B435-11E9-9278-68D0E5697425","call_identifier":"FWF","name":"Rigorous Systems Engineering","grant_number":"S 11407_N23"},{"call_identifier":"FWF","name":"Formal methods for the design and analysis of complex systems","grant_number":"Z211","_id":"25F42A32-B435-11E9-9278-68D0E5697425"},{"_id":"25B1EC9E-B435-11E9-9278-68D0E5697425","grant_number":"618091","name":"Speed of Adaptation in Population Genetics and Evolutionary Computation","call_identifier":"FP7"},{"_id":"25681D80-B435-11E9-9278-68D0E5697425","grant_number":"291734","name":"International IST Postdoc Fellowship Programme","call_identifier":"FP7"},{"grant_number":"250152","name":"Limits to selection in biology and in evolutionary computation","call_identifier":"FP7","_id":"25B07788-B435-11E9-9278-68D0E5697425"}],"ec_funded":1,"intvolume":"        54","scopus_import":"1","doi":"10.1007/s00236-016-0278-x","status":"public","publication_status":"published","issue":"8","date_updated":"2025-07-10T11:50:42Z","language":[{"iso":"eng"}],"article_processing_charge":"No","ddc":["006","576"],"_id":"1351","file":[{"access_level":"open_access","date_updated":"2020-07-14T12:44:46Z","file_name":"2017_ActaInformatica_Giacobbe.pdf","checksum":"4e661d9135d7f8c342e8e258dee76f3e","content_type":"application/pdf","date_created":"2019-01-17T15:57:29Z","file_id":"5841","creator":"dernst","file_size":755241,"relation":"main_file"}]},{"oa":1,"author":[{"id":"49351290-F248-11E8-B48F-1D18A9856A87","last_name":"Daca","first_name":"Przemyslaw","full_name":"Daca, Przemyslaw"},{"id":"335E5684-F248-11E8-B48F-1D18A9856A87","last_name":"Gupta","first_name":"Ashutosh","full_name":"Gupta, Ashutosh"},{"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":[{"relation":"dissertation_contains","status":"public","id":"1155"}]},"quality_controlled":"1","month":"01","volume":9583,"year":"2016","day":"01","date_created":"2018-12-11T11:50:50Z","alternative_title":["LNCS"],"publist_id":"6104","date_published":"2016-01-01T00:00:00Z","external_id":{"arxiv":["1511.02615"],"isi":["000375148800016"]},"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).","publisher":"Springer","isi":1,"abstract":[{"lang":"eng","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."}],"citation":{"short":"P. Daca, A. Gupta, T.A. Henzinger, in:, Springer, 2016, pp. 328–347.","chicago":"Daca, Przemyslaw, Ashutosh Gupta, and Thomas A Henzinger. “Abstraction-Driven Concolic Testing,” 9583:328–47. Springer, 2016. <a href=\"https://doi.org/10.1007/978-3-662-49122-5_16\">https://doi.org/10.1007/978-3-662-49122-5_16</a>.","apa":"Daca, P., Gupta, A., &#38; 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. <a href=\"https://doi.org/10.1007/978-3-662-49122-5_16\">https://doi.org/10.1007/978-3-662-49122-5_16</a>","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.","ista":"Daca P, Gupta A, Henzinger TA. 2016. Abstraction-driven concolic testing. VMCAI: Verification, Model Checking and Abstract Interpretation, LNCS, vol. 9583, 328–347.","ama":"Daca P, Gupta A, Henzinger TA. Abstraction-driven concolic testing. In: Vol 9583. Springer; 2016:328-347. doi:<a href=\"https://doi.org/10.1007/978-3-662-49122-5_16\">10.1007/978-3-662-49122-5_16</a>","mla":"Daca, Przemyslaw, et al. <i>Abstraction-Driven Concolic Testing</i>. Vol. 9583, Springer, 2016, pp. 328–47, doi:<a href=\"https://doi.org/10.1007/978-3-662-49122-5_16\">10.1007/978-3-662-49122-5_16</a>."},"main_file_link":[{"open_access":"1","url":"https://arxiv.org/abs/1511.02615"}],"ec_funded":1,"project":[{"grant_number":"267989","name":"Quantitative Reactive Modeling","call_identifier":"FP7","_id":"25EE3708-B435-11E9-9278-68D0E5697425"},{"name":"Formal methods for the design and analysis of complex systems","grant_number":"Z211","call_identifier":"FWF","_id":"25F42A32-B435-11E9-9278-68D0E5697425"},{"call_identifier":"FWF","grant_number":"S 11407_N23","name":"Rigorous Systems Engineering","_id":"25832EC2-B435-11E9-9278-68D0E5697425"}],"page":"328 - 347","user_id":"317138e5-6ab7-11ef-aa6d-ffef3953e345","arxiv":1,"department":[{"_id":"ToHe"}],"title":"Abstraction-driven concolic testing","oa_version":"Preprint","type":"conference","_id":"1230","article_processing_charge":"No","language":[{"iso":"eng"}],"date_updated":"2026-04-15T10:02:12Z","conference":{"name":"VMCAI: Verification, Model Checking and Abstract Interpretation","end_date":"2016-01-19","start_date":"2016-01-17","location":"St. Petersburg, FL, USA"},"publication_status":"published","status":"public","doi":"10.1007/978-3-662-49122-5_16","scopus_import":"1","intvolume":"      9583"},{"publist_id":"5091","file_date_updated":"2020-07-14T12:45:22Z","date_published":"2015-01-15T00:00:00Z","publication_identifier":{"isbn":["978-1-4503-3300-9"]},"publisher":"ACM","has_accepted_license":"1","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"}],"citation":{"chicago":"Gupta, Ashutosh, Thomas A Henzinger, Arjun Radhakrishna, Roopsha Samanta, and Thorsten Tarrach. “Succinct Representation of Concurrent Trace Sets,” 433–44. ACM, 2015. <a href=\"https://doi.org/10.1145/2676726.2677008\">https://doi.org/10.1145/2676726.2677008</a>.","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., &#38; Tarrach, T. (2015). Succinct representation of concurrent trace sets (pp. 433–444). Presented at the POPL: Principles of Programming Languages, Mumbai, India: ACM. <a href=\"https://doi.org/10.1145/2676726.2677008\">https://doi.org/10.1145/2676726.2677008</a>","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.","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.","ama":"Gupta A, Henzinger TA, Radhakrishna A, Samanta R, Tarrach T. Succinct representation of concurrent trace sets. In: ACM; 2015:433-444. doi:<a href=\"https://doi.org/10.1145/2676726.2677008\">10.1145/2676726.2677008</a>","mla":"Gupta, Ashutosh, et al. <i>Succinct Representation of Concurrent Trace Sets</i>. ACM, 2015, pp. 433–44, doi:<a href=\"https://doi.org/10.1145/2676726.2677008\">10.1145/2676726.2677008</a>."},"oa":1,"quality_controlled":"1","author":[{"full_name":"Gupta, Ashutosh","last_name":"Gupta","first_name":"Ashutosh","id":"335E5684-F248-11E8-B48F-1D18A9856A87"},{"id":"40876CD8-F248-11E8-B48F-1D18A9856A87","orcid":"0000−0002−2985−7724","last_name":"Henzinger","first_name":"Thomas A","full_name":"Henzinger, Thomas A"},{"full_name":"Radhakrishna, Arjun","first_name":"Arjun","last_name":"Radhakrishna","id":"3B51CAC4-F248-11E8-B48F-1D18A9856A87"},{"full_name":"Samanta, Roopsha","id":"3D2AAC08-F248-11E8-B48F-1D18A9856A87","first_name":"Roopsha","last_name":"Samanta"},{"last_name":"Tarrach","first_name":"Thorsten","orcid":"0000-0003-4409-8487","id":"3D6E8F2C-F248-11E8-B48F-1D18A9856A87","full_name":"Tarrach, Thorsten"}],"month":"01","day":"15","year":"2015","date_created":"2018-12-11T11:55:05Z","ddc":["005"],"_id":"1992","file":[{"file_name":"IST-2015-317-v1+1_author_version.pdf","checksum":"f0d4395b600f410a191256ac0b73af32","access_level":"open_access","date_updated":"2020-07-14T12:45:22Z","content_type":"application/pdf","date_created":"2018-12-12T10:17:56Z","file_id":"5314","creator":"system","file_size":399462,"relation":"main_file"}],"article_processing_charge":"No","language":[{"iso":"eng"}],"conference":{"start_date":"2015-01-15","location":"Mumbai, India","name":"POPL: Principles of Programming Languages","end_date":"2015-01-17"},"date_updated":"2025-03-07T08:44:29Z","status":"public","publication_status":"published","scopus_import":"1","doi":"10.1145/2676726.2677008","page":"433 - 444","user_id":"2DF688A6-F248-11E8-B48F-1D18A9856A87","pubrep_id":"317","department":[{"_id":"ToHe"}],"title":"Succinct representation of concurrent trace sets","type":"conference","oa_version":"Submitted Version"},{"title":"Guest editors' introduction to special issue on computational methods in systems biology","volume":25,"department":[{"_id":"ToHe"}],"type":"journal_article","date_created":"2018-12-11T11:54:07Z","oa_version":"None","article_number":"7","day":"01","year":"2015","user_id":"317138e5-6ab7-11ef-aa6d-ffef3953e345","month":"05","quality_controlled":"1","author":[{"last_name":"Gupta","first_name":"Ashutosh","id":"335E5684-F248-11E8-B48F-1D18A9856A87","full_name":"Gupta, Ashutosh"},{"full_name":"Henzinger, Thomas A","orcid":"0000−0002−2985−7724","id":"40876CD8-F248-11E8-B48F-1D18A9856A87","last_name":"Henzinger","first_name":"Thomas A"}],"citation":{"ieee":"A. Gupta and T. A. Henzinger, “Guest editors’ introduction to special issue on computational methods in systems biology,” <i>ACM Transactions on Modeling and Computer Simulation</i>, vol. 25, no. 2. ACM, 2015.","short":"A. Gupta, T.A. Henzinger, ACM Transactions on Modeling and Computer Simulation 25 (2015).","chicago":"Gupta, Ashutosh, and Thomas A Henzinger. “Guest Editors’ Introduction to Special Issue on Computational Methods in Systems Biology.” <i>ACM Transactions on Modeling and Computer Simulation</i>. ACM, 2015. <a href=\"https://doi.org/10.1145/2745799\">https://doi.org/10.1145/2745799</a>.","apa":"Gupta, A., &#38; Henzinger, T. A. (2015). Guest editors’ introduction to special issue on computational methods in systems biology. <i>ACM Transactions on Modeling and Computer Simulation</i>. ACM. <a href=\"https://doi.org/10.1145/2745799\">https://doi.org/10.1145/2745799</a>","ama":"Gupta A, Henzinger TA. Guest editors’ introduction to special issue on computational methods in systems biology. <i>ACM Transactions on Modeling and Computer Simulation</i>. 2015;25(2). doi:<a href=\"https://doi.org/10.1145/2745799\">10.1145/2745799</a>","mla":"Gupta, Ashutosh, and Thomas A. Henzinger. “Guest Editors’ Introduction to Special Issue on Computational Methods in Systems Biology.” <i>ACM Transactions on Modeling and Computer Simulation</i>, vol. 25, no. 2, 7, ACM, 2015, doi:<a href=\"https://doi.org/10.1145/2745799\">10.1145/2745799</a>.","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."},"status":"public","publication_status":"published","issue":"2","date_updated":"2025-09-23T09:11:51Z","intvolume":"        25","doi":"10.1145/2745799","scopus_import":"1","publication":"ACM Transactions on Modeling and Computer Simulation","external_id":{"isi":["000354789200001"]},"date_published":"2015-05-01T00:00:00Z","publist_id":"5302","article_processing_charge":"No","language":[{"iso":"eng"}],"publisher":"ACM","isi":1,"_id":"1808"},{"intvolume":"      9035","doi":"10.1007/978-3-662-46681-0_47","scopus_import":"1","publication_status":"published","status":"public","date_updated":"2025-07-10T11:50:42Z","conference":{"start_date":"2015-04-11","location":"London, United Kingdom","name":"TACAS: Tools and Algorithms for the Construction and Analysis of Systems","end_date":"2015-04-18"},"language":[{"iso":"eng"}],"article_processing_charge":"No","_id":"1835","oa_version":"Preprint","type":"conference","title":"Model checking gene regulatory networks","department":[{"_id":"ToHe"},{"_id":"CaGu"},{"_id":"NiBa"}],"user_id":"2DF688A6-F248-11E8-B48F-1D18A9856A87","arxiv":1,"page":"469 - 483","project":[{"_id":"25EE3708-B435-11E9-9278-68D0E5697425","name":"Quantitative Reactive Modeling","grant_number":"267989","call_identifier":"FP7"},{"_id":"25832EC2-B435-11E9-9278-68D0E5697425","call_identifier":"FWF","grant_number":"S 11407_N23","name":"Rigorous Systems Engineering"},{"name":"Formal methods for the design and analysis of complex systems","grant_number":"Z211","call_identifier":"FWF","_id":"25F42A32-B435-11E9-9278-68D0E5697425"},{"_id":"25B1EC9E-B435-11E9-9278-68D0E5697425","grant_number":"618091","name":"Speed of Adaptation in Population Genetics and Evolutionary Computation","call_identifier":"FP7"},{"grant_number":"250152","name":"Limits to selection in biology and in evolutionary computation","call_identifier":"FP7","_id":"25B07788-B435-11E9-9278-68D0E5697425"},{"call_identifier":"FP7","grant_number":"291734","name":"International IST Postdoc Fellowship Programme","_id":"25681D80-B435-11E9-9278-68D0E5697425"}],"ec_funded":1,"main_file_link":[{"url":"http://arxiv.org/abs/1410.7704","open_access":"1"}],"citation":{"ista":"Giacobbe M, Guet CC, Gupta A, Henzinger TA, Paixao T, Petrov T. 2015. Model checking gene regulatory networks. 9035, 469–483.","mla":"Giacobbe, Mirco, et al. <i>Model Checking Gene Regulatory Networks</i>. Vol. 9035, Springer, 2015, pp. 469–83, doi:<a href=\"https://doi.org/10.1007/978-3-662-46681-0_47\">10.1007/978-3-662-46681-0_47</a>.","ama":"Giacobbe M, Guet CC, Gupta A, Henzinger TA, Paixao T, Petrov T. Model checking gene regulatory networks. 2015;9035:469-483. doi:<a href=\"https://doi.org/10.1007/978-3-662-46681-0_47\">10.1007/978-3-662-46681-0_47</a>","apa":"Giacobbe, M., Guet, C. C., Gupta, A., Henzinger, T. A., Paixao, T., &#38; 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. <a href=\"https://doi.org/10.1007/978-3-662-46681-0_47\">https://doi.org/10.1007/978-3-662-46681-0_47</a>","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. <a href=\"https://doi.org/10.1007/978-3-662-46681-0_47\">https://doi.org/10.1007/978-3-662-46681-0_47</a>.","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."},"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 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.","lang":"eng"}],"publisher":"Springer","date_published":"2015-04-01T00:00:00Z","external_id":{"arxiv":["1410.7704"]},"acknowledgement":"SNSF Early Postdoc.Mobility Fellowship, the grant number P2EZP2 148797.\r\n","publist_id":"5267","date_created":"2018-12-11T11:54:16Z","series_title":"Lecture Notes in Computer Science","alternative_title":["LNCS"],"year":"2015","day":"01","volume":9035,"month":"04","related_material":{"record":[{"relation":"later_version","id":"1351","status":"public"}]},"author":[{"full_name":"Giacobbe, Mirco","orcid":"0000-0001-8180-0904","id":"3444EA5E-F248-11E8-B48F-1D18A9856A87","last_name":"Giacobbe","first_name":"Mirco"},{"last_name":"Guet","first_name":"Calin C","orcid":"0000-0001-6220-2052","id":"47F8433E-F248-11E8-B48F-1D18A9856A87","full_name":"Guet, Calin C"},{"full_name":"Gupta, Ashutosh","id":"335E5684-F248-11E8-B48F-1D18A9856A87","first_name":"Ashutosh","last_name":"Gupta"},{"full_name":"Henzinger, Thomas A","id":"40876CD8-F248-11E8-B48F-1D18A9856A87","orcid":"0000−0002−2985−7724","last_name":"Henzinger","first_name":"Thomas A"},{"full_name":"Paixao, Tiago","last_name":"Paixao","first_name":"Tiago","id":"2C5658E6-F248-11E8-B48F-1D18A9856A87","orcid":"0000-0003-2361-3953"},{"full_name":"Petrov, Tatjana","first_name":"Tatjana","last_name":"Petrov","id":"3D5811FC-F248-11E8-B48F-1D18A9856A87","orcid":"0000-0002-9041-0905"}],"quality_controlled":"1","oa":1},{"volume":169,"date_created":"2018-12-11T11:53:33Z","alternative_title":["EPTCS"],"year":"2014","day":"02","oa":1,"month":"12","author":[{"last_name":"Gupta","first_name":"Ashutosh","id":"335E5684-F248-11E8-B48F-1D18A9856A87","full_name":"Gupta, Ashutosh"},{"full_name":"Popeea, Corneliu","last_name":"Popeea","first_name":"Corneliu"},{"last_name":"Rybalchenko","first_name":"Andrey","full_name":"Rybalchenko, Andrey"}],"quality_controlled":"1","citation":{"apa":"Gupta, A., Popeea, C., &#38; Rybalchenko, A. (2014). Generalised interpolation by solving recursion free-horn clauses. In <i>Electronic Proceedings in Theoretical Computer Science, EPTCS</i> (Vol. 169, pp. 31–38). Vienna, Austria: Open Publishing Association. <a href=\"https://doi.org/10.4204/EPTCS.169.5\">https://doi.org/10.4204/EPTCS.169.5</a>","chicago":"Gupta, Ashutosh, Corneliu Popeea, and Andrey Rybalchenko. “Generalised Interpolation by Solving Recursion Free-Horn Clauses.” In <i>Electronic Proceedings in Theoretical Computer Science, EPTCS</i>, 169:31–38. Open Publishing Association, 2014. <a href=\"https://doi.org/10.4204/EPTCS.169.5\">https://doi.org/10.4204/EPTCS.169.5</a>.","short":"A. Gupta, C. Popeea, A. Rybalchenko, in:, Electronic Proceedings in Theoretical Computer Science, EPTCS, Open Publishing Association, 2014, pp. 31–38.","ieee":"A. Gupta, C. Popeea, and A. Rybalchenko, “Generalised interpolation by solving recursion free-horn clauses,” in <i>Electronic Proceedings in Theoretical Computer Science, EPTCS</i>, Vienna, Austria, 2014, vol. 169, pp. 31–38.","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.","mla":"Gupta, Ashutosh, et al. “Generalised Interpolation by Solving Recursion Free-Horn Clauses.” <i>Electronic Proceedings in Theoretical Computer Science, EPTCS</i>, vol. 169, Open Publishing Association, 2014, pp. 31–38, doi:<a href=\"https://doi.org/10.4204/EPTCS.169.5\">10.4204/EPTCS.169.5</a>.","ama":"Gupta A, Popeea C, Rybalchenko A. Generalised interpolation by solving recursion free-horn clauses. In: <i>Electronic Proceedings in Theoretical Computer Science, EPTCS</i>. Vol 169. Open Publishing Association; 2014:31-38. doi:<a href=\"https://doi.org/10.4204/EPTCS.169.5\">10.4204/EPTCS.169.5</a>"},"corr_author":"1","abstract":[{"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.","lang":"eng"}],"publication":"Electronic Proceedings in Theoretical Computer Science, EPTCS","main_file_link":[{"open_access":"1","url":"http://arxiv.org/abs/1303.7378"}],"external_id":{"arxiv":["1303.7378"]},"date_published":"2014-12-02T00:00:00Z","publist_id":"5435","publisher":"Open Publishing Association","title":"Generalised interpolation by solving recursion free-horn clauses","department":[{"_id":"ToHe"}],"oa_version":"Submitted Version","type":"conference","user_id":"2DF688A6-F248-11E8-B48F-1D18A9856A87","arxiv":1,"page":"31 - 38","publication_status":"published","status":"public","date_updated":"2025-06-11T08:03:28Z","conference":{"name":"HCVS: Horn Clauses for Verification and Synthesis","end_date":"2014-07-17","start_date":"2014-07-17","location":"Vienna, Austria"},"intvolume":"       169","scopus_import":"1","doi":"10.4204/EPTCS.169.5","language":[{"iso":"eng"}],"article_processing_charge":"No","_id":"1702"},{"scopus_import":"1","doi":"10.1007/978-3-319-13338-6_6","intvolume":"      8855","date_updated":"2024-10-21T06:02:48Z","conference":{"location":"Haifa, Israel","start_date":"2014-11-18","end_date":"2014-11-20","name":"HVC: Haifa Verification Conference"},"publication_status":"published","status":"public","_id":"1869","language":[{"iso":"eng"}],"oa_version":"None","type":"conference","department":[{"_id":"ToHe"}],"title":"Suraq - a controller synthesis tool using uninterpreted functions","page":"68 - 74","user_id":"4435EBFC-F248-11E8-B48F-1D18A9856A87","ec_funded":1,"project":[{"_id":"25EE3708-B435-11E9-9278-68D0E5697425","name":"Quantitative Reactive Modeling","grant_number":"267989","call_identifier":"FP7"},{"_id":"25863FF4-B435-11E9-9278-68D0E5697425","call_identifier":"FWF","grant_number":"S11407","name":"Game Theory"}],"publication":"HVC 2014","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"}],"citation":{"mla":"Hofferek, Georg, and Ashutosh Gupta. “Suraq - a Controller Synthesis Tool Using Uninterpreted Functions.” <i>HVC 2014</i>, edited by Eran Yahav, vol. 8855, Springer, 2014, pp. 68–74, doi:<a href=\"https://doi.org/10.1007/978-3-319-13338-6_6\">10.1007/978-3-319-13338-6_6</a>.","ama":"Hofferek G, Gupta A. Suraq - a controller synthesis tool using uninterpreted functions. In: Yahav E, ed. <i>HVC 2014</i>. Vol 8855. Springer; 2014:68-74. doi:<a href=\"https://doi.org/10.1007/978-3-319-13338-6_6\">10.1007/978-3-319-13338-6_6</a>","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.","ieee":"G. Hofferek and A. Gupta, “Suraq - a controller synthesis tool using uninterpreted functions,” in <i>HVC 2014</i>, Haifa, Israel, 2014, vol. 8855, pp. 68–74.","apa":"Hofferek, G., &#38; Gupta, A. (2014). Suraq - a controller synthesis tool using uninterpreted functions. In E. Yahav (Ed.), <i>HVC 2014</i> (Vol. 8855, pp. 68–74). Haifa, Israel: Springer. <a href=\"https://doi.org/10.1007/978-3-319-13338-6_6\">https://doi.org/10.1007/978-3-319-13338-6_6</a>","short":"G. Hofferek, A. Gupta, in:, E. Yahav (Ed.), HVC 2014, Springer, 2014, pp. 68–74.","chicago":"Hofferek, Georg, and Ashutosh Gupta. “Suraq - a Controller Synthesis Tool Using Uninterpreted Functions.” In <i>HVC 2014</i>, edited by Eran Yahav, 8855:68–74. Springer, 2014. <a href=\"https://doi.org/10.1007/978-3-319-13338-6_6\">https://doi.org/10.1007/978-3-319-13338-6_6</a>."},"publisher":"Springer","publist_id":"5228","acknowledgement":"The work presented in this paper was supported in part by the European Research Council (ERC) under grant agreement QUAINT (I774-N23)","date_published":"2014-01-01T00:00:00Z","year":"2014","day":"01","date_created":"2018-12-11T11:54:27Z","alternative_title":["LNCS"],"editor":[{"first_name":"Eran","last_name":"Yahav","full_name":"Yahav, Eran"}],"volume":8855,"author":[{"full_name":"Hofferek, Georg","first_name":"Georg","last_name":"Hofferek"},{"last_name":"Gupta","first_name":"Ashutosh","id":"335E5684-F248-11E8-B48F-1D18A9856A87","full_name":"Gupta, Ashutosh"}],"quality_controlled":"1","month":"01"},{"department":[{"_id":"ToHe"}],"pubrep_id":"641","title":"Extensional crisis and proving identity","oa_version":"Submitted Version","type":"conference","ec_funded":1,"project":[{"_id":"25EE3708-B435-11E9-9278-68D0E5697425","call_identifier":"FP7","name":"Quantitative Reactive Modeling","grant_number":"267989"},{"_id":"25F5A88A-B435-11E9-9278-68D0E5697425","name":"Moderne Concurrency Paradigms","grant_number":"S11402-N23","call_identifier":"FWF"}],"page":"185 - 200","user_id":"2DF688A6-F248-11E8-B48F-1D18A9856A87","date_updated":"2026-07-08T06:49:33Z","conference":{"name":"ATVA: Automated Technology for Verification and Analysis","end_date":"2014-11-07","location":"Sydney, Australia","start_date":"2014-11-03"},"publication_status":"published","status":"public","doi":"10.1007/978-3-319-11936-6_14","scopus_import":"1","intvolume":"      8837","_id":"1872","file":[{"content_type":"application/pdf","date_created":"2018-12-12T10:10:15Z","file_name":"IST-2016-641-v1+1_atva2014.pdf","checksum":"af4bd3fc1f4c93075e4dc5cbf625fe7b","access_level":"open_access","date_updated":"2020-07-14T12:45:19Z","file_size":244294,"relation":"main_file","creator":"system","file_id":"4801"}],"ddc":["000"],"language":[{"iso":"eng"}],"article_processing_charge":"No","volume":8837,"year":"2014","day":"01","date_created":"2018-12-11T11:54:28Z","alternative_title":["LNCS"],"oa":1,"author":[{"full_name":"Gupta, Ashutosh","first_name":"Ashutosh","last_name":"Gupta","id":"335E5684-F248-11E8-B48F-1D18A9856A87"},{"first_name":"Laura","last_name":"Kovács","full_name":"Kovács, Laura"},{"full_name":"Kragl, Bernhard","last_name":"Kragl","first_name":"Bernhard","id":"320FC952-F248-11E8-B48F-1D18A9856A87","orcid":"0000-0001-7745-9117"},{"full_name":"Voronkov, Andrei","first_name":"Andrei","last_name":"Voronkov"}],"quality_controlled":"1","month":"01","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."}],"citation":{"mla":"Gupta, Ashutosh, et al. “Extensional Crisis and Proving Identity.” <i>12th International Symposium on Automated Technology for Verification and Analysis</i>, vol. 8837, Springer, 2014, pp. 185–200, doi:<a href=\"https://doi.org/10.1007/978-3-319-11936-6_14\">10.1007/978-3-319-11936-6_14</a>.","ama":"Gupta A, Kovács L, Kragl B, Voronkov A. Extensional crisis and proving identity. In: <i>12th International Symposium on Automated Technology for Verification and Analysis</i>. Vol 8837. Springer; 2014:185-200. doi:<a href=\"https://doi.org/10.1007/978-3-319-11936-6_14\">10.1007/978-3-319-11936-6_14</a>","ista":"Gupta A, Kovács L, Kragl B, Voronkov A. 2014. Extensional crisis and proving identity. 12th International Symposium on Automated Technology for Verification and Analysis. ATVA: Automated Technology for Verification and Analysis, LNCS, vol. 8837, 185–200.","ieee":"A. Gupta, L. Kovács, B. Kragl, and A. Voronkov, “Extensional crisis and proving identity,” in <i>12th International Symposium on Automated Technology for Verification and Analysis</i>, Sydney, Australia, 2014, vol. 8837, pp. 185–200.","apa":"Gupta, A., Kovács, L., Kragl, B., &#38; Voronkov, A. (2014). Extensional crisis and proving identity. In <i>12th International Symposium on Automated Technology for Verification and Analysis</i> (Vol. 8837, pp. 185–200). Sydney, Australia: Springer. <a href=\"https://doi.org/10.1007/978-3-319-11936-6_14\">https://doi.org/10.1007/978-3-319-11936-6_14</a>","chicago":"Gupta, Ashutosh, Laura Kovács, Bernhard Kragl, and Andrei Voronkov. “Extensional Crisis and Proving Identity.” In <i>12th International Symposium on Automated Technology for Verification and Analysis</i>, 8837:185–200. Springer, 2014. <a href=\"https://doi.org/10.1007/978-3-319-11936-6_14\">https://doi.org/10.1007/978-3-319-11936-6_14</a>.","short":"A. Gupta, L. Kovács, B. Kragl, A. Voronkov, in:, 12th International Symposium on Automated Technology for Verification and Analysis, Springer, 2014, pp. 185–200."},"publication":"12th International Symposium on Automated Technology for Verification and Analysis","publist_id":"5226","date_published":"2014-01-01T00:00:00Z","acknowledgement":"This research was supported in part by the Austrian National Research Network RiSE (S11410-N23).","file_date_updated":"2020-07-14T12:45:19Z","publisher":"Springer","has_accepted_license":"1","das_tickbox":"1"},{"author":[{"full_name":"Blanc, Régis","last_name":"Blanc","first_name":"Régis"},{"full_name":"Gupta, Ashutosh","last_name":"Gupta","first_name":"Ashutosh","id":"335E5684-F248-11E8-B48F-1D18A9856A87"},{"full_name":"Kovács, Laura","first_name":"Laura","last_name":"Kovács"},{"first_name":"Bernhard","last_name":"Kragl","id":"320FC952-F248-11E8-B48F-1D18A9856A87","orcid":"0000-0001-7745-9117","full_name":"Kragl, Bernhard"}],"quality_controlled":"1","month":"01","oa":1,"year":"2013","day":"14","date_created":"2018-12-11T11:56:29Z","series_title":"Lecture Notes in Computer Science","alternative_title":["LNCS"],"volume":8312,"publisher":"Springer","has_accepted_license":"1","publist_id":"4724","date_published":"2013-01-14T00:00:00Z","file_date_updated":"2020-07-14T12:45:34Z","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"}],"citation":{"ieee":"R. Blanc, A. Gupta, L. Kovács, and B. Kragl, “Tree interpolation in Vampire,” vol. 8312. Springer, pp. 173–181, 2013.","short":"R. Blanc, A. Gupta, L. Kovács, B. Kragl, 8312 (2013) 173–181.","chicago":"Blanc, Régis, Ashutosh Gupta, Laura Kovács, and Bernhard Kragl. “Tree Interpolation in Vampire.” Lecture Notes in Computer Science. Springer, 2013. <a href=\"https://doi.org/10.1007/978-3-642-45221-5_13\">https://doi.org/10.1007/978-3-642-45221-5_13</a>.","apa":"Blanc, R., Gupta, A., Kovács, L., &#38; Kragl, B. (2013). Tree interpolation in Vampire. Presented at the LPAR: Logic for Programming, Artificial Intelligence, and Reasoning, Stellenbosch, South Africa: Springer. <a href=\"https://doi.org/10.1007/978-3-642-45221-5_13\">https://doi.org/10.1007/978-3-642-45221-5_13</a>","ama":"Blanc R, Gupta A, Kovács L, Kragl B. Tree interpolation in Vampire. 2013;8312:173-181. doi:<a href=\"https://doi.org/10.1007/978-3-642-45221-5_13\">10.1007/978-3-642-45221-5_13</a>","mla":"Blanc, Régis, et al. <i>Tree Interpolation in Vampire</i>. Vol. 8312, Springer, 2013, pp. 173–81, doi:<a href=\"https://doi.org/10.1007/978-3-642-45221-5_13\">10.1007/978-3-642-45221-5_13</a>.","ista":"Blanc R, Gupta A, Kovács L, Kragl B. 2013. Tree interpolation in Vampire. 8312, 173–181."},"page":"173 - 181","user_id":"2DF688A6-F248-11E8-B48F-1D18A9856A87","project":[{"name":"Rigorous Systems Engineering","grant_number":"S 11407_N23","call_identifier":"FWF","_id":"25832EC2-B435-11E9-9278-68D0E5697425"}],"oa_version":"Submitted Version","type":"conference","department":[{"_id":"ToHe"}],"title":"Tree interpolation in Vampire","file":[{"file_id":"7858","creator":"dernst","file_size":279206,"relation":"main_file","date_updated":"2020-07-14T12:45:34Z","access_level":"open_access","checksum":"9cebaafca032e6769d273f393305c705","file_name":"2013_LPAR_Blanc.pdf","date_created":"2020-05-15T11:10:40Z","content_type":"application/pdf"}],"_id":"2237","ddc":["000"],"language":[{"iso":"eng"}],"article_processing_charge":"No","scopus_import":1,"doi":"10.1007/978-3-642-45221-5_13","intvolume":"      8312","date_updated":"2020-08-11T10:09:42Z","conference":{"end_date":"2013-12-19","name":"LPAR: Logic for Programming, Artificial Intelligence, and Reasoning","location":"Stellenbosch, South Africa","start_date":"2013-12-14"},"publication_status":"published","status":"public"},{"date_updated":"2024-10-09T20:55:17Z","corr_author":"1","abstract":[{"lang":"eng","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."}],"conference":{"end_date":"2013-09-24","name":"CMSB: Computational Methods in Systems Biology","location":"Klosterneuburg, Austria","start_date":"2013-09-22"},"publication_status":"published","status":"public","citation":{"mla":"Gupta, Ashutosh, and Thomas A. Henzinger, editors. <i>Computational Methods in Systems Biology</i>. Vol. 8130, Springer, 2013, doi:<a href=\"https://doi.org/10.1007/978-3-642-40708-6\">10.1007/978-3-642-40708-6</a>.","ama":"Gupta A, Henzinger TA, eds. <i>Computational Methods in Systems Biology</i>. Vol 8130. Springer; 2013. doi:<a href=\"https://doi.org/10.1007/978-3-642-40708-6\">10.1007/978-3-642-40708-6</a>","ista":"Gupta A, Henzinger TA eds. 2013. Computational Methods in Systems Biology, Springer,p.","ieee":"A. Gupta and T. A. Henzinger, Eds., <i>Computational Methods in Systems Biology</i>, vol. 8130. Springer, 2013.","apa":"Gupta, A., &#38; Henzinger, T. A. (Eds.). (2013). <i>Computational Methods in Systems Biology</i> (Vol. 8130). Presented at the CMSB: Computational Methods in Systems Biology, Klosterneuburg, Austria: Springer. <a href=\"https://doi.org/10.1007/978-3-642-40708-6\">https://doi.org/10.1007/978-3-642-40708-6</a>","short":"A. Gupta, T.A. Henzinger, eds., Computational Methods in Systems Biology, Springer, 2013.","chicago":"Gupta, Ashutosh, and Thomas A Henzinger, eds. <i>Computational Methods in Systems Biology</i>. Vol. 8130. Springer, 2013. <a href=\"https://doi.org/10.1007/978-3-642-40708-6\">https://doi.org/10.1007/978-3-642-40708-6</a>."},"doi":"10.1007/978-3-642-40708-6","intvolume":"      8130","publist_id":"4643","publication_identifier":{"isbn":["978-3-642-40707-9"]},"date_published":"2013-07-01T00:00:00Z","_id":"2288","publisher":"Springer","language":[{"iso":"eng"}],"department":[{"_id":"ToHe"}],"editor":[{"first_name":"Ashutosh","last_name":"Gupta","id":"335E5684-F248-11E8-B48F-1D18A9856A87","full_name":"Gupta, Ashutosh"},{"first_name":"Thomas A","last_name":"Henzinger","orcid":"0000−0002−2985−7724","id":"40876CD8-F248-11E8-B48F-1D18A9856A87","full_name":"Henzinger, Thomas A"}],"title":"Computational Methods in Systems Biology","volume":8130,"year":"2013","day":"01","oa_version":"None","date_created":"2018-12-11T11:56:47Z","alternative_title":["LNCS"],"type":"conference_editor","quality_controlled":"1","user_id":"2DF688A6-F248-11E8-B48F-1D18A9856A87","month":"07"},{"ec_funded":1,"project":[{"call_identifier":"FWF","name":"Rigorous Systems Engineering","grant_number":"S 11407_N23","_id":"25832EC2-B435-11E9-9278-68D0E5697425"},{"name":"Quantitative Reactive Modeling","grant_number":"267989","call_identifier":"FP7","_id":"25EE3708-B435-11E9-9278-68D0E5697425"}],"page":"77 - 84","user_id":"2DF688A6-F248-11E8-B48F-1D18A9856A87","arxiv":1,"department":[{"_id":"ToHe"}],"title":"Synthesizing multiple boolean functions using interpolation on a single proof","oa_version":"Preprint","type":"conference","_id":"1385","language":[{"iso":"eng"}],"date_updated":"2024-10-21T06:02:56Z","conference":{"end_date":"2013-10-23","name":"FMCAD: Formal Methods in Computer-Aided Design","location":"Portland, OR, United States","start_date":"2013-10-20"},"publication_status":"published","status":"public","scopus_import":"1","doi":"10.1109/FMCAD.2013.6679394","oa":1,"author":[{"full_name":"Hofferek, Georg","last_name":"Hofferek","first_name":"Georg"},{"id":"335E5684-F248-11E8-B48F-1D18A9856A87","last_name":"Gupta","first_name":"Ashutosh","full_name":"Gupta, Ashutosh"},{"full_name":"Könighofer, Bettina","first_name":"Bettina","last_name":"Könighofer"},{"full_name":"Jiang, Jie","first_name":"Jie","last_name":"Jiang"},{"full_name":"Bloem, Roderick","first_name":"Roderick","last_name":"Bloem"}],"quality_controlled":"1","month":"12","year":"2013","day":"11","date_created":"2018-12-11T11:51:43Z","publist_id":"5825","date_published":"2013-12-11T00:00:00Z","external_id":{"arxiv":["1308.4767"]},"acknowledgement":"This research was supported by the European Commission through project\r\nDIAMOND  (FP7-2009-IST-4-248613), and  QUAINT  (I774-N23),  ","publisher":"IEEE","abstract":[{"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.","lang":"eng"}],"citation":{"mla":"Hofferek, Georg, et al. “Synthesizing Multiple Boolean Functions Using Interpolation on a Single Proof.” <i>2013 Formal Methods in Computer-Aided Design</i>, IEEE, 2013, pp. 77–84, doi:<a href=\"https://doi.org/10.1109/FMCAD.2013.6679394\">10.1109/FMCAD.2013.6679394</a>.","ama":"Hofferek G, Gupta A, Könighofer B, Jiang J, Bloem R. Synthesizing multiple boolean functions using interpolation on a single proof. In: <i>2013 Formal Methods in Computer-Aided Design</i>. IEEE; 2013:77-84. doi:<a href=\"https://doi.org/10.1109/FMCAD.2013.6679394\">10.1109/FMCAD.2013.6679394</a>","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.","ieee":"G. Hofferek, A. Gupta, B. Könighofer, J. Jiang, and R. Bloem, “Synthesizing multiple boolean functions using interpolation on a single proof,” in <i>2013 Formal Methods in Computer-Aided Design</i>, Portland, OR, United States, 2013, pp. 77–84.","apa":"Hofferek, G., Gupta, A., Könighofer, B., Jiang, J., &#38; Bloem, R. (2013). Synthesizing multiple boolean functions using interpolation on a single proof. In <i>2013 Formal Methods in Computer-Aided Design</i> (pp. 77–84). Portland, OR, United States: IEEE. <a href=\"https://doi.org/10.1109/FMCAD.2013.6679394\">https://doi.org/10.1109/FMCAD.2013.6679394</a>","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.","chicago":"Hofferek, Georg, Ashutosh Gupta, Bettina Könighofer, Jie Jiang, and Roderick Bloem. “Synthesizing Multiple Boolean Functions Using Interpolation on a Single Proof.” In <i>2013 Formal Methods in Computer-Aided Design</i>, 77–84. IEEE, 2013. <a href=\"https://doi.org/10.1109/FMCAD.2013.6679394\">https://doi.org/10.1109/FMCAD.2013.6679394</a>."},"publication":"2013 Formal Methods in Computer-Aided Design","main_file_link":[{"url":"http://arxiv.org/abs/1308.4767","open_access":"1"}]},{"article_processing_charge":"No","language":[{"iso":"eng"}],"ddc":["005"],"file":[{"content_type":"application/pdf","date_created":"2018-12-18T13:13:33Z","file_name":"2013_CAV_Dragoi.pdf","checksum":"a901cc6b71db08b61c0d4c0cbacc6287","access_level":"open_access","date_updated":"2020-07-14T12:47:10Z","file_size":236480,"relation":"main_file","creator":"dernst","file_id":"5748"}],"_id":"5747","status":"public","publication_status":"published","conference":{"name":"CAV: Computer Aided Verification","end_date":"2013-07-19","start_date":"2013-07-13","location":"Saint Petersburg, Russia"},"date_updated":"2025-07-10T11:52:57Z","intvolume":"      8044","doi":"10.1007/978-3-642-39799-8_11","scopus_import":"1","project":[{"call_identifier":"FP7","name":"Quantitative Reactive Modeling","grant_number":"267989","_id":"25EE3708-B435-11E9-9278-68D0E5697425"},{"name":"Rigorous Systems Engineering","grant_number":"S 11407_N23","call_identifier":"FWF","_id":"25832EC2-B435-11E9-9278-68D0E5697425"}],"ec_funded":1,"user_id":"2DF688A6-F248-11E8-B48F-1D18A9856A87","page":"174-190","title":"Automatic Linearizability Proofs of Concurrent Objects with Cooperating Updates","pubrep_id":"195","department":[{"_id":"ToHe"}],"place":"Berlin, Heidelberg","type":"book_chapter","oa_version":"None","date_published":"2013-08-01T00:00:00Z","file_date_updated":"2020-07-14T12:47:10Z","publication_identifier":{"eissn":["1611-3349"],"eisbn":["9783642397998"],"issn":["0302-9743"],"isbn":["9783642397981"]},"has_accepted_license":"1","publisher":"Springer Berlin Heidelberg","citation":{"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.","mla":"Dragoi, Cezara, et al. “Automatic Linearizability Proofs of Concurrent Objects with Cooperating Updates.” <i>Computer Aided Verification</i>, vol. 8044, Springer Berlin Heidelberg, 2013, pp. 174–90, doi:<a href=\"https://doi.org/10.1007/978-3-642-39799-8_11\">10.1007/978-3-642-39799-8_11</a>.","ama":"Dragoi C, Gupta A, Henzinger TA. Automatic Linearizability Proofs of Concurrent Objects with Cooperating Updates. In: <i>Computer Aided Verification</i>. Vol 8044. CAV. Berlin, Heidelberg: Springer Berlin Heidelberg; 2013:174-190. doi:<a href=\"https://doi.org/10.1007/978-3-642-39799-8_11\">10.1007/978-3-642-39799-8_11</a>","apa":"Dragoi, C., Gupta, A., &#38; Henzinger, T. A. (2013). Automatic Linearizability Proofs of Concurrent Objects with Cooperating Updates. In <i>Computer Aided Verification</i> (Vol. 8044, pp. 174–190). Berlin, Heidelberg: Springer Berlin Heidelberg. <a href=\"https://doi.org/10.1007/978-3-642-39799-8_11\">https://doi.org/10.1007/978-3-642-39799-8_11</a>","chicago":"Dragoi, Cezara, Ashutosh Gupta, and Thomas A Henzinger. “Automatic Linearizability Proofs of Concurrent Objects with Cooperating Updates.” In <i>Computer Aided Verification</i>, 8044:174–90. CAV. Berlin, Heidelberg: Springer Berlin Heidelberg, 2013. <a href=\"https://doi.org/10.1007/978-3-642-39799-8_11\">https://doi.org/10.1007/978-3-642-39799-8_11</a>.","short":"C. Dragoi, A. Gupta, T.A. Henzinger, in:, Computer Aided Verification, Springer Berlin Heidelberg, Berlin, Heidelberg, 2013, pp. 174–190.","ieee":"C. Dragoi, A. Gupta, and T. A. Henzinger, “Automatic Linearizability Proofs of Concurrent Objects with Cooperating Updates,” in <i>Computer Aided Verification</i>, vol. 8044, Berlin, Heidelberg: Springer Berlin Heidelberg, 2013, pp. 174–190."},"publication":"Computer Aided Verification","oa":1,"month":"08","quality_controlled":"1","author":[{"last_name":"Dragoi","first_name":"Cezara","id":"2B2B5ED0-F248-11E8-B48F-1D18A9856A87","full_name":"Dragoi, Cezara"},{"full_name":"Gupta, Ashutosh","first_name":"Ashutosh","last_name":"Gupta","id":"335E5684-F248-11E8-B48F-1D18A9856A87"},{"last_name":"Henzinger","first_name":"Thomas A","orcid":"0000−0002−2985−7724","id":"40876CD8-F248-11E8-B48F-1D18A9856A87","full_name":"Henzinger, Thomas A"}],"volume":8044,"series_title":"CAV","date_created":"2018-12-18T13:10:21Z","day":"01","year":"2013"},{"oa":1,"quality_controlled":"1","author":[{"last_name":"Grebenshchikov","first_name":"Sergey","full_name":"Grebenshchikov, Sergey"},{"id":"335E5684-F248-11E8-B48F-1D18A9856A87","last_name":"Gupta","first_name":"Ashutosh","full_name":"Gupta, Ashutosh"},{"last_name":"Lopes","first_name":"Nuno P.","full_name":"Lopes, Nuno P."},{"last_name":"Popeea","first_name":"Corneliu","full_name":"Popeea, Corneliu"},{"first_name":"Andrey","last_name":"Rybalchenko","full_name":"Rybalchenko, Andrey"}],"month":"04","editor":[{"full_name":"Flanagan, Cormac","last_name":"Flanagan","first_name":"Cormac"},{"full_name":"König, Barbara","last_name":"König","first_name":"Barbara"}],"volume":7214,"day":"01","year":"2012","series_title":"LNCS","alternative_title":["LNCS"],"date_created":"2022-03-21T08:03:30Z","date_published":"2012-04-01T00:00:00Z","publication_identifier":{"issn":["0302-9743"],"isbn":["9783642287558"],"eisbn":["9783642287565"],"eissn":["1611-3349"]},"publisher":"Springer","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."}],"corr_author":"1","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.","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. <i>Tools and Algorithms for the Construction and Analysis of Systems</i>. Vol 7214. LNCS. Berlin, Heidelberg: Springer; 2012:549-551. doi:<a href=\"https://doi.org/10.1007/978-3-642-28756-5_46\">10.1007/978-3-642-28756-5_46</a>","mla":"Grebenshchikov, Sergey, et al. “HSF(C): A Software Verifier Based on Horn Clauses.” <i>Tools and Algorithms for the Construction and Analysis of Systems</i>, edited by Cormac Flanagan and Barbara König, vol. 7214, Springer, 2012, pp. 549–51, doi:<a href=\"https://doi.org/10.1007/978-3-642-28756-5_46\">10.1007/978-3-642-28756-5_46</a>.","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.","chicago":"Grebenshchikov, Sergey, Ashutosh Gupta, Nuno P. Lopes, Corneliu Popeea, and Andrey Rybalchenko. “HSF(C): A Software Verifier Based on Horn Clauses.” In <i>Tools and Algorithms for the Construction and Analysis of Systems</i>, edited by Cormac Flanagan and Barbara König, 7214:549–51. LNCS. Berlin, Heidelberg: Springer, 2012. <a href=\"https://doi.org/10.1007/978-3-642-28756-5_46\">https://doi.org/10.1007/978-3-642-28756-5_46</a>.","apa":"Grebenshchikov, S., Gupta, A., Lopes, N. P., Popeea, C., &#38; Rybalchenko, A. (2012). HSF(C): A software verifier based on Horn clauses. In C. Flanagan &#38; B. König (Eds.), <i>Tools and Algorithms for the Construction and Analysis of Systems</i> (Vol. 7214, pp. 549–551). Berlin, Heidelberg: Springer. <a href=\"https://doi.org/10.1007/978-3-642-28756-5_46\">https://doi.org/10.1007/978-3-642-28756-5_46</a>","ieee":"S. Grebenshchikov, A. Gupta, N. P. Lopes, C. Popeea, and A. Rybalchenko, “HSF(C): A software verifier based on Horn clauses,” in <i>Tools and Algorithms for the Construction and Analysis of Systems</i>, Tallinn, Estonia, 2012, vol. 7214, pp. 549–551."},"main_file_link":[{"open_access":"1","url":"https://doi.org/10.1007/978-3-642-28756-5_46"}],"publication":"Tools and Algorithms for the Construction and Analysis of Systems","page":"549-551","user_id":"2DF688A6-F248-11E8-B48F-1D18A9856A87","department":[{"_id":"ToHe"}],"title":"HSF(C): A software verifier based on Horn clauses","type":"conference","place":"Berlin, Heidelberg","oa_version":"Published Version","ddc":["000"],"_id":"10906","article_processing_charge":"No","language":[{"iso":"eng"}],"conference":{"start_date":"2012-03-24","location":"Tallinn, Estonia","end_date":"2012-04-01","name":"TACAS: Tools and Algorithms for the Construction and Analysis of Systems"},"date_updated":"2026-06-18T10:45:24Z","status":"public","publication_status":"published","doi":"10.1007/978-3-642-28756-5_46","scopus_import":"1","intvolume":"      7214"},{"language":[{"iso":"eng"}],"article_processing_charge":"No","_id":"5745","file":[{"date_created":"2018-12-18T13:07:35Z","content_type":"application/pdf","date_updated":"2020-07-14T12:47:10Z","access_level":"open_access","checksum":"68415837a315de3cc4d120f6019d752c","file_name":"2012_ATVA_Gupta.pdf","relation":"main_file","file_size":465502,"creator":"dernst","file_id":"5746"}],"ddc":["005"],"intvolume":"      7561","scopus_import":"1","doi":"10.1007/978-3-642-33386-6_10","publication_status":"published","status":"public","date_updated":"2025-04-15T07:56:27Z","conference":{"end_date":"2012-10-06","name":"ATVA: Automated Technology for Verification and Analysis","location":"Thiruvananthapuram, Kerala, India","start_date":"2012-10-03"},"user_id":"2DF688A6-F248-11E8-B48F-1D18A9856A87","page":"107-121","project":[{"call_identifier":"FP7","name":"Quantitative Reactive Modeling","grant_number":"267989","_id":"25EE3708-B435-11E9-9278-68D0E5697425"}],"ec_funded":1,"oa_version":"Submitted Version","type":"conference","title":"Improved single pass algorithms for resolution proof reduction","department":[{"_id":"ToHe"}],"pubrep_id":"180","has_accepted_license":"1","publisher":"Springer Nature","OA_place":"repository","publication_identifier":{"eissn":["1611-3349"],"eisbn":["9783642333866"],"isbn":["9783642333859"],"issn":["0302-9743"]},"date_published":"2012-09-28T00:00:00Z","acknowledgement":"This work was supported by the ERC Advanced Investigator grant on Quantitative\r\nReactive Modeling (QUAREM).","file_date_updated":"2020-07-14T12:47:10Z","publication":"10th International Symposium on Automated Technology for Verification and Analysis","citation":{"ieee":"A. Gupta, “Improved single pass algorithms for resolution proof reduction,” in <i>10th International Symposium on Automated Technology for Verification and Analysis</i>, Thiruvananthapuram, Kerala, India, 2012, vol. 7561, pp. 107–121.","apa":"Gupta, A. (2012). Improved single pass algorithms for resolution proof reduction. In <i>10th International Symposium on Automated Technology for Verification and Analysis</i> (Vol. 7561, pp. 107–121). Thiruvananthapuram, Kerala, India: Springer Nature. <a href=\"https://doi.org/10.1007/978-3-642-33386-6_10\">https://doi.org/10.1007/978-3-642-33386-6_10</a>","short":"A. Gupta, in:, 10th International Symposium on Automated Technology for Verification and Analysis, Springer Nature, 2012, pp. 107–121.","chicago":"Gupta, Ashutosh. “Improved Single Pass Algorithms for Resolution Proof Reduction.” In <i>10th International Symposium on Automated Technology for Verification and Analysis</i>, 7561:107–21. Springer Nature, 2012. <a href=\"https://doi.org/10.1007/978-3-642-33386-6_10\">https://doi.org/10.1007/978-3-642-33386-6_10</a>.","mla":"Gupta, Ashutosh. “Improved Single Pass Algorithms for Resolution Proof Reduction.” <i>10th International Symposium on Automated Technology for Verification and Analysis</i>, vol. 7561, Springer Nature, 2012, pp. 107–21, doi:<a href=\"https://doi.org/10.1007/978-3-642-33386-6_10\">10.1007/978-3-642-33386-6_10</a>.","ama":"Gupta A. Improved single pass algorithms for resolution proof reduction. In: <i>10th International Symposium on Automated Technology for Verification and Analysis</i>. Vol 7561. Springer Nature; 2012:107-121. doi:<a href=\"https://doi.org/10.1007/978-3-642-33386-6_10\">10.1007/978-3-642-33386-6_10</a>","ista":"Gupta A. 2012. Improved single pass algorithms for resolution proof reduction. 10th International Symposium on Automated Technology for Verification and Analysis. ATVA: Automated Technology for Verification and Analysis, LNCS, vol. 7561, 107–121."},"corr_author":"1","abstract":[{"text":"Unsatisfiability proofs find many applications in verification. Today, many SAT solvers are capable of producing resolution proofs of unsatisfiability. For efficiency smaller proofs are preferred over bigger ones. The solvers apply proof reduction methods to remove redundant parts of the proofs while and after generating the proofs. One method of reducing resolution proofs is redundant resolution reduction, i.e., removing repeated pivots in the paths of resolution proofs (aka Pivot recycle). The known single pass algorithm only tries to remove redundancies in the parts of the proof that are trees. In this paper, we present three modifications to improve the algorithm such that the redundancies can be found in the parts of the proofs that are DAGs. The first modified algorithm covers greater number of redundancies as compared to the known algorithm without incurring any additional cost. The second modified algorithm covers even greater number of the redundancies but it may have longer run times. Our third modified algorithm is parametrized and can trade off between run times and the coverage of the redundancies. We have implemented our algorithms in OpenSMT and applied them on unsatisfiability proofs of 198 examples from plain MUS track of SAT11 competition. The first and second algorithm additionally remove 0.89% and 10.57% of clauses respectively as compared to the original algorithm. For certain value of the parameter, the third algorithm removes almost as many clauses as the second algorithm but is significantly faster.","lang":"eng"}],"month":"09","author":[{"full_name":"Gupta, Ashutosh","id":"335E5684-F248-11E8-B48F-1D18A9856A87","last_name":"Gupta","first_name":"Ashutosh"}],"quality_controlled":"1","oa":1,"date_created":"2018-12-18T13:01:46Z","alternative_title":["LNCS"],"year":"2012","day":"28","volume":7561},{"title":"Delayed continuous time Markov chains for genetic regulatory circuits","department":[{"_id":"CaGu"},{"_id":"ToHe"}],"type":"conference","oa_version":"None","project":[{"call_identifier":"FP7","name":"Quantitative Reactive Modeling","grant_number":"267989","_id":"25EE3708-B435-11E9-9278-68D0E5697425"}],"ec_funded":1,"user_id":"3E5EF7F0-F248-11E8-B48F-1D18A9856A87","page":"294 - 309","status":"public","publication_status":"published","conference":{"location":"Berkeley, CA, USA","start_date":"2012-07-07","end_date":"2012-07-13","name":"CAV: Computer Aided Verification"},"date_updated":"2024-10-09T20:54:47Z","doi":"10.1007/978-3-642-31424-7_24","scopus_import":1,"language":[{"iso":"eng"}],"_id":"3136","volume":"7358 ","alternative_title":["LNCS"],"date_created":"2018-12-11T12:01:36Z","day":"01","year":"2012","month":"07","quality_controlled":"1","author":[{"full_name":"Guet, Calin C","first_name":"Calin C","last_name":"Guet","orcid":"0000-0001-6220-2052","id":"47F8433E-F248-11E8-B48F-1D18A9856A87"},{"full_name":"Gupta, Ashutosh","last_name":"Gupta","first_name":"Ashutosh","id":"335E5684-F248-11E8-B48F-1D18A9856A87"},{"id":"40876CD8-F248-11E8-B48F-1D18A9856A87","orcid":"0000−0002−2985−7724","last_name":"Henzinger","first_name":"Thomas A","full_name":"Henzinger, Thomas A"},{"last_name":"Mateescu","first_name":"Maria","id":"3B43276C-F248-11E8-B48F-1D18A9856A87","full_name":"Mateescu, Maria"},{"id":"4C7638DA-F248-11E8-B48F-1D18A9856A87","last_name":"Sezgin","first_name":"Ali","full_name":"Sezgin, Ali"}],"citation":{"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.","mla":"Guet, Calin C., et al. <i>Delayed Continuous Time Markov Chains for Genetic Regulatory Circuits</i>. Vol. 7358, Springer, 2012, pp. 294–309, doi:<a href=\"https://doi.org/10.1007/978-3-642-31424-7_24\">10.1007/978-3-642-31424-7_24</a>.","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:<a href=\"https://doi.org/10.1007/978-3-642-31424-7_24\">10.1007/978-3-642-31424-7_24</a>","apa":"Guet, C. C., Gupta, A., Henzinger, T. A., Mateescu, M., &#38; 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. <a href=\"https://doi.org/10.1007/978-3-642-31424-7_24\">https://doi.org/10.1007/978-3-642-31424-7_24</a>","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. <a href=\"https://doi.org/10.1007/978-3-642-31424-7_24\">https://doi.org/10.1007/978-3-642-31424-7_24</a>.","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."},"abstract":[{"lang":"eng","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."}],"corr_author":"1","date_published":"2012-07-01T00:00:00Z","acknowledgement":"This work was supported by the ERC Advanced Investigator grant on Quantitative Reactive Modeling (QUAREM) and by the Swiss National Science Foundation.","publist_id":"3561","publisher":"Springer"},{"language":[{"iso":"eng"}],"_id":"3264","publication_status":"published","status":"public","date_updated":"2024-10-21T06:03:01Z","conference":{"start_date":"2011-12-05","location":"Kenting, Taiwan","name":"APLAS: Asian Symposium on Programming Languages and Systems","end_date":"2011-12-07"},"intvolume":"      7078","doi":"10.1007/978-3-642-25318-8_16","scopus_import":"1","project":[{"_id":"25832EC2-B435-11E9-9278-68D0E5697425","call_identifier":"FWF","grant_number":"S 11407_N23","name":"Rigorous Systems Engineering"},{"call_identifier":"FP7","name":"Quantitative Reactive Modeling","grant_number":"267989","_id":"25EE3708-B435-11E9-9278-68D0E5697425"}],"ec_funded":1,"user_id":"4435EBFC-F248-11E8-B48F-1D18A9856A87","page":"188 - 203","title":"Solving recursion-free Horn clauses over LI+UIF","department":[{"_id":"ToHe"}],"oa_version":"None","type":"conference","date_published":"2011-12-05T00:00:00Z","publist_id":"3383","publisher":"Springer","citation":{"short":"A. Gupta, C. Popeea, A. Rybalchenko, in:, H. Yang (Ed.), Springer, 2011, pp. 188–203.","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. <a href=\"https://doi.org/10.1007/978-3-642-25318-8_16\">https://doi.org/10.1007/978-3-642-25318-8_16</a>.","apa":"Gupta, A., Popeea, C., &#38; 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. <a href=\"https://doi.org/10.1007/978-3-642-25318-8_16\">https://doi.org/10.1007/978-3-642-25318-8_16</a>","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.","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.","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:<a href=\"https://doi.org/10.1007/978-3-642-25318-8_16\">10.1007/978-3-642-25318-8_16</a>","mla":"Gupta, Ashutosh, et al. <i>Solving Recursion-Free Horn Clauses over LI+UIF</i>. Edited by Hongseok Yang, vol. 7078, Springer, 2011, pp. 188–203, doi:<a href=\"https://doi.org/10.1007/978-3-642-25318-8_16\">10.1007/978-3-642-25318-8_16</a>."},"abstract":[{"lang":"eng","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."}],"month":"12","author":[{"full_name":"Gupta, Ashutosh","first_name":"Ashutosh","last_name":"Gupta","id":"335E5684-F248-11E8-B48F-1D18A9856A87"},{"full_name":"Popeea, Corneliu","last_name":"Popeea","first_name":"Corneliu"},{"full_name":"Rybalchenko, Andrey","first_name":"Andrey","last_name":"Rybalchenko"}],"quality_controlled":"1","volume":7078,"editor":[{"first_name":"Hongseok","last_name":"Yang","full_name":"Yang, Hongseok"}],"date_created":"2018-12-11T12:02:20Z","alternative_title":["LNCS"],"year":"2011","day":"05"},{"extern":1,"month":"01","quality_controlled":0,"author":[{"last_name":"Gupta","first_name":"Ashutosh","id":"335E5684-F248-11E8-B48F-1D18A9856A87","full_name":"Ashutosh Gupta"},{"last_name":"Henzinger","first_name":"Thomas A","id":"40876CD8-F248-11E8-B48F-1D18A9856A87","orcid":"0000−0002−2985−7724","full_name":"Thomas Henzinger"},{"last_name":"Majumdar","first_name":"Ritankar","full_name":"Majumdar, Ritankar S"},{"last_name":"Rybalchenko","first_name":"Andrey","full_name":"Rybalchenko, Andrey"},{"full_name":"Xu, Ru-Gang","first_name":"Ru","last_name":"Xu"}],"page":"147 - 158","title":"Proving non-termination","type":"conference","date_created":"2018-12-11T12:09:17Z","day":"01","year":"2008","date_published":"2008-01-01T00:00:00Z","publist_id":"208","publisher":"ACM","_id":"4521","status":"public","citation":{"ista":"Gupta A, Henzinger TA, Majumdar R, Rybalchenko A, Xu R. 2008. Proving non-termination. POPL: Principles of Programming Languages, 147–158.","ama":"Gupta A, Henzinger TA, Majumdar R, Rybalchenko A, Xu R. Proving non-termination. In: ACM; 2008:147-158. doi:<a href=\"https://doi.org/10.1145/1328438.1328459\">10.1145/1328438.1328459</a>","mla":"Gupta, Ashutosh, et al. <i>Proving Non-Termination</i>. ACM, 2008, pp. 147–58, doi:<a href=\"https://doi.org/10.1145/1328438.1328459\">10.1145/1328438.1328459</a>.","short":"A. Gupta, T.A. Henzinger, R. Majumdar, A. Rybalchenko, R. Xu, in:, ACM, 2008, pp. 147–158.","chicago":"Gupta, Ashutosh, Thomas A Henzinger, Ritankar Majumdar, Andrey Rybalchenko, and Ru Xu. “Proving Non-Termination,” 147–58. ACM, 2008. <a href=\"https://doi.org/10.1145/1328438.1328459\">https://doi.org/10.1145/1328438.1328459</a>.","apa":"Gupta, A., Henzinger, T. A., Majumdar, R., Rybalchenko, A., &#38; Xu, R. (2008). Proving non-termination (pp. 147–158). Presented at the POPL: Principles of Programming Languages, ACM. <a href=\"https://doi.org/10.1145/1328438.1328459\">https://doi.org/10.1145/1328438.1328459</a>","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."},"publication_status":"published","conference":{"name":"POPL: Principles of Programming Languages"},"abstract":[{"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.","lang":"eng"}],"date_updated":"2021-01-12T07:59:25Z","main_file_link":[{"open_access":"0","url":"http://pub.ist.ac.at/%7Etah/Publications/proving_non-termination.pdf"}],"doi":"10.1145/1328438.1328459"}]