{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,11]],"date-time":"2024-09-11T08:39:26Z","timestamp":1726043966128},"publisher-location":"Cham","reference-count":31,"publisher":"Springer International Publishing","isbn-type":[{"type":"print","value":"9783030304454"},{"type":"electronic","value":"9783030304461"}],"license":[{"start":{"date-parts":[[2019,1,1]],"date-time":"2019-01-01T00:00:00Z","timestamp":1546300800000},"content-version":"tdm","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2019]]},"DOI":"10.1007\/978-3-030-30446-1_28","type":"book-chapter","created":{"date-parts":[[2019,9,8]],"date-time":"2019-09-08T19:03:18Z","timestamp":1567969398000},"page":"532-548","update-policy":"http:\/\/dx.doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":1,"title":["Partially Bounded Context-Aware Verification"],"prefix":"10.1007","author":[{"given":"Luka","family":"Le Roux","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Ciprian","family":"Teodorov","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2019,9,9]]},"reference":[{"key":"28_CR1","doi-asserted-by":"publisher","unstructured":"Barnat, J., Brim, L., Simecek, P.: Cluster-based I\/O-efficient LTL model checking. In: Proceedings of the 2009 IEEE\/ACM International Conference on Automated Software Engineering, pp. 635\u2013639. ASE 2009. IEEE Computer Society, Washington (2009). https:\/\/doi.org\/10.1109\/ASE.2009.32","DOI":"10.1109\/ASE.2009.32"},{"key":"28_CR2","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"232","DOI":"10.1007\/BFb0020949","volume-title":"Hybrid Systems III","author":"J Bengtsson","year":"1996","unstructured":"Bengtsson, J., Larsen, K., Larsson, F., Pettersson, P., Yi, W.: UPPAAL \u2014 a tool suite for automatic verification of real-time systems. In: Alur, R., Henzinger, T.A., Sontag, E.D. (eds.) HS 1995. LNCS, vol. 1066, pp. 232\u2013243. Springer, Heidelberg (1996). https:\/\/doi.org\/10.1007\/BFb0020949"},{"key":"28_CR3","unstructured":"Berthomieu, B., et al.: Fiacre: an intermediate language for model verification in the topcased environment. In: European Congress on Embedded Real-Time Software (ERTS). SEE, Toulouse, France (Jan 2008). https:\/\/hal.inria.fr\/inria-00262442"},{"key":"28_CR4","series-title":"Communications in Computer and Information Science","doi-asserted-by":"publisher","first-page":"110","DOI":"10.1007\/978-3-319-07512-9_8","volume-title":"ABZ 2014: The Landing Gear Case Study","author":"B Berthomieu","year":"2014","unstructured":"Berthomieu, B., Dal Zilio, S., Fronc, \u0141.: Model-checking real-time properties of an aircraft landing gear system using fiacre. In: Boniol, F., Wiels, V., Ait Ameur, Y., Schewe, K.-D. (eds.) ABZ 2014. CCIS, vol. 433, pp. 110\u2013125. Springer, Cham (2014). https:\/\/doi.org\/10.1007\/978-3-319-07512-9_8"},{"key":"28_CR5","doi-asserted-by":"crossref","first-page":"157","DOI":"10.1002\/9781118569535.ch8","volume-title":"Embedded Systems","author":"Frederic Boniol","year":"2013","unstructured":"Boniol, F., Dhaussy, P., Le Roux, L., Roger, J.C.: Model-based analysis. In: Embedded systems, Analysis and Modeling with SysML, UML and AADL, pp. 157\u2013184. Wiley (May 2013). https:\/\/hal.archives-ouvertes.fr\/hal-00843139"},{"key":"28_CR6","series-title":"Communications in Computer and Information Science","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1007\/978-3-319-07512-9_1","volume-title":"ABZ 2014: The Landing Gear Case Study","author":"F Boniol","year":"2014","unstructured":"Boniol, F., Wiels, V.: The landing gear system case study. In: Boniol, F., Wiels, V., Ait Ameur, Y., Schewe, K.-D. (eds.) ABZ 2014. CCIS, vol. 433, pp. 1\u201318. Springer, Cham (2014). https:\/\/doi.org\/10.1007\/978-3-319-07512-9_1"},{"issue":"2","key":"28_CR7","doi-asserted-by":"publisher","first-page":"142","DOI":"10.1016\/0890-5401(92)90017-A","volume":"98","author":"J Burch","year":"1992","unstructured":"Burch, J., Clarke, E., McMillan, K., Dill, D., Hwang, L.: Symbolic model checking: $$10^{20}$$ states and beyond. Inf. Comput. 98(2), 142\u2013170 (1992). https:\/\/doi.org\/10.1016\/0890-5401(92)90017-A","journal-title":"Inf. Comput."},{"issue":"2","key":"28_CR8","doi-asserted-by":"publisher","first-page":"244","DOI":"10.1145\/5397.5399","volume":"8","author":"EM Clarke","year":"1986","unstructured":"Clarke, E.M., Emerson, E.A., Sistla, A.P.: Automatic verification of finite-state concurrent systems using temporal logic specifications. ACM Trans. Program. Lang. Syst. 8(2), 244\u2013263 (1986). https:\/\/doi.org\/10.1145\/5397.5399","journal-title":"ACM Trans. Program. Lang. Syst."},{"issue":"1","key":"28_CR9","doi-asserted-by":"publisher","first-page":"77","DOI":"10.1007\/BF00625969","volume":"9","author":"EM Clarke","year":"1996","unstructured":"Clarke, E.M., Enders, R., Filkorn, T., Jha, S.: Exploiting symmetry in temporal logic model checking. Formal Methods Syst. Des. 9(1), 77\u2013104 (1996). https:\/\/doi.org\/10.1007\/BF00625969","journal-title":"Formal Methods Syst. Des."},{"issue":"1","key":"28_CR10","doi-asserted-by":"publisher","first-page":"7","DOI":"10.1023\/A:1011276507260","volume":"19","author":"E Clarke","year":"2001","unstructured":"Clarke, E., Biere, A., Raimi, R., Zhu, Y.: Bounded model checking using satisfiability solving. Formal Methods Syst. Des. 19(1), 7\u201334 (2001). https:\/\/doi.org\/10.1023\/A:1011276507260","journal-title":"Formal Methods Syst. Des."},{"key":"28_CR11","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"52","DOI":"10.1007\/BFb0025774","volume-title":"Logics of Programs","author":"EM Clarke","year":"1982","unstructured":"Clarke, E.M., Emerson, E.A.: Design and synthesis of synchronization skeletons using branching time temporal logic. In: Kozen, D. (ed.) Logic of Programs 1981. LNCS, vol. 131, pp. 52\u201371. Springer, Heidelberg (1982). https:\/\/doi.org\/10.1007\/BFb0025774"},{"key":"28_CR12","doi-asserted-by":"publisher","unstructured":"Dhaussy, P., Boniol, F., Landel, E.: Using context descriptions and property definition patterns for software formal verification. In: Proceedings of the 2008 IEEE International Conference on Software Testing Verification and Validation Workshop, pp. 89\u201396. ICSTW 2008. IEEE Computer Society, Washington (2008). https:\/\/doi.org\/10.1109\/ICSTW.2008.52","DOI":"10.1109\/ICSTW.2008.52"},{"key":"28_CR13","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1155\/2012\/547157","volume":"2012","author":"Philippe Dhaussy","year":"2012","unstructured":"Dhaussy, P., Boniol, F., Roger, J.C., Le Roux, L.: Improving model checking with context modelling. In: Advances in Software Engineering 2012, ID 547157, 13 p (October 2012). https:\/\/doi.org\/10.1155\/2012\/547157","journal-title":"Advances in Software Engineering"},{"key":"28_CR14","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"438","DOI":"10.1007\/978-3-642-04425-0_34","volume-title":"Model Driven Engineering Languages and Systems","author":"P Dhaussy","year":"2009","unstructured":"Dhaussy, P., Pillain, P.-Y., Creff, S., Raji, A., Le Traon, Y., Baudry, B.: Evaluating context descriptions and property definition patterns for software formal validation. In: Sch\u00fcrr, A., Selic, B. (eds.) MODELS 2009. LNCS, vol. 5795, pp. 438\u2013452. Springer, Heidelberg (2009). https:\/\/doi.org\/10.1007\/978-3-642-04425-0_34"},{"key":"28_CR15","series-title":"Communications in Computer and Information Science","doi-asserted-by":"publisher","first-page":"52","DOI":"10.1007\/978-3-319-07512-9_4","volume-title":"ABZ 2014: The Landing Gear Case Study","author":"P Dhaussy","year":"2014","unstructured":"Dhaussy, P., Teodorov, C.: Context-aware verification of a landing gear system. In: Boniol, F., Wiels, V., Ait Ameur, Y., Schewe, K.-D. (eds.) ABZ 2014. CCIS, vol. 433, pp. 52\u201365. Springer, Cham (2014). https:\/\/doi.org\/10.1007\/978-3-319-07512-9_4"},{"key":"28_CR16","doi-asserted-by":"publisher","unstructured":"Dumas, X., Dhaussy, P., Boniol, F., Bonnafous, E.: Application of partial-order methods for the verification of closed-loop SDL systems. In: Proceedings of the 2011 ACM Symposium on Applied Computing, pp. 1666\u20131673. SAC 2011. ACM, New York (2011). https:\/\/doi.org\/10.1145\/1982185.1982533","DOI":"10.1145\/1982185.1982533"},{"key":"28_CR17","unstructured":"Godefroid, P.: The Ulg partial-order package for SPIN. In: SPIN Workshop. Montr\u00e9al, Quebec (1995)"},{"issue":"5","key":"28_CR18","doi-asserted-by":"publisher","first-page":"279","DOI":"10.1109\/32.588521","volume":"23","author":"GJ Holzmann","year":"1997","unstructured":"Holzmann, G.J.: The model checker SPIN. IEEE Trans. Softw. Eng. 23(5), 279\u2013295 (1997). https:\/\/doi.org\/10.1109\/32.588521","journal-title":"IEEE Trans. Softw. Eng."},{"key":"28_CR19","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"298","DOI":"10.1007\/3-540-36384-X_24","volume-title":"Verification, Model Checking, and Abstract Interpretation","author":"D Kroening","year":"2003","unstructured":"Kroening, D., Strichman, O.: Efficient computation of recurrence diameters. In: Zuck, L.D., Attie, P.C., Cortesi, A., Mukhopadhyay, S. (eds.) VMCAI 2003. LNCS, vol. 2575, pp. 298\u2013309. Springer, Heidelberg (2003). https:\/\/doi.org\/10.1007\/3-540-36384-X_24"},{"issue":"2","key":"28_CR20","doi-asserted-by":"publisher","first-page":"143","DOI":"10.1016\/j.entcs.2006.02.036","volume":"176","author":"P Parizek","year":"2007","unstructured":"Parizek, P., Plasil, F.: Specification and generation of environment for model checking of software components. Electron. Notes Theor. Comput. Sci. 176(2), 143\u2013154 (2007). https:\/\/doi.org\/10.1016\/j.entcs.2006.02.036","journal-title":"Electron. Notes Theor. Comput. Sci."},{"key":"28_CR21","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"905","DOI":"10.1007\/11751649_99","volume-title":"Computational Science and Its Applications - ICCSA 2006","author":"S Park","year":"2006","unstructured":"Park, S., Kwon, G.: Avoidance of state explosion using dependency analysis in model checking control flow model. In: Gavrilova, M.L., et al. (eds.) ICCSA 2006. LNCS, vol. 3984, pp. 905\u2013911. Springer, Heidelberg (2006). https:\/\/doi.org\/10.1007\/11751649_99"},{"issue":"1","key":"28_CR22","doi-asserted-by":"publisher","first-page":"39","DOI":"10.1007\/BF00121262","volume":"8","author":"D Peled","year":"1996","unstructured":"Peled, D.: Combining partial order reductions with on-the-fly model-checking. Formal Methods Syst. Des. 8(1), 39\u201364 (1996). https:\/\/doi.org\/10.1007\/BF00121262","journal-title":"Formal Methods Syst. Des."},{"key":"28_CR23","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"337","DOI":"10.1007\/3-540-11494-7_22","volume-title":"International Symposium on Programming","author":"JP Queille","year":"1982","unstructured":"Queille, J.P., Sifakis, J.: Specification and verification of concurrent systems in CESAR. In: Dezani-Ciancaglini, M., Montanari, U. (eds.) Programming 1982. LNCS, vol. 137, pp. 337\u2013351. Springer, Heidelberg (1982). https:\/\/doi.org\/10.1007\/3-540-11494-7_22"},{"issue":"2","key":"28_CR24","doi-asserted-by":"publisher","first-page":"229","DOI":"10.1007\/s10009-015-0401-2","volume":"19","author":"C Teodorov","year":"2017","unstructured":"Teodorov, C., Dhaussy, P., Le Roux, L.: Environment-driven reachability for timed systems. Int. J. Softw. Tools Technol. Transfer 19(2), 229\u2013245 (2017). https:\/\/doi.org\/10.1007\/s10009-015-0401-2","journal-title":"Int. J. Softw. Tools Technol. Transfer"},{"key":"28_CR25","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"53","DOI":"10.1007\/978-3-319-11587-0_7","volume-title":"Model and Data Engineering","author":"C Teodorov","year":"2014","unstructured":"Teodorov, C., Le Roux, L., Dhaussy, P.: Context-aware verification of a cruise-control system. In: Ait Ameur, Y., Bellatreche, L., Papadopoulos, G.A. (eds.) MEDI 2014. LNCS, vol. 8748, pp. 53\u201364. Springer, Cham (2014). https:\/\/doi.org\/10.1007\/978-3-319-11587-0_7"},{"issue":"7","key":"28_CR26","doi-asserted-by":"publisher","first-page":"516","DOI":"10.1002\/stvr.1611","volume":"26","author":"C Teodorov","year":"2016","unstructured":"Teodorov, C., Le Roux, L., Drey, Z., Dhaussy, P.: Past-free[ze] reachability analysis: reaching further with DAG-directed exhaustive state-space analysis. Softw. Test. Verif. Reliab. 26(7), 516\u2013542 (2016). https:\/\/doi.org\/10.1002\/stvr.1611","journal-title":"Softw. Test. Verif. Reliab."},{"issue":"3","key":"28_CR27","doi-asserted-by":"publisher","first-page":"194","DOI":"10.1049\/iet-sen.2009.0017","volume":"4","author":"O Tkachuk","year":"2010","unstructured":"Tkachuk, O., Dwyer, M.B.: Environment generation for validating event-driven software using model checking. IET Softw. 4(3), 194\u2013209 (2010). https:\/\/doi.org\/10.1049\/iet-sen.2009.0017","journal-title":"IET Softw."},{"key":"28_CR28","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"491","DOI":"10.1007\/3-540-53863-1_36","volume-title":"Advances in Petri Nets 1990","author":"A Valmari","year":"1991","unstructured":"Valmari, A.: Stubborn sets for reduced state space generation. In: Rozenberg, G. (ed.) ICATPN 1989. LNCS, vol. 483, pp. 491\u2013515. Springer, Heidelberg (1991). https:\/\/doi.org\/10.1007\/3-540-53863-1_36"},{"key":"28_CR29","unstructured":"Wiels, V., Ledinot, E., Belin, E., Dassault, M.: Experiences in using model checking to verify real time properties of a landing gear control system. In: Embedded Real-Time Systems (ERTS). Toulouse, France (Jan 2006)"},{"key":"28_CR30","doi-asserted-by":"publisher","first-page":"58","DOI":"10.1007\/978-3-642-16164-3_5","volume-title":"Model Checking Software","author":"Kenro Yatake","year":"2010","unstructured":"Yatake, K., Aoki, T.: Automatic generation of model checking scripts based on environment modeling. In: Model Checking Software - 17th International SPIN Workshop, Enschede, The Netherlands, September 27\u201329, 2010. Proceedings, pp. 58\u201375 (2010). https:\/\/doi.org\/10.1007\/978-3-642-16164-3_5"},{"key":"28_CR31","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"54","DOI":"10.1007\/3-540-48153-2_6","volume-title":"Correct Hardware Design and Verification Methods","author":"Y Yu","year":"1999","unstructured":"Yu, Y., Manolios, P., Lamport, L.: Model checking TLA+ specifications. In: Pierre, L., Kropf, T. (eds.) CHARME 1999. LNCS, vol. 1703, pp. 54\u201366. Springer, Heidelberg (1999). https:\/\/doi.org\/10.1007\/3-540-48153-2_6"}],"container-title":["Lecture Notes in Computer Science","Software Engineering and Formal Methods"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-030-30446-1_28","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2023,9,19]],"date-time":"2023-09-19T20:28:17Z","timestamp":1695155297000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-030-30446-1_28"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2019]]},"ISBN":["9783030304454","9783030304461"],"references-count":31,"URL":"https:\/\/doi.org\/10.1007\/978-3-030-30446-1_28","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2019]]},"assertion":[{"value":"9 September 2019","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}},{"value":"SEFM","order":1,"name":"conference_acronym","label":"Conference Acronym","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"International Conference on Software Engineering and Formal Methods","order":2,"name":"conference_name","label":"Conference Name","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Oslo","order":3,"name":"conference_city","label":"Conference City","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Norway","order":4,"name":"conference_country","label":"Conference Country","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"2019","order":5,"name":"conference_year","label":"Conference Year","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"18 September 2019","order":7,"name":"conference_start_date","label":"Conference Start Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"20 September 2019","order":8,"name":"conference_end_date","label":"Conference End Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"17","order":9,"name":"conference_number","label":"Conference Number","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"sefm2019","order":10,"name":"conference_id","label":"Conference ID","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"http:\/\/sefm2019.inria.fr\/","order":11,"name":"conference_url","label":"Conference URL","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Single-blind","order":1,"name":"type","label":"Type","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"EasyChair","order":2,"name":"conference_management_system","label":"Conference Management System","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"89","order":3,"name":"number_of_submissions_sent_for_review","label":"Number of Submissions Sent for Review","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"27","order":4,"name":"number_of_full_papers_accepted","label":"Number of Full Papers Accepted","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"0","order":5,"name":"number_of_short_papers_accepted","label":"Number of Short Papers Accepted","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"30% - The value is computed by the equation \"Number of Full Papers Accepted \/ Number of Submissions Sent for Review * 100\" and then rounded to a whole number.","order":6,"name":"acceptance_rate_of_full_papers","label":"Acceptance Rate of Full Papers","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"3","order":7,"name":"average_number_of_reviews_per_paper","label":"Average Number of Reviews per Paper","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"6","order":8,"name":"average_number_of_papers_per_reviewer","label":"Average Number of Papers per Reviewer","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"Yes","order":9,"name":"external_reviewers_involved","label":"External Reviewers Involved","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}}]}}