{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,10]],"date-time":"2024-09-10T13:14:51Z","timestamp":1725974091646},"publisher-location":"Cham","reference-count":26,"publisher":"Springer International Publishing","isbn-type":[{"type":"print","value":"9783319635156"},{"type":"electronic","value":"9783319635163"}],"license":[{"start":{"date-parts":[[2018,1,1]],"date-time":"2018-01-01T00:00:00Z","timestamp":1514764800000},"content-version":"unspecified","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":[[2018]]},"DOI":"10.1007\/978-3-319-63516-3_16","type":"book-chapter","created":{"date-parts":[[2018,4,4]],"date-time":"2018-04-04T23:43:39Z","timestamp":1522885419000},"page":"617-632","update-policy":"http:\/\/dx.doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":0,"title":["An Application of Parallel Satisfiability Solving to the Verification of Complex Embedded Systems"],"prefix":"10.1007","author":[{"given":"Orlando","family":"Ferrante","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Alberto","family":"Ferrari","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Christos","family":"Sofronis","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Leonardo","family":"Mangeruca","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Luca","family":"Benvenuti","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2018,4,6]]},"reference":[{"key":"16_CR1","doi-asserted-by":"crossref","unstructured":"Miller, S., Anderson, E., Wagner, L., Whalen, M., Heimdahl, M.: Formal verification of flight critical software. In: Proceedings of the AIAA Guidance, Navigation and Control Conference and Exhibit. (2005) 15\u201318","DOI":"10.2514\/6.2005-6431"},{"key":"16_CR2","unstructured":"Miller, S., Whalen, M., Cofer, D.: Software model checking takes off. Communications of the ACM 53(2) (2010) 58\u201364"},{"key":"16_CR3","unstructured":"Cimatti, A., Clarke, E., Giunchiglia, E., Giunchiglia, F., Pistore, M., Roveri, M., Sebastiani, R., Tacchella, A.: Nusmv 2: An opensource tool for symbolic model checking. (2002) 359\u2013364"},{"key":"16_CR4","unstructured":"http:\/\/sal.csl.sri.com\/"},{"key":"16_CR5","unstructured":"http:\/\/www.prover.com\/"},{"key":"16_CR6","doi-asserted-by":"crossref","unstructured":"Ball, T., Levin, V., Rajamani, S.K.: A decade of software model checking with SLAM, Communications of the ACM, 54(7), pp 68\u201376, 2011.","DOI":"10.1145\/1965724.1965743"},{"key":"16_CR7","doi-asserted-by":"crossref","unstructured":"Ball, T., Cook, B., Levin, V., Rajamani, S.K.: SLAM and Static Driver Verifier: Technology transfer of formal methods inside Microsoft. pp 1\u201320, IFM, 2004.","DOI":"10.1007\/978-3-540-24756-2_1"},{"key":"16_CR8","doi-asserted-by":"crossref","unstructured":"Godefroid, P.: Compositional dynamic test generation (extended abstract), POPL 2007.","DOI":"10.1145\/1190216.1190226"},{"key":"16_CR9","unstructured":"Burch, J.R., Clarke, E.M., Mc Millan, K.L., Dill, D.L., Hwang, L.J.: Symbolic model checking: 10\u02c620 states and beyond, LICS, 1990."},{"key":"16_CR10","doi-asserted-by":"crossref","unstructured":"Biere, A., Cimatti, A., Clarke, E., Zhu, Y.: Symbolic model checking without BDDs. Tools and Algorithms for the Construction and Analysis of Systems (1999) 193\u2013207","DOI":"10.21236\/ADA360973"},{"key":"16_CR11","unstructured":"Barrett, C., Sebastiani, R., Seshia, S., Tinelli, C.: Satisfiability modulo theories. Handbook of Satisfiability 4 (2009)"},{"key":"16_CR12","doi-asserted-by":"crossref","unstructured":"Hamadi, Y., Sais, L.: ManySAT: a parallel SAT solver. Journal on Satisfiability, Boolean Modeling and Computation (JSAT) (2009)","DOI":"10.3233\/SAT190070"},{"key":"16_CR13","unstructured":"http:\/\/www.mathworks.com\/products\/simulink\/"},{"key":"16_CR14","unstructured":"http:\/\/www.omg.org\/spec\/QVT\/index.htm"},{"key":"16_CR15","unstructured":"Ferrari, A., Mangeruca, L., Ferrante, O., Mignogna, A.: DesyreML: a SysML profile for heterogeneous embedded systems. In: Embedded Real Time Software and Systems (ERTS). (2012)"},{"key":"16_CR16","doi-asserted-by":"crossref","unstructured":"Mangeruca, L., Ferrante, O., Ferrari, A.: Formalization and completeness of evolving requirements using contracts. In: 8th IEEE International Symposium on Industrial Embedded Systems (SIES). (2013)","DOI":"10.1109\/SIES.2013.6601484"},{"key":"16_CR17","doi-asserted-by":"crossref","unstructured":"Carloni, M., Ferrante, O., Ferrari, A., Massaroli, G., Orazzo, A., Petrone, I., Velardi, L.: Contract-based analysis for verification of communication-based train control (CBTC) system. In: SAFECOMP. (2014)","DOI":"10.1007\/978-3-319-10557-4_17"},{"key":"16_CR18","doi-asserted-by":"crossref","unstructured":"Carloni, M., Ferrante, O., Ferrari, A., Massaroli, G., Orazzo, A., Petrone, I., Velardi, L.: Contract modeling and verification with formal specs verifier toolsuite - application to Ansaldo STS rapid transit metro system use case. In: SAFECOMP. (2015)","DOI":"10.1007\/978-3-319-24249-1_16"},{"key":"16_CR19","unstructured":"Ferrante, O., Benvenuti, L., Mangeruca, L., Sofronis, C., Ferrari, A.: Parallel NuSMV: a NuSMV extension for the verification of complex embedded systems. Lecture Notes in Computer Science: Computer Safety, Reliability, and Security 7613 (2012) 409\u2013416"},{"key":"16_CR20","unstructured":"Marazza, M., Ferrante, O., Ferrari, A.: Automatic generation of failure scenarios for sytems-on-chip. In: Real Time Software and Systems (ERTS). (2014)"},{"key":"16_CR21","unstructured":"Ferrante, O., Ferrari, A., Marazza, M.: An algorithm for the incremental generation of high coverage test suites. In: 19th IEEE European Test Symposium. (2014)"},{"key":"16_CR22","unstructured":"Ferrante, O., Ferrari, A., Marazza, M.: Formal Specs Verifier ATG: a tool for model-based generation of high coverage test suites. In: ERTS. (2016)"},{"key":"16_CR23","doi-asserted-by":"crossref","unstructured":"Een, N., S\u00f6rensson, N.: An extensible SAT-solver [ver 1.2] (2003)","DOI":"10.1007\/978-3-540-24605-3_37"},{"key":"16_CR24","unstructured":"Herbstritt, M.: zChaff: Modifications and extensions. (2001)"},{"key":"16_CR25","unstructured":"Murray, R.M., et al.: Feedback Systems An Introduction for Scientists and Engineers. Princeton University Press (2009)"},{"key":"16_CR26","unstructured":"http:\/\/www.danse-ip.eu\/home\/"}],"container-title":["Handbook of Parallel Constraint Reasoning"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-319-63516-3_16","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2020,10,30]],"date-time":"2020-10-30T23:01:11Z","timestamp":1604098871000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-319-63516-3_16"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2018]]},"ISBN":["9783319635156","9783319635163"],"references-count":26,"URL":"https:\/\/doi.org\/10.1007\/978-3-319-63516-3_16","relation":{},"subject":[],"published":{"date-parts":[[2018]]}}}