{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,1,30]],"date-time":"2025-01-30T05:59:39Z","timestamp":1738216779366,"version":"3.34.0"},"publisher-location":"Boston, MA","reference-count":66,"publisher":"Springer US","isbn-type":[{"type":"print","value":"9781402081569"},{"type":"electronic","value":"9781402081576"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"DOI":"10.1007\/978-1-4020-8157-6_23","type":"book-chapter","created":{"date-parts":[[2008,4,7]],"date-time":"2008-04-07T16:54:40Z","timestamp":1207587280000},"page":"257-281","source":"Crossref","is-referenced-by-count":3,"title":["Static Program Transformations for Efficient Software Model Checking"],"prefix":"10.1007","author":[{"given":"Shobha","family":"Vasudevan","sequence":"first","affiliation":[]},{"given":"Jacob A.","family":"Abraham","sequence":"additional","affiliation":[]}],"member":"297","reference":[{"key":"23_CR1","doi-asserted-by":"crossref","unstructured":"Alur, Rajeev, Henzinger, Thomas A., and Ho, Pei-Hsin (1993). Automatic symbolic verification of embedded systems. In IEEE Real-Time Systems Symposium, pages 2\u201311.","DOI":"10.1109\/REAL.1993.393520"},{"key":"23_CR2","doi-asserted-by":"crossref","first-page":"629","DOI":"10.1109\/PROC.1986.13527","volume":"74","author":"A. Avizenis","year":"1986","unstructured":"Avizenis, A. and Laprie, J. (1986). Dependable computing: From concepts to design diversity. Proceedings of the IEEE, 74:629\u2013638.","journal-title":"Proceedings of the IEEE"},{"issue":"4","key":"23_CR3","doi-asserted-by":"publisher","first-page":"51","DOI":"10.1109\/2.585154","volume":"30","author":"A. Avizienis","year":"1997","unstructured":"Avizienis, A. (1997). Toward systematic design of fault-tolerant systems. Computer, 30(4):51\u201358.","journal-title":"Computer"},{"key":"23_CR4","doi-asserted-by":"crossref","unstructured":"Avizienis, A. and Kelly, J. P. J. (1984). Fault tolerance by design diversity: Concepts and experiments. pages 67\u201380.","DOI":"10.1109\/MC.1984.1659219"},{"key":"23_CR5","doi-asserted-by":"crossref","unstructured":"Balarin, F. and Sangiovanni-Vincentelli, A. L. (1993). An iterative approach to language containment. In Proceedings of the 5th International Conference on Computer Aided Verification, pages 29\u201340.","DOI":"10.1007\/3-540-56922-7_4"},{"key":"23_CR6","doi-asserted-by":"crossref","unstructured":"Ball, Thomas and Rajamani, Sriram K. (2000). Bebop: A symbolic model checker for boolean programs. In SPIN, pages 113\u2013130.","DOI":"10.1007\/10722468_7"},{"key":"23_CR7","first-page":"103","volume":"2057","author":"T. Ball","year":"2001","unstructured":"Ball, Thomas and Rajamani, Sriram K. (2001). Automatically validating temporal safety properties of interfaces. Lecture Notes in Computer Science, 2057:103\u2013122.","journal-title":"Lecture Notes in Computer Science"},{"key":"23_CR8","doi-asserted-by":"crossref","unstructured":"Bensalem, Saddek, Graf, Susanne, and Lakhnech, Yassine (2003). Abstraction as the key for invariant verification. In Symposium on Verification celebrating Zohar Manna\u2019s 64th Birthday.","DOI":"10.1007\/978-3-540-39910-0_4"},{"key":"23_CR9","doi-asserted-by":"publisher","first-page":"319","DOI":"10.1007\/BFb0028755","volume":"1427","author":"S. Bensalem","year":"1998","unstructured":"Bensalem, Saddek, Lakhnech, Yassine, and Owre, Sam (1998). Computing abstractions of in finite state systems compositionally and automatically. In Computer-Aided Verification, CAV\u2019 98, volume 1427, pages 319\u2013331.","journal-title":"Computer-Aided Verification, CAV\u2019 98"},{"issue":"1","key":"23_CR10","doi-asserted-by":"publisher","first-page":"37","DOI":"10.1023\/A:1008697817793","volume":"6","author":"R. Bharadwaj","year":"1999","unstructured":"Bharadwaj, R. and Heitmeyer, C. L. (1999). Model checking complete requirements specifications using abstraction. Automated Software Engineering: An International Journal, 6(1):37\u201368.","journal-title":"Automated Software Engineering: An International Journal"},{"issue":"1","key":"23_CR11","doi-asserted-by":"publisher","first-page":"93","DOI":"10.1145\/371282.371364","volume":"2","author":"R. E. Bryant","year":"2001","unstructured":"Bryant, R. E., German, S., and Velev, M. N. (2001). Processor verification using efficient reductions of the logic of uninterpreted functions to propositional logic. ACM Trans. Comput. Logic, 2(1):93\u2013134.","journal-title":"ACM Trans. Comput. Logic"},{"key":"23_CR12","unstructured":"Cabodi, G., Camurati, P., and Quer, S. (1994). Symbolic exploration of large circuits with enhanced forward\/backward traversals. In Proceedings of the conference on European design automation, pages 22\u201327."},{"key":"23_CR13","doi-asserted-by":"crossref","first-page":"595","DOI":"10.1016\/S0950-5849(98)00086-X","volume":"40","author":"G. Canfora","year":"1998","unstructured":"Canfora, G., Cimitile, A., and Lucia, A. De (1998). Conditioned program slicing. Information and Software Technology Special Issue on Program Slicing, 40:595\u2013607.","journal-title":"Information and Software Technology Special Issue on Program Slicing"},{"key":"23_CR14","doi-asserted-by":"crossref","unstructured":"Chou, C. and Peled, D. (1996). Formal verification of a partial-order reduction technique for model checking. In Tools and Algorithms for Construction and Analysis of Systems, pages 241\u2013257.","DOI":"10.1007\/3-540-61042-1_48"},{"issue":"2","key":"23_CR15","doi-asserted-by":"publisher","first-page":"244","DOI":"10.1145\/5397.5399","volume":"8","author":"E. M. Clarke","year":"1986","unstructured":"Clarke, E. M., Emerson, E. A., and Sistla, A. P. (1986). Automatic verification of finite state concurrent system using temporal logic specifications: a practical approach. ACM Trans. Program. Lang. Syst., 8(2):244\u2013263.","journal-title":"ACM Trans. Program. Lang. Syst."},{"key":"23_CR16","doi-asserted-by":"crossref","unstructured":"Clarke, E. M., Grumberg, O., Jha, S., Lu, Y., and Veith, H. (2000). Counterexample-guided abstraction refinement. In Computer Aided Verification, pages 154\u2013169.","DOI":"10.1007\/10722167_15"},{"issue":"5","key":"23_CR17","doi-asserted-by":"publisher","first-page":"1512","DOI":"10.1145\/186025.186051","volume":"16","author":"E. M. Clarke","year":"1994","unstructured":"Clarke, Edmund M., Grumberg, Orna, and Long, David E. (1994). Model checking and abstraction. ACM Transactions on Programming Languages and Systems, 16(5): 1512\u20131542.","journal-title":"ACM Transactions on Programming Languages and Systems"},{"key":"23_CR18","doi-asserted-by":"crossref","unstructured":"Colon, Michael and Uribe, Tomas E. (1998). Generating finite-state abstractions of reactive systems using decision procedures. In Computer Aided Verification, pages 293\u2013304.","DOI":"10.1007\/BFb0028753"},{"key":"23_CR19","doi-asserted-by":"crossref","unstructured":"Corbett, James C., Dwyer, Matthew B., Hatcliff, John, Laubach, Shawn, P\u0103s\u0103reanu, Corina S., Robby, and Zheng, Hongjun (2000). Bandera: extracting finite-state models from Java source code. In International Conference on Software Engineering, pages 439\u2013448.","DOI":"10.1145\/337180.337234"},{"key":"23_CR20","doi-asserted-by":"crossref","first-page":"138","DOI":"10.1007\/3-540-44577-3_10","volume":"2000","author":"P. Cousot","year":"2001","unstructured":"Cousot, P. (2001). Abstract interpretation based formal methods and future challenges, invited paper. In Informatics \u2014 10 Years Back, 10 Years Ahead, volume 2000 of Lecture Notes in Computer Science, pages 138\u2013156.","journal-title":"Informatics \u2014 10 Years Back, 10 Years Ahead"},{"key":"23_CR21","doi-asserted-by":"crossref","unstructured":"Cousot, P. (2003). Automatic verification by abstract interpretation, invited tutorial. In Proceedings of the Fourth International Conference on Verification, Model Checking and Abstract Interpretation (VMCAI2003), pages 20\u201324.","DOI":"10.1007\/3-540-36384-X_4"},{"key":"23_CR22","doi-asserted-by":"crossref","unstructured":"Cousot, P. and Cousot, R. (1977). Abstract interpretation: a unified lattice model for static analysis of programs by construction or approximation of fixpoints. In Proceedings of the 4th ACM SIGACT-SIGPLAN symposium on Principles of programming languages, pages 238\u2013252.","DOI":"10.1145\/512950.512973"},{"issue":"1","key":"23_CR23","doi-asserted-by":"publisher","first-page":"69","DOI":"10.1023\/A:1008649901864","volume":"6","author":"P. Cousot","year":"1999","unstructured":"Cousot, P. and Cousot, R. (1999). Refining model checking by abstract interpretation. Automated Software Engineering, 6(1):69\u201395.","journal-title":"Automated Software Engineering"},{"key":"23_CR24","unstructured":"Dams, D. (1996). Abstract Interpretation and Partition Refinement for Model Checking. PhD thesis, Eindhoven University of Technology."},{"issue":"2","key":"23_CR25","doi-asserted-by":"publisher","first-page":"253","DOI":"10.1145\/244795.244800","volume":"19","author":"D. Dams","year":"1997","unstructured":"Dams, D., Gerth, R., and Grumberg, O. (1997). Abstract interpretation of reactive systems. ACM Trans. Program. Lang. Syst., 19(2):253\u2013291.","journal-title":"ACM Trans. Program. Lang. Syst."},{"key":"23_CR26","doi-asserted-by":"crossref","unstructured":"Dams, D., Hesse, W., and Holzmann, G. J. Abstracting C with abC. pages 515\u2013520.","DOI":"10.1007\/3-540-45657-0_43"},{"key":"23_CR27","doi-asserted-by":"crossref","unstructured":"Danicic, S., Fox, C., Harman, M., and Hierons, R. (2000). Consit: A conditioned program slicer. pages 216\u2013226.","DOI":"10.1109\/ICSM.2000.883049"},{"key":"23_CR28","doi-asserted-by":"crossref","unstructured":"Daoudi, M., Ouarbya, L., Howroyd, J., Danicic, S., Marman, Mark, Fox, Chris, and Ward, M. P. (2002). Consus: A scalable approach to conditional slicing. In IEEE Proceedings of the Working Conference on Reverse Engineering, pages 181\u2013189.","DOI":"10.1109\/WCRE.2002.1173069"},{"key":"23_CR29","doi-asserted-by":"crossref","unstructured":"Das, S., Dill, D., and Park, S. (1999). Experience with predicate abstraction. In Computer Aided Verification, pages 160\u2013171.","DOI":"10.1007\/3-540-48683-6_16"},{"key":"23_CR30","doi-asserted-by":"crossref","unstructured":"Dwyer, M. B., Hatcliff, J., Joehanes, R., Laubach, S., Pasareanu, C. S., Robby, Zheng, H., and Visser, W. (2001). Tool-supported program abstraction for finite-state verification. In International Conference on Software Engineering, pages 177\u2013187.","DOI":"10.1109\/ICSE.2001.919092"},{"issue":"1\/2","key":"23_CR31","doi-asserted-by":"publisher","first-page":"105","DOI":"10.1007\/BF00625970","volume":"9","author":"E. A. Emerson","year":"1996","unstructured":"Emerson, E. Allen and Sistla, A. Prasad (1996). Symmetry and model checking. Formal Methods in System Design: An International Journal, 9(1\/2):105\u2013131.","journal-title":"Formal Methods in System Design: An International Journal"},{"key":"23_CR32","doi-asserted-by":"crossref","unstructured":"Govindaraju, S. G. and Dill, D. L. (1998). Verification by approximate forward and backward reachability. In Proceedings of the 1998 IEEE\/ACM international conference on Computeraided design, pages 366\u2013370. ACM Press.","DOI":"10.1145\/288548.289055"},{"key":"23_CR33","doi-asserted-by":"crossref","unstructured":"Govindaraju, Shankar G. and Dill, David L. (2000). Counterexample-guided choice of projections in approximate symbolic model checking. In Proceedings of the 2000 IEEE\/ACM international conference on Computer-aided design, pages 115\u2013119.","DOI":"10.1109\/ICCAD.2000.896460"},{"key":"23_CR34","doi-asserted-by":"crossref","unstructured":"Graf, S. and Saidi, H. (1997). Construction of abstract state graphs with pvs. In Proceedings of the 9th International Conference on Computer Aided Verification, pages 72\u201383.","DOI":"10.1007\/3-540-63166-6_10"},{"issue":"1","key":"23_CR35","doi-asserted-by":"publisher","first-page":"45","DOI":"10.1016\/S0164-1212(02)00135-8","volume":"68","author":"M. Harman","year":"2003","unstructured":"Harman, M., Binkley, D., and Danicic, S. (2003). Amorphous program slicing. Journal of Systems and Software, 68(1):45\u201364.","journal-title":"Journal of Systems and Software"},{"issue":"4","key":"23_CR36","doi-asserted-by":"publisher","first-page":"315","DOI":"10.1023\/A:1026599015809","volume":"13","author":"J. Hatcliff","year":"2000","unstructured":"Hatcliff, J., Dwyer, M. B., and Zheng, H. (2000). Slicing software for model construction. Higher-Order and Symbolic Computation, 13(4):315\u2013353.","journal-title":"Higher-Order and Symbolic Computation"},{"issue":"12","key":"23_CR37","first-page":"1465","volume":"15","author":"H. Cho","year":"1996","unstructured":"H. Cho, G. Hachtel, E. Macii, B. Pleisser, and F. Somenzi (1996). Algorithms for approximate fsm traversal based on state space decomposition. IEEE TCAD, 15(12): 1465\u20131478.","journal-title":"IEEE TCAD"},{"key":"23_CR38","doi-asserted-by":"crossref","unstructured":"Henzinger, T. A., Jhala, R., Majumdar, R., and Sutre, G. (2002). Lazy abstraction. In Symposium on Principles of Programming Languages, pages 58\u201370.","DOI":"10.1145\/503272.503279"},{"key":"23_CR39","doi-asserted-by":"crossref","unstructured":"Henzinger, T. A., Jhala, R., Majumdar, R., and Sutre, G. (2003). Software verification with blast. In Proceedings of the Tenth International Workshop on Model Checking of Software (SPIN), pages 235\u2013239. Lecture Notes in Computer Science 2648, Springer-Verlag.","DOI":"10.1007\/3-540-44829-2_17"},{"issue":"2","key":"23_CR40","doi-asserted-by":"publisher","first-page":"72","DOI":"10.1002\/bltj.2223","volume":"5","author":"G. J. Holzmann","year":"2000","unstructured":"Holzmann, G. J. and Smith, M. H. (2000). Automating software feature verification. Bell Labs Technical Journal, 5(2):72\u201387.","journal-title":"Bell Labs Technical Journal"},{"issue":"3","key":"23_CR41","doi-asserted-by":"publisher","first-page":"155","DOI":"10.1016\/0020-0190(88)90054-3","volume":"29","author":"B. Korel","year":"1988","unstructured":"Korel, B. and Laski, J. (1988). Dynamic program slicing. Inf. Process. Lett., 29(3): 155\u2013163.","journal-title":"Inf. Process. Lett."},{"issue":"3","key":"23_CR42","doi-asserted-by":"publisher","first-page":"187","DOI":"10.1016\/0164-1212(90)90094-3","volume":"13","author":"B. Korel","year":"1990","unstructured":"Korel, B. and Laski, J. (1990). Dynamic slicing of computer programs. Journal of Systems and Software, 13(3):187\u2013195.","journal-title":"Journal of Systems and Software"},{"key":"23_CR43","doi-asserted-by":"publisher","first-page":"333","DOI":"10.1016\/0304-3975(82)90125-6","volume":"27","author":"D. Kozen","year":"1998","unstructured":"Kozen, D. (1998). Results on the propositional mu-calculus. In Theoretical Computer Science, volume 27, pages 333\u2013354.","journal-title":"Theoretical Computer Science"},{"key":"23_CR44","doi-asserted-by":"crossref","unstructured":"Kurshan, R. P. (1990). Analysis of discrete event coordination. In Proceedings on Stepwise refinement of distributed systems: models, formalisms, correctness, pages 414\u2013453.","DOI":"10.1007\/3-540-52559-9_74"},{"key":"23_CR45","unstructured":"Kurshan, R. P. (1994). Computer-aided verification of coordinating processes: the automatatheoretic approach. Princeton University Press."},{"key":"23_CR46","unstructured":"Lafuente, Alberto Lluch (2002). Database of promela models. http:\/\/www.informatik.uni-freiburg.de\/~lafuente\/models\/models.html."},{"key":"23_CR47","unstructured":"Lee, W., Pardo, A., Jang, J., Hachtel, G., and Somenzi, F. (1996). Tearing based automatic abstraction for ctl model checking. In Proceedings of the 1996 IEEE\/ACM international conference on Computer-aided design, pages 76\u201381."},{"key":"23_CR48","doi-asserted-by":"crossref","unstructured":"Lichtenstein, O. and Pnueli, A. (1985). Checking that finite state concurrent programs satisfy their linear specification. In Proceedings of the 12th ACM SIGACT-SIGPLAN symposium on Principles of programming languages, pages 97\u2013107.","DOI":"10.1145\/318593.318622"},{"key":"23_CR49","doi-asserted-by":"crossref","unstructured":"Lind-Nielsen, J. and Andersen, H. (1999). Stepwise CTL model checking of state\/event systems. In CAV\u201999: Computer Aided Verification.","DOI":"10.1007\/3-540-48683-6_28"},{"issue":"1","key":"23_CR50","doi-asserted-by":"publisher","first-page":"11","DOI":"10.1007\/BF01384313","volume":"6","author":"C. Loiseaux","year":"1995","unstructured":"Loiseaux, C., Graf, S., Sifakis, J., Bouajjani, A., and Bensalem, S. (1995). Property preserving abstractions for the verification of concurrent systems. Formal Methods in System Design, 6(1):11\u201344.","journal-title":"Formal Methods in System Design"},{"key":"23_CR51","doi-asserted-by":"crossref","unstructured":"Manna, Z. and Pnueli, A. (1992). The Temporal Logic of Reactive and Concurrent Systems: Specification. Springer-Verlag.","DOI":"10.1007\/978-1-4612-0931-7"},{"key":"23_CR52","unstructured":"Millett, L. and Teitelbaum, T. (1998). Slicing promela and its applications to model checking."},{"key":"23_CR53","unstructured":"Milner, R. (1971). An algebraic definition of simulation between programs. In Proceedings of the 2nd International Joint Conference on Artificial Intelligence., pages 481\u2013489."},{"issue":"1","key":"23_CR54","doi-asserted-by":"publisher","first-page":"2","DOI":"10.1109\/12.656068","volume":"47","author":"D. Moundanos","year":"1998","unstructured":"Moundanos, Dinos, Abraham, Jacob A., and Hoskote, Yatin V. (1998). Abstraction techniques for validation coverage analysis and test generation. IEEE Trans. Comput., 47(1):2\u201314.","journal-title":"IEEE Trans. Comput."},{"key":"23_CR55","doi-asserted-by":"crossref","unstructured":"Namjoshi, K. S. and Kurshan, R. P. (2000). Syntactic program transformations for automatic abstraction. In Computer Aided Verification, pages 435\u2013449.","DOI":"10.1007\/10722167_33"},{"issue":"5","key":"23_CR56","doi-asserted-by":"publisher","first-page":"177","DOI":"10.1145\/390011.808263","volume":"19","author":"K. J. Ottenstein","year":"1984","unstructured":"Ottenstein, K. J. and Ottenstein, L.M. (1984). The program dependence graph in software development environments. SIGPLAN Notices, 19(5):177\u2013184.","journal-title":"SIGPLAN Notices"},{"key":"23_CR57","doi-asserted-by":"crossref","unstructured":"Pardo, A. and Hachtel, G. (1998). Incremental CTL model checking using BDD subsetting. In Proceedings of the Design Automation Conference.","DOI":"10.1145\/277044.277171"},{"key":"23_CR58","unstructured":"Pardo, Abelardo (1997). Automatic Abstraction Techniques for Formal Verification of Digital Systems. PhD thesis, University of Colorado at Boulder."},{"key":"23_CR59","doi-asserted-by":"crossref","unstructured":"Park, D. (1981). Concurrency and automata on infinite sequences. In Proceedings of the 5th GI-Conference on Theoretical Computer Science, pages 167\u2013183. Springer-Verlag.","DOI":"10.1007\/BFb0017309"},{"key":"23_CR60","first-page":"68","volume":"407","author":"P. Wolfer","year":"1990","unstructured":"P. Wolfer and V. Lovinfosse (1990). Verifying properties of large sets of processes with network invariants. 407:68\u201380.","journal-title":"Verifying properties of large sets of processes with network invariants"},{"key":"23_CR61","doi-asserted-by":"crossref","first-page":"72","DOI":"10.1007\/3-540-63166-6_10","volume":"1254","author":"S. Graf","year":"1997","unstructured":"S. Graf and H. Saidi (1997). Construction of abstract state graphs with PVS. In Proc. 9th INternational Conference on Computer Aided Verification (CAV\u201997), volume 1254, pages 72\u201383.","journal-title":"Proc. 9th INternational Conference on Computer Aided Verification (CAV\u201997)"},{"key":"23_CR62","doi-asserted-by":"crossref","first-page":"458","DOI":"10.1007\/3-540-12896-4_381","volume":"164","author":"J. Sifakis","year":"1983","unstructured":"Sifakis, J. (1983). Property preserving homomorphisms of transition systems. Lecture Notes in Computer Science, 164:458\u2013473.","journal-title":"Lecture Notes in Computer Science"},{"key":"23_CR63","unstructured":"Tip, F. (1995). Generation of Program Analysis Tools. PhD thesis."},{"issue":"6","key":"23_CR64","first-page":"107","volume":"26","author":"G. A. Venkatesh","year":"1991","unstructured":"Venkatesh, G. A. (1991). The semantic approach to program slicing. ACM SIGPLAN Conf. on Programming Language Design and Implementation, 26(6):107\u2013119.","journal-title":"ACM SIGPLAN Conf. on Programming Language Design and Implementation"},{"key":"23_CR65","unstructured":"Weiser, M. (1979). Program slices: formal, psychological, and practical investigations of an automatic program abstraction method. PhD thesis."},{"issue":"4","key":"23_CR66","doi-asserted-by":"publisher","first-page":"352","DOI":"10.1109\/TSE.1984.5010248","volume":"10","author":"M. Weiser","year":"1984","unstructured":"Weiser, M. (1984). Program slicing. IEEE Transactions on Software Engineering, 10(4):352\u2013357.","journal-title":"IEEE Transactions on Software Engineering"}],"container-title":["IFIP International Federation for Information Processing","Building the Information Society"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-1-4020-8157-6_23.pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,1,29]],"date-time":"2025-01-29T15:02:26Z","timestamp":1738162946000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-1-4020-8157-6_23"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[null]]},"ISBN":["9781402081569","9781402081576"],"references-count":66,"URL":"https:\/\/doi.org\/10.1007\/978-1-4020-8157-6_23","relation":{},"subject":[]}}