{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,5,21]],"date-time":"2026-05-21T09:07:53Z","timestamp":1779354473457,"version":"3.51.4"},"publisher-location":"Cham","reference-count":32,"publisher":"Springer Nature Switzerland","isbn-type":[{"value":"9783032267511","type":"print"},{"value":"9783032267528","type":"electronic"}],"license":[{"start":{"date-parts":[[2026,1,1]],"date-time":"2026-01-01T00:00:00Z","timestamp":1767225600000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/www.springernature.com\/gp\/researchers\/text-and-data-mining"},{"start":{"date-parts":[[2026,1,1]],"date-time":"2026-01-01T00:00:00Z","timestamp":1767225600000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.springernature.com\/gp\/researchers\/text-and-data-mining"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2026]]},"DOI":"10.1007\/978-3-032-26752-8_1","type":"book-chapter","created":{"date-parts":[[2026,5,21]],"date-time":"2026-05-21T08:13:08Z","timestamp":1779351188000},"page":"3-21","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":0,"title":["Counterexample-Guided Interval Weakening"],"prefix":"10.1007","author":[{"ORCID":"https:\/\/orcid.org\/0009-0009-8910-5899","authenticated-orcid":false,"given":"Ben M.","family":"Andrew","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0003-1426-1896","authenticated-orcid":false,"given":"Louise A.","family":"Dennis","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-0875-3862","authenticated-orcid":false,"given":"Michael","family":"Fisher","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0001-7708-3877","authenticated-orcid":false,"given":"Marie","family":"Farrell","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2026,5,22]]},"reference":[{"key":"1_CR1","doi-asserted-by":"crossref","unstructured":"Aarts, F., Heidarian, F., Kuppens, H., Olsen, P., Vaandrager, F.: Automata learning through counterexample guided abstraction refinement. In: Formal Methods (2012)","DOI":"10.1007\/978-3-642-32759-9_4"},{"key":"1_CR2","doi-asserted-by":"crossref","unstructured":"Abreu, A., Macedo, N., Mendes, A.: Exploring automatic specification repair in dafny programs. In: International Conference on Automated Software Engineering Workshops (2023)","DOI":"10.1109\/ASEW60602.2023.00019"},{"key":"1_CR3","unstructured":"Akshay, S., Contractor, P., Gastin, P., Govind, R., Srivathsan, B.: Efficient verification of metric temporal properties with past in pointwise semantics. https:\/\/arxiv.org\/abs\/2510.14699v1. 2025"},{"key":"1_CR4","doi-asserted-by":"crossref","unstructured":"Alur, R., et al.: Syntax-guided synthesis. In: Formal Methods in Computer-Aided Design (2013)","DOI":"10.1109\/FMCAD.2013.6679385"},{"key":"1_CR5","doi-asserted-by":"crossref","unstructured":"Alur, R., Henzinger, T.A.: Real-time logics: complexity and expressiveness. Inf. Comput. 104, 1 (1993)","DOI":"10.1006\/inco.1993.1025"},{"key":"1_CR6","doi-asserted-by":"crossref","unstructured":"Alur, R., Moarref, S., Topcu, U.: Counter-strategy guided refinement of GR(1) temporal logic specifications. In: Formal Methods in Computer-Aided Design (2013)","DOI":"10.1109\/FMCAD.2013.6679387"},{"key":"1_CR7","doi-asserted-by":"crossref","unstructured":"Andrew, B.M.: Weakening goals in logical specifications. In: Rigorous State-Based Methods (2026)","DOI":"10.1007\/978-3-031-94533-5_22"},{"key":"1_CR8","unstructured":"Baier, C., Katoen, J.-P.: Principles of model checking (2008)"},{"key":"1_CR9","doi-asserted-by":"crossref","unstructured":"Bourbouh, H., et al.: Integrating formal verification and assurance: an inspection rover case study. In: NASA Formal Methods (2021)","DOI":"10.1007\/978-3-030-76384-8_4"},{"key":"1_CR10","doi-asserted-by":"crossref","unstructured":"Brihaye, T., Geeraerts, G., Ho, H.-M., Milchior, A., Monmege, B.: Efficient algorithms and tools for MITL model-checking and synthesis. In: International Conference on Engineering of Complex Computer Systems (2018)","DOI":"10.1109\/ICECCS2018.2018.00027"},{"key":"1_CR11","doi-asserted-by":"crossref","unstructured":"Brizzio, M., Cordy, M., Papadakis, M., S\u00e1nchez, C., Aguirre, N., Degiovanni, R.: Automated repair of unrealisable LTL specifications guided by model counting. In: Genetic and Evolutionary Computation Conference (2023)","DOI":"10.1145\/3583131.3590454"},{"key":"1_CR12","doi-asserted-by":"crossref","unstructured":"Cavada, R., et al.: The NUXMV symbolic model checker. In: Computer Aided Verification (2014)","DOI":"10.1007\/978-3-319-08867-9_22"},{"key":"1_CR13","doi-asserted-by":"crossref","unstructured":"Cerqueira, J., Cunha, A., Macedo, N.: Timely specification repair for alloy 6. In: Software Engineering and Formal Methods (2022)","DOI":"10.1007\/978-3-031-17108-6_18"},{"key":"1_CR14","doi-asserted-by":"crossref","unstructured":"Clarke, E., Grumberg, O., Jha, S., Lu, Y., Veith, H.: Counterexample-guided abstraction refinement. In: Computer Aided Verification (2000)","DOI":"10.1007\/10722167_15"},{"key":"1_CR15","doi-asserted-by":"crossref","unstructured":"Clarke, E., Kroening, D., Ouaknine, J., Strichman, O.: Completeness and complexity of bounded model checking. In: Verification, Model Checking, and Abstract Interpretation (2004)","DOI":"10.1007\/978-3-540-24622-0_9"},{"key":"1_CR16","doi-asserted-by":"crossref","unstructured":"Cobleigh, J.M., Giannakopoulou, D., P\u0103s\u0103reanu, C.S.: Learning assumptions for compositional verification. In: Tools and Algorithms for the Construction and Analysis of Systems (2003)","DOI":"10.1007\/3-540-36577-X_24"},{"key":"1_CR17","doi-asserted-by":"crossref","unstructured":"Farrell, M., Luckcuck, M., Monahan, R., Reynolds, C., Sheridan, O.: FRETting and formal modelling: a mechanical lung ventilator. In: Rigorous State-Based Methods (2024)","DOI":"10.1007\/978-3-031-63790-2_28"},{"key":"1_CR18","doi-asserted-by":"crossref","unstructured":"Farrell, M., Luckcuck, M., Sheridan, O., Monahan, R.: FRETting about requirements: formalised requirements for an aircraft engine controller. In: Requirements Engineering: Foundation for Software Quality (2022)","DOI":"10.1007\/978-3-030-98464-9_9"},{"key":"1_CR19","doi-asserted-by":"crossref","unstructured":"Farrell, M., Mavrakis, N., Ferrando, A., Dixon, C., Gao, Y.: Formal modelling and runtime verification of autonomous grasping for active debris removal. In: Frontiers in Robotics and AI, vol. 8 (2022)","DOI":"10.3389\/frobt.2021.639282"},{"key":"1_CR20","doi-asserted-by":"crossref","unstructured":"Gazzola, L., Micucci, D., Mariani, L.: Automatic software repair: a survey. In: International Conference on Software Engineering (2018)","DOI":"10.1145\/3180155.3182526"},{"key":"1_CR21","unstructured":"Giannakopoulou, D., Pressburger, T., Mavridou, A., Rhein, J., Schumann, J., Shi, N.: Formal requirements elicitation with FRET. In: International Working Conference on Requirements Engineering: Foundation for Software Quality (2020)"},{"key":"1_CR22","doi-asserted-by":"crossref","unstructured":"Giannakopoulou, D., Pressburger, T., Mavridou, A., Schumann, J.: Automated formalization of structured natural language requirements. In: Information and Software Technology, vol. 137 (2021)","DOI":"10.1016\/j.infsof.2021.106590"},{"key":"1_CR23","doi-asserted-by":"crossref","unstructured":"Holzmann, G.J.: The model checker SPIN. IEEE Trans. Softw. Eng. 23, 5 (1997)","DOI":"10.1109\/32.588521"},{"key":"1_CR24","doi-asserted-by":"crossref","unstructured":"Howar, F., Steffen, B., Merten, M.: Automata learning with automated alphabet abstraction refinement. In: Verification, Model Checking, and Abstract Interpretation (2011)","DOI":"10.1007\/978-3-642-18275-4_19"},{"key":"1_CR25","unstructured":"ISO. Particular requirements for basic safety and essential performance of critical care ventilators. 80601-2-12 (2023)"},{"key":"1_CR26","doi-asserted-by":"crossref","unstructured":"Koymans, R.: Specifying real-time properties with metric temporal logic. Real-Time Syst. 2, 4 (1990)","DOI":"10.1007\/BF01995674"},{"key":"1_CR27","doi-asserted-by":"crossref","unstructured":"Liu, W., Winfield, A.F.T.: Modeling and optimization of adaptive foraging in swarm robotic systems. Int. J. Robot. Res. 29, 14 (2010)","DOI":"10.1177\/0278364910375139"},{"key":"1_CR28","doi-asserted-by":"crossref","unstructured":"Maoz, S., Ringert, J.O., Shalom, R.: Symbolic repairs for GR(1) specifications. In: International Conference on Software Engineering (2019)","DOI":"10.1109\/ICSE.2019.00106"},{"key":"1_CR29","doi-asserted-by":"crossref","unstructured":"Mavridou, A., et al.: The Ten lockheed martin cyber-physical challenges: formalized, analyzed, and explained. In: International Requirements Engineering Conference (2020)","DOI":"10.1109\/RE48521.2020.00040"},{"key":"1_CR30","doi-asserted-by":"crossref","unstructured":"Pressburger, T., Katis, A., Dutle, A., Mavridou, A.: Authoring, analyzing, and monitoring requirements for a lift-plus-cruise aircraft. In: Requirements Engineering: Foundation for Software Quality (2023)","DOI":"10.1007\/978-3-031-29786-1_21"},{"key":"1_CR31","doi-asserted-by":"crossref","unstructured":"Sheridan, O., Becker, L.B., Farrell, M., Luckcuck, M., Monahan, R.: Sharper specs for smarter drones: formalising requirements with FRET. In: Requirements Engineering: Foundation for Software Quality (2025)","DOI":"10.1007\/978-3-031-88531-0_25"},{"key":"1_CR32","doi-asserted-by":"crossref","unstructured":"V\u00e1zquez, G., Mavridou, A., Farrell, M., Pressburger, T., Calinescu, R.: Robotics: A New mission for FRET requirements. In: NASA Formal Methods (2024)","DOI":"10.1007\/978-3-031-60698-4_22"}],"container-title":["Lecture Notes in Computer Science","Rigorous State-Based Methods"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-032-26752-8_1","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2026,5,21]],"date-time":"2026-05-21T08:13:19Z","timestamp":1779351199000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/978-3-032-26752-8_1"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2026]]},"ISBN":["9783032267511","9783032267528"],"references-count":32,"URL":"https:\/\/doi.org\/10.1007\/978-3-032-26752-8_1","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[2026]]},"assertion":[{"value":"22 May 2026","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}},{"value":"ABZ","order":1,"name":"conference_acronym","label":"Conference Acronym","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"International Conference on Rigorous State-Based Methods","order":2,"name":"conference_name","label":"Conference Name","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Tokyo","order":3,"name":"conference_city","label":"Conference City","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Japan","order":4,"name":"conference_country","label":"Conference Country","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"2026","order":5,"name":"conference_year","label":"Conference Year","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"18 May 2026","order":7,"name":"conference_start_date","label":"Conference Start Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"20 May 2026","order":8,"name":"conference_end_date","label":"Conference End Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"12","order":9,"name":"conference_number","label":"Conference Number","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"abz2026","order":10,"name":"conference_id","label":"Conference ID","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"https:\/\/abz-conf.org\/site\/2026\/","order":11,"name":"conference_url","label":"Conference URL","group":{"name":"ConferenceInfo","label":"Conference Information"}}]}}