{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,11,1]],"date-time":"2025-11-01T06:08:29Z","timestamp":1761977309875,"version":"build-2065373602"},"publisher-location":"Cham","reference-count":46,"publisher":"Springer International Publishing","isbn-type":[{"type":"print","value":"9783319030760"},{"type":"electronic","value":"9783319030777"}],"license":[{"start":{"date-parts":[[2013,1,1]],"date-time":"2013-01-01T00:00:00Z","timestamp":1356998400000},"content-version":"tdm","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2013]]},"DOI":"10.1007\/978-3-319-03077-7_19","type":"book-chapter","created":{"date-parts":[[2013,10,28]],"date-time":"2013-10-28T01:40:21Z","timestamp":1382924421000},"page":"279-294","source":"Crossref","is-referenced-by-count":5,"title":["Efficient Analysis of Reliability Architectures via Predicate Abstraction"],"prefix":"10.1007","author":[{"given":"Marco","family":"Bozzano","sequence":"first","affiliation":[]},{"given":"Alessandro","family":"Cimatti","sequence":"additional","affiliation":[]},{"given":"Cristian","family":"Mattarei","sequence":"additional","affiliation":[]}],"member":"297","reference":[{"key":"19_CR1","unstructured":"Proc. of Formal Methods in Computer-Aided Design, FMCAD 2007, Austin, Texas, USA, November 11-14. IEEE Computer Society (2007)"},{"key":"19_CR2","unstructured":"Proc. of 9th International Conference on Formal Methods in Computer-Aided Design, FMCAD 2009, Austin, Texas, USA, November 15-18. IEEE (2009)"},{"issue":"7","key":"19_CR3","doi-asserted-by":"publisher","first-page":"682","DOI":"10.1109\/T-C.1974.224016","volume":"100","author":"J.A. Abraham","year":"1974","unstructured":"Abraham, J.A., Siewiorek, D.P.: An algorithm for the accurate reliability evaluation of triple modular redundancy networks. IEEE Trans. on Comp.\u00a0100(7), 682\u2013692 (1974)","journal-title":"IEEE Trans. on Comp."},{"key":"19_CR4","unstructured":"Akerlund, O., Bieber, P., Boede, E., Bozzano, M., Bretschneider, M., Castel, C., Cavallo, A., Cifaldi, M., Gauthier, J., Griffault, A., et al.: ISAAC, A framework for integrated safety analysis of functional, geometrical and human aspects. In: Proc. ERTS (2006)"},{"key":"19_CR5","unstructured":"Anderson, T., Lee, P.A.: Fault tolerance, principles and practice. Prentice\/Hall International (1981)"},{"key":"19_CR6","unstructured":"Barrett, C.W., Sebastiani, R., Seshia, S.A., Tinelli, C.: Satisfiability modulo theories. In: Biere, et al. (eds.) [9], pp. 825\u2013885"},{"key":"19_CR7","unstructured":"Bensalem, S., Ganesh, V., Lakhnech, Y., Munoz, C., Owre, S., Rue\u00df, H., Rushby, J., Rusu, V., Sa\u0131di, H., Shankar, N., et al.: An overview of sal. In: Proc. of the 5th NASA Langley Formal Methods Workshop (2000)"},{"key":"19_CR8","doi-asserted-by":"publisher","first-page":"117","DOI":"10.1016\/S0065-2458(03)58003-2","volume":"58","author":"A. Biere","year":"2003","unstructured":"Biere, A., Cimatti, A., Clarke, E.M., Strichman, O., Zhu, Y.: Bounded model checking. Advances in Computers\u00a058, 117\u2013148 (2003)","journal-title":"Advances in Computers"},{"key":"19_CR9","unstructured":"Biere, A., Heule, M., van Maaren, H., Walsh, T. (eds.): Handbook of Satisfiability. FAIA, vol.\u00a0185. IOS Press (2009)"},{"key":"19_CR10","doi-asserted-by":"publisher","first-page":"265","DOI":"10.1007\/s10817-005-9004-z","volume":"35","author":"M. Bozzano","year":"2005","unstructured":"Bozzano, M., Bruttomesso, R., Cimatti, A., Junttila, T., van Rossum, P., Schulz, S., Sebastiani, R.: MathSAT: Tight Integration of SAT and Mathematical Decision Procedures. Journal of Automated Reasoning\u00a035, 265\u2013293 (2005)","journal-title":"Journal of Automated Reasoning"},{"key":"19_CR11","unstructured":"Bozzano, M., Cimatti, A., Katoen, J.P., Nguyen, V.Y., Noll, T., Roveri, M.: Safety, dependability, and performance analysis of extended AADL models. The Computer Journal (March 2010), doi:10.1093\/com"},{"key":"19_CR12","unstructured":"Bozzano, M., Cimatti, A., Lisagor, O., Mattarei, C., Mover, S., Roveri, M., Tonetta, S.: Symbolic model checking and safety assessment of altarica models. ECEASST\u00a046 (2012)"},{"key":"19_CR13","doi-asserted-by":"crossref","unstructured":"Bozzano, M., Cimatti, A., Mattarei, C.: Automated analysis of reliability architectures. In: ICECCS, pp. 198\u2013207. IEEE Computer Society (2013)","DOI":"10.1109\/ICECCS.2013.37"},{"key":"19_CR14","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"162","DOI":"10.1007\/978-3-540-75596-8_13","volume-title":"Automated Technology for Verification and Analysis","author":"M. Bozzano","year":"2007","unstructured":"Bozzano, M., Cimatti, A., Tapparo, F.: Symbolic Fault Tree Analysis for Reactive Systems. In: Namjoshi, K.S., Yoneda, T., Higashino, T., Okamura, Y. (eds.) ATVA 2007. LNCS, vol.\u00a04762, pp. 162\u2013176. Springer, Heidelberg (2007)"},{"issue":"1","key":"19_CR15","doi-asserted-by":"publisher","first-page":"5","DOI":"10.1007\/s10009-006-0001-2","volume":"9","author":"M. Bozzano","year":"2007","unstructured":"Bozzano, M., Villafiorita, A.: The FSAP\/NuSMV-SA Safety Analysis Platform. International Journal on Software Tools for Technology Transfer\u00a09(1), 5\u201324 (2007)","journal-title":"International Journal on Software Tools for Technology Transfer"},{"key":"19_CR16","doi-asserted-by":"crossref","unstructured":"Bozzano, M., Villafiorita, A.: Design and Safety Assessment of Critical Systems. CRC Press (Taylor and Francis), An Auerbach Book (2010)","DOI":"10.1201\/b10094"},{"key":"19_CR17","unstructured":"Bozzano, M., Villafiorita, A., \u00c5kerlund, O., Bieber, P., Bougnol, C., B\u00f6de, E., Bretschneider, M., Cavallo, A., et al.: ESACS: An integrated methodology for design and safety analysis of complex systems. In: Proc. ESREL 2003, pp. 237\u2013245 (2003)"},{"issue":"8","key":"19_CR18","doi-asserted-by":"publisher","first-page":"677","DOI":"10.1109\/TC.1986.1676819","volume":"35","author":"R.E. Bryant","year":"1986","unstructured":"Bryant, R.E.: Graph-based algorithms for boolean function manipulation. IEEE Trans. Computers\u00a035(8), 677\u2013691 (1986)","journal-title":"IEEE Trans. Computers"},{"key":"19_CR19","doi-asserted-by":"crossref","unstructured":"Ciardo, G., Muppala, J., Trivedi, K.: SPNP: stochastic Petri net package. In: Proc. of the Third International Workshop on Petri Nets and Performance Models, PNPM 1989, pp. 142\u2013151. IEEE (1989)","DOI":"10.1109\/PNPM.1989.68548"},{"issue":"4","key":"19_CR20","doi-asserted-by":"publisher","first-page":"410","DOI":"10.1007\/s100090050046","volume":"2","author":"A. Cimatti","year":"2000","unstructured":"Cimatti, A., Clarke, E., Giunchiglia, F., Roveri, M.: NuSMV: A new symbolic model checker. International Journal on Software Tools for Technology Transfer (STTT)\u00a02(4), 410\u2013425 (2000)","journal-title":"International Journal on Software Tools for Technology Transfer (STTT)"},{"key":"19_CR21","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"93","DOI":"10.1007\/978-3-642-36742-7_7","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"A. Cimatti","year":"2013","unstructured":"Cimatti, A., Griggio, A., Schaafsma, B.J., Sebastiani, R.: The MathSAT5 SMT Solver. In: Piterman, N., Smolka, S.A. (eds.) TACAS 2013. LNCS, vol.\u00a07795, pp. 93\u2013107. Springer, Heidelberg (2013)"},{"key":"19_CR22","doi-asserted-by":"crossref","unstructured":"Cimatti, A., Mover, S., Tonetta, S.: SMT-Based Verification of Hybrid Systems. In: Hoffmann, J., Selman, B. (eds.) AAAI (2012)","DOI":"10.1007\/s10703-012-0158-0"},{"issue":"1","key":"19_CR23","doi-asserted-by":"publisher","first-page":"46","DOI":"10.1007\/s10703-012-0158-0","volume":"42","author":"A. Cimatti","year":"2013","unstructured":"Cimatti, A., Mover, S., Tonetta, S.: SMT-based scenario verification for hybrid systems. Formal Methods in System Design\u00a042(1), 46\u201366 (2013)","journal-title":"Formal Methods in System Design"},{"key":"19_CR24","doi-asserted-by":"crossref","unstructured":"Cimatti, A., Tonetta, S.: A property-based proof system for contract-based design. In: 2012 38th EUROMICRO Conference on Software Engineering and Advanced Applications (SEAA), pp. 21\u201328. IEEE (2012)","DOI":"10.1109\/SEAA.2012.68"},{"key":"19_CR25","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"496","DOI":"10.1007\/978-3-540-27813-9_45","volume-title":"Computer Aided Verification","author":"L. Moura de","year":"2004","unstructured":"de Moura, L., Owre, S., Rue\u00df, H., Rushby, J., Shankar, N., Sorea, M., Tiwari, A.: SAL 2. In: Alur, R., Peled, D.A. (eds.) CAV 2004. LNCS, vol.\u00a03114, pp. 496\u2013500. Springer, Heidelberg (2004)"},{"issue":"3","key":"19_CR26","doi-asserted-by":"publisher","first-page":"342","DOI":"10.1109\/TR.2004.833308","volume":"53","author":"M. Favalli","year":"2004","unstructured":"Favalli, M., Metra, C.: TMR voting in the presence of crosstalk faults at the voter inputs. IEEE Transactions on Reliability\u00a053(3), 342\u2013348 (2004)","journal-title":"IEEE Transactions on Reliability"},{"issue":"3-4","key":"19_CR27","doi-asserted-by":"crossref","first-page":"209","DOI":"10.3233\/SAT190012","volume":"1","author":"M. Fr\u00e4nzle","year":"2007","unstructured":"Fr\u00e4nzle, M., Herde, C., Teige, T., Ratschan, S., Schubert, T.: Efficient solving of large non-linear arithmetic constraint systems with complex boolean structure. J. on Satisfiability, Boolean Modeling and Computation\u00a01(3-4), 209\u2013236 (2007)","journal-title":"J. on Satisfiability, Boolean Modeling and Computation"},{"key":"19_CR28","doi-asserted-by":"crossref","unstructured":"Hamamatsu, M., Tsuchiya, T., Kikuno, T.: On the reliability of cascaded TMR systems. In: 2010 IEEE 16th Pacific Rim International Symposium on Dependable Computing (PRDC), pp. 184\u2013190. IEEE (2010)","DOI":"10.1109\/PRDC.2010.45"},{"key":"19_CR29","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"441","DOI":"10.1007\/11691372_29","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"A. Hinton","year":"2006","unstructured":"Hinton, A., Kwiatkowska, M., Norman, G., Parker, D.: PRISM: A tool for automatic verification of probabilistic systems. In: Hermanns, H., Palsberg, J. (eds.) TACAS 2006. LNCS, vol.\u00a03920, pp. 441\u2013444. Springer, Heidelberg (2006)"},{"issue":"5","key":"19_CR30","doi-asserted-by":"publisher","first-page":"279","DOI":"10.1109\/32.588521","volume":"23","author":"G.J. Holzmann","year":"1997","unstructured":"Holzmann, G.J.: The model checker spin. IEEE Transactions on Software Engineering\u00a023(5), 279\u2013295 (1997)","journal-title":"IEEE Transactions on Software Engineering"},{"key":"19_CR31","doi-asserted-by":"crossref","unstructured":"Johnson, J.M., Wirthlin, M.J.: Voter insertion algorithms for fpga designs using triple modular redundancy. In: Proc. of the 18th Annual ACM\/SIGDA International Symposium on Field Programmable Gate Arrays, pp. 249\u2013258. ACM (2010)","DOI":"10.1145\/1723112.1723154"},{"key":"19_CR32","unstructured":"Jones, G., Sheeran, M.: Relations and refinement in circuit design. In: 3rd Refinement Workshop, vol.\u00a090, pp. 133\u2013152. Citeseer (1990)"},{"key":"19_CR33","unstructured":"Joshi, A., Whalen, M., Heimdahl, M.P.E.: Modelbased safety analysis: Final report. Technical report (2005)"},{"key":"19_CR34","doi-asserted-by":"crossref","unstructured":"Katoen, J.-P., Khattri, M., Zapreevt, I.S.: A markov reward model checker. In: Second International Conference on the Quantitative Evaluation of Systems, pp. 243\u2013244. IEEE (2005)","DOI":"10.1109\/QEST.2005.2"},{"key":"19_CR35","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"424","DOI":"10.1007\/11817963_39","volume-title":"Computer Aided Verification","author":"S.K. Lahiri","year":"2006","unstructured":"Lahiri, S.K., Nieuwenhuis, R., Oliveras, A.: SMT Techniques for Fast Predicate Abstraction. In: Ball, T., Jones, R.B. (eds.) CAV 2006. LNCS, vol.\u00a04144, pp. 424\u2013437. Springer, Heidelberg (2006)"},{"key":"19_CR36","unstructured":"Tan, L., Tan, Q., Li, J.: Specification and verification of the triple-modular redundancy fault tolerant system using csp. In: The Fourth International Conference on Dependability, DEPEND 2011, pp. 14\u201317 (2011)"},{"issue":"21","key":"19_CR37","doi-asserted-by":"publisher","first-page":"657","DOI":"10.1587\/elex.4.657","volume":"4","author":"S. Lee","year":"2007","unstructured":"Lee, S., Jung, J.I., Lee, I.: Voting structures for cascaded triple modular redundant modules. IEICE Electronic Express\u00a04(21), 657\u2013664 (2007)","journal-title":"IEICE Electronic Express"},{"key":"19_CR38","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1007\/978-3-540-45069-6_1","volume-title":"Computer Aided Verification","author":"K.L. McMillan","year":"2003","unstructured":"McMillan, K.L.: Interpolation and SAT-based model checking. In: Hunt Jr., W.A., Somenzi, F. (eds.) CAV 2003. LNCS, vol.\u00a02725, pp. 1\u201313. Springer, Heidelberg (2003)"},{"key":"19_CR39","doi-asserted-by":"crossref","unstructured":"McMillan, K.L.: Symbolic Model Checking. Kluwer Academic Publishers (1993)","DOI":"10.1007\/978-1-4615-3190-6"},{"issue":"1","key":"19_CR40","doi-asserted-by":"publisher","first-page":"89","DOI":"10.1016\/0166-5316(95)00012-M","volume":"24","author":"W.H. Sanders","year":"1995","unstructured":"Sanders, W.H., Obal II, D., Qureshi, M.A., Widjanarko, F.: The ultrasan modeling environment. Perf. Evaluation\u00a024(1), 89\u2013115 (1995)","journal-title":"Perf. Evaluation"},{"key":"19_CR41","unstructured":"Silva, J.P.M., Lynce, I., Malik, S.: Conflict-driven clause learning sat solvers. In: Biere, et al. (eds.) [9], pp. 131\u2013153"},{"issue":"4","key":"19_CR42","doi-asserted-by":"publisher","first-page":"298","DOI":"10.1109\/MDT.2005.93","volume":"22","author":"D.D. Thaker","year":"2005","unstructured":"Thaker, D.D., Amirtharajah, R., Impens, F., Chuang, I.L., Chong, F.T.: Recursive TMR: Scaling fault tolerance in the nanoscale era. IEEE Design & Test of Computers\u00a022(4), 298\u2013305 (2005)","journal-title":"IEEE Design & Test of Computers"},{"key":"19_CR43","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"89","DOI":"10.1007\/978-3-642-05089-3_7","volume-title":"FM 2009: Formal Methods","author":"S. Tonetta","year":"2009","unstructured":"Tonetta, S.: Abstract model checking without computing the abstraction. In: Cavalcanti, A., Dams, D.R. (eds.) FM 2009. LNCS, vol.\u00a05850, pp. 89\u2013105. Springer, Heidelberg (2009)"},{"key":"19_CR44","doi-asserted-by":"crossref","unstructured":"Trivedi, K.S.: Sharpe 2002: Symbolic hierarchical automated reliability and performance evaluator. In: Proc. International Conference on Dependable Systems and Networks, DSN 2002, p. 544. IEEE (2002)","DOI":"10.1109\/DSN.2002.1028975"},{"key":"19_CR45","unstructured":"Vesely, W.E., Stamatelatos, M., Dugan, J., Fragola, J., Minarick III, J., Railsback, J.: Fault Tree Handbook with Aerospace Applications (2002)"},{"key":"19_CR46","doi-asserted-by":"crossref","unstructured":"Yeh, Y.C.: Triple-triple redundant 777 primary flight computer. In: Proc. of the IEEE Aerospace Applications Conference, vol.\u00a01, pp. 293\u2013307. IEEE (1996)","DOI":"10.1109\/AERO.1996.495891"}],"container-title":["Lecture Notes in Computer Science","Hardware and Software: Verification and Testing"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-319-03077-7_19","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,4,30]],"date-time":"2025-04-30T18:28:58Z","timestamp":1746037738000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-319-03077-7_19"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2013]]},"ISBN":["9783319030760","9783319030777"],"references-count":46,"URL":"https:\/\/doi.org\/10.1007\/978-3-319-03077-7_19","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2013]]}}}