{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,4,29]],"date-time":"2025-04-29T23:10:03Z","timestamp":1745968203720,"version":"3.40.4"},"reference-count":33,"publisher":"Springer Science and Business Media LLC","issue":"2","license":[{"start":{"date-parts":[[2013,3,3]],"date-time":"2013-03-03T00:00:00Z","timestamp":1362268800000},"content-version":"tdm","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["Int J Softw Tools Technol Transfer"],"published-print":{"date-parts":[[2013,4]]},"DOI":"10.1007\/s10009-013-0270-5","type":"journal-article","created":{"date-parts":[[2013,3,2]],"date-time":"2013-03-02T11:32:18Z","timestamp":1362223938000},"page":"85-88","source":"Crossref","is-referenced-by-count":2,"title":["Tools for software verification"],"prefix":"10.1007","volume":"15","author":[{"given":"Parosh Aziz","family":"Abdulla","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"K. Rustan M.","family":"Leino","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2013,3,3]]},"reference":[{"key":"270_CR1","doi-asserted-by":"crossref","unstructured":"Abdulla, P.A., \u010cer\u0101ns K., Jonsson, B., Tsay, Y-K.: General decidability theorems for infinite-state systems. In: Proceedings LICS \u201996, 11th IEEE International Symposium on Logic in Computer Science, pp. 313\u2013321. IEEE, Berlin (1996)","DOI":"10.1109\/LICS.1996.561359"},{"key":"270_CR2","doi-asserted-by":"crossref","unstructured":"Abdulla, P.A., Ben Henda, N., Delzanno, G., Rezine, A.: Regular model checking without transducers (on efficient verification of parameterized systems). In: Proceedings TACAS \u201907, 13th International Conference on Tools and Algorithms for the Construction and Analysis of Systems. Lecture Notes in Computer Science, vol. 4424, pp. 721\u2013736. Springer, Berlin (2007)","DOI":"10.1007\/978-3-540-71209-1_56"},{"key":"270_CR3","doi-asserted-by":"crossref","unstructured":"Abdulla, P.A.; Jonsson, B.: Verifying programs with unreliable channels. In: Proceeding LICS \u201993, 8th IEEE International Symposium on Logic in Computer Science, pp. 160\u2013170. IEEE, Berlin (1993)","DOI":"10.1109\/LICS.1993.287591"},{"key":"270_CR4","doi-asserted-by":"crossref","first-page":"183","DOI":"10.1016\/0304-3975(94)90010-8","volume":"126","author":"R Alur","year":"1994","unstructured":"Alur, R., Dill, D.: A theory of timed automata. Theor. Comput. Sci. 126, 183\u2013235 (1994)","journal-title":"Theor. Comput. Sci."},{"key":"270_CR5","doi-asserted-by":"crossref","unstructured":"Atig, M.F., Bouajjani, A., Burckhardt, S., Musuvathi, M.: On the verification problem for weak memory models. In: POPL, pp. 7\u201318. ACM, New York (2010)","DOI":"10.1145\/1707801.1706303"},{"key":"270_CR6","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. In: Integrated Formal Methods. LNCS, vol. 2999, pp. 1\u201320. Springer, Berlin (2004)","DOI":"10.1007\/978-3-540-24756-2_1"},{"key":"270_CR7","doi-asserted-by":"crossref","unstructured":"Ball, T., Majumdar, R., Millstein, T., Rajamani, S.K.: Automatic predicate abstraction of C programs. In: PLDI 2001, pp. 203\u2013213. ACM, New York (2001)","DOI":"10.1145\/381694.378846"},{"key":"270_CR8","doi-asserted-by":"crossref","unstructured":"Blanchet, B., Cousot, P., Cousot, R., Feret, J., Mauborgne, L., Min\u00e9, A., Monniaux, D., Rival, X.: A static analyzer for large safety-critical software. In: PLDI, pp. 196\u2013207. ACM, New York (2003)","DOI":"10.1145\/780822.781153"},{"key":"270_CR9","doi-asserted-by":"crossref","unstructured":"Bouajjani, A., Esparza, J., Maler, O.: Reachability Analysis of Pushdown Automata: Application to Model Checking. In: Proceedings International Conference on Concurrency Theory (CONCUR\u201997). LNCS, vol. 1243, pp. 135\u2013150. Springer, Berlin (1997)","DOI":"10.1007\/3-540-63141-0_10"},{"issue":"12","key":"270_CR10","doi-asserted-by":"crossref","first-page":"1035","DOI":"10.1109\/TC.1986.1676711","volume":"C\u201335","author":"MC Browne","year":"1986","unstructured":"Browne, M.C., Clarke, E.M., Dill, D.L., Mishra, B.: Automatic verification of sequential circuits using temporal logic. IEEE Trans. Comput. C\u201335(12), 1035\u20131044 (1986)","journal-title":"IEEE Trans. Comput."},{"issue":"8","key":"270_CR11","doi-asserted-by":"crossref","first-page":"677","DOI":"10.1109\/TC.1986.1676819","volume":"C\u201335","author":"RE Bryant","year":"1986","unstructured":"Bryant, R.E.: Graph-based algorithms for boolean function manipulation. IEEE Trans. Comput. C\u201335(8), 677\u2013691 (1986)","journal-title":"IEEE Trans. Comput."},{"key":"270_CR12","unstructured":"Burch, J.R., Clarke, E.M., McMillan, K.L., Dill, D.L., Hwang, L.J.: Symbolic model checking: $$10^{20}$$ states and beyond. Inform. Comput. 98(2), 142\u2013170 (1992)"},{"key":"270_CR13","doi-asserted-by":"crossref","unstructured":"Burkart, O., Steffen, B.: Model checking for context-free processes. In: CONCUR. LNCS, pp 123\u2013137. Springer, Berlin (1992)","DOI":"10.1007\/BFb0084787"},{"key":"270_CR14","doi-asserted-by":"crossref","unstructured":"Burkart, O., Steffen, B.: Pushdown processes: Parallel composition and model checking. In: CONCUR. LNCS, pp 98\u2013113. Springer, Berlin (1994)","DOI":"10.1007\/978-3-540-48654-1_9"},{"issue":"1","key":"270_CR15","doi-asserted-by":"crossref","first-page":"7","DOI":"10.1023\/A:1011276507260","volume":"19","author":"EM Clarke","year":"2001","unstructured":"Clarke, E.M., Biere, A., Raimi, R., Zhu, Y.: Bounded model checking using satisfiability solving. Form. Methods Syst. Des. 19(1), 7\u201334 (2001)","journal-title":"Form. Methods Syst. Des."},{"key":"270_CR16","doi-asserted-by":"crossref","unstructured":"Clarke, E.M., Grumberg, O., Jha, S., Lu, Y., Veith, H.: Counterexample-guided abstraction refinement. In: Proceeding 12th International Conference on Computer Aided Verification. Lecture Notes in Computer Science, vol. 1855. Springer, Berlin (2000)","DOI":"10.1007\/10722167_15"},{"key":"270_CR17","doi-asserted-by":"crossref","unstructured":"Clarke, E.M., Grumberg, O., Long, D.E.: Model checking and abstraction. In: Proceedings 19th ACM Symposium on Principles of Programming Languages, pp. 343\u2013354. ACM, New York (1992)","DOI":"10.1145\/143165.143235"},{"key":"270_CR18","doi-asserted-by":"crossref","first-page":"279","DOI":"10.1007\/s100090050035","volume":"2","author":"EM Clarke","year":"1999","unstructured":"Clarke, E.M., Grumberg, O., Minea, M., Peled, D.: State space reduction using partial order techniques. Softw. Tools Technol. Transf. 2, 279\u2013287 (1999)","journal-title":"Softw. Tools Technol. Transf."},{"key":"270_CR19","unstructured":"Clarke, E.M., Emerson, E.A.: Design and synthesis of synchronization skeletons using branching time temporal logic. In: Kozen D. (ed.) Proceeding IBM workshop on Logics of Programs. Lecture Notes in Computer Science, vol. 131. Springer, Berlin (1982)"},{"key":"270_CR20","doi-asserted-by":"crossref","first-page":"241","DOI":"10.1016\/0167-6423(83)90017-5","volume":"2","author":"EM Clarke","year":"1982","unstructured":"Clarke, E.M., Emerson, E.A.: Synthesis of synchronization skeletons using branching time temporal logic. Sci. Comput. Progr. 2, 241\u2013266 (1982)","journal-title":"Sci. Comput. Progr."},{"key":"270_CR21","doi-asserted-by":"crossref","unstructured":"Cousot, P., Cousot, R.: Abstract interpretation: A unified lattice model for static analysis of programs by construction or approximation of fixpoints. In: POPL, pp. 238\u2013252. ACM, New York (1977)","DOI":"10.1145\/512950.512973"},{"key":"270_CR22","doi-asserted-by":"crossref","unstructured":"de Moura, L., Bj\u00f8rner, N.: Satisfiability modulo theories: introduction and applications. Commun. ACM 54(9), 69\u201377 (2011)","DOI":"10.1145\/1995376.1995394"},{"key":"270_CR23","doi-asserted-by":"crossref","unstructured":"Esparza, J., Schwoon S.: A BDD-based model checker for recursive programs. In: Berry, Comon, Finkel (eds) Proceedings 13th International Conference on Computer Aided Verification. Lecture Notes in Computer Science, vol. 2102, pp. 324\u2013336. Springer, Berlin (2001)","DOI":"10.1007\/3-540-44585-4_30"},{"key":"270_CR24","doi-asserted-by":"crossref","unstructured":"Garavel, H., Lang, F., Mateescu, R., Serwe, W.: Cadp 2011: a tool-box for construction and analysis of distributed processes. Int J Softw Tools Technol Transfer (2013). doi: 10.1007\/s10009-012-0244-z","DOI":"10.1007\/s10009-012-0244-z"},{"key":"270_CR25","doi-asserted-by":"crossref","unstructured":"Godefroid, P.: Partial-Order Methods for the Verification of Concurrent Systems: An Approach to the State-Explosion Problem. PhD thesis, University of Li\u00e8ge. Lecture notes in Computer Science, vol. 1032. Springer, Berlin (1996)","DOI":"10.1007\/3-540-60761-7"},{"key":"270_CR26","doi-asserted-by":"crossref","unstructured":"Gordon, M.: Twenty years of theorem proving for HOL\u2019s past, present and future. In: TPHOLs. Lecture Notes in Computer Science, vol. 5170, pp. 1\u20135. Springer, Berlin (2008)","DOI":"10.1007\/978-3-540-71067-7_1"},{"key":"270_CR27","doi-asserted-by":"crossref","unstructured":"Jacobs, B., Piessens, F.: Expressive modular fine-grained concurrency specification. In: POPL, pp. 271\u2013282. ACM, New York (2011)","DOI":"10.1145\/1925844.1926417"},{"key":"270_CR28","doi-asserted-by":"crossref","unstructured":"Rustan, K., Leino, M., M\u00fcller, P.: A basis for verifying multi-threaded programs. In: ESOP. Lecture Notes in Computer Science, vol. 5502, pp. 378\u2013393. ACM, New York (2009)","DOI":"10.1007\/978-3-642-00590-9_27"},{"key":"270_CR29","doi-asserted-by":"crossref","unstructured":"Marques, A.P., Ravn, A.P., Srba, J., Vighio, S.: Model checking web services business activity protocol. Int J Softw Tools Technol Transfer (2013). doi: 10.1007\/s10009-012-0231-4","DOI":"10.1007\/s10009-012-0231-4"},{"key":"270_CR30","doi-asserted-by":"crossref","unstructured":"Queille, J.P., Sifakis, J.: Specification and verification of concurrent systems in CESAR. In: 5th International Symposium on Programming, Turin. Lecture Notes in Computer Science, vol. 137, pp. 337\u2013352. Springer, Berlin (1982)","DOI":"10.1007\/3-540-11494-7_22"},{"key":"270_CR31","doi-asserted-by":"crossref","unstructured":"Tsay, Y-K., Tsai, M-H., Chang, J-S., Chang, Y-W., Liu, C-S.: B\u00fcchi store: an open repository of $$\\omega $$ -automata. Int J Softw Tools Technol Transfer (2013). doi: 10.1007\/s10009-012-0268-4","DOI":"10.1007\/s10009-012-0268-4"},{"key":"270_CR32","doi-asserted-by":"crossref","unstructured":"Valmari, A.: Stubborn sets for reduced state space generation. In: Advances in Petri Nets. Lecture Notes in Computer Science, vol. 483, pp. 491\u2013515. Springer, Berlin (1990)","DOI":"10.1007\/3-540-53863-1_36"},{"key":"270_CR33","doi-asserted-by":"crossref","unstructured":"Wenzel M., Paulson L.C., Nipkow T.: The Isabelle framework. In: TPHOLs. Lecture Notes in Computer Science, vol. 5170, pp. 33\u201338. Springer, Berlin (2008)","DOI":"10.1007\/978-3-540-71067-7_7"}],"container-title":["International Journal on Software Tools for Technology Transfer"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s10009-013-0270-5.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/article\/10.1007\/s10009-013-0270-5\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s10009-013-0270-5","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,4,29]],"date-time":"2025-04-29T22:51:02Z","timestamp":1745967062000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/s10009-013-0270-5"}},"subtitle":["Introduction to the special section from the seventeenth international conference on tools and algorithms for the construction and analysis of systems"],"short-title":[],"issued":{"date-parts":[[2013,3,3]]},"references-count":33,"journal-issue":{"issue":"2","published-print":{"date-parts":[[2013,4]]}},"alternative-id":["270"],"URL":"https:\/\/doi.org\/10.1007\/s10009-013-0270-5","relation":{},"ISSN":["1433-2779","1433-2787"],"issn-type":[{"type":"print","value":"1433-2779"},{"type":"electronic","value":"1433-2787"}],"subject":[],"published":{"date-parts":[[2013,3,3]]}}}