乐胖代购免代理版

{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,7,15]],"date-time":"2024-07-15T00:21:21Z","timestamp":1721002881177},"reference-count":44,"publisher":"Pleiades Publishing Ltd","issue":"8","license":[{"start":{"date-parts":[[2020,12,1]],"date-time":"2020-12-01T00:00:00Z","timestamp":1606780800000},"content-version":"tdm","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"},{"start":{"date-parts":[[2020,12,1]],"date-time":"2020-12-01T00:00:00Z","timestamp":1606780800000},"content-version":"vor","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":["Program Comput Soft"],"published-print":{"date-parts":[[2020,12]]},"DOI":"10.1134\/s0361768820080022","type":"journal-article","created":{"date-parts":[[2020,12,22]],"date-time":"2020-12-22T12:03:01Z","timestamp":1608638581000},"page":"712-730","update-policy":"http:\/\/dx.doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":8,"title":["Analysis of Correct Synchronization of Operating System Components"],"prefix":"10.1134","volume":"46","author":[{"given":"P. S.","family":"Andrianov","sequence":"first","affiliation":[]}],"member":"137","published-online":{"date-parts":[[2020,12,22]]},"reference":[{"key":"3561_CR1","doi-asserted-by":"publisher","first-page":"373","DOI":"10.1145\/2578855.2535845","volume":"49","author":"P. Abdulla","year":"2014","unstructured":"Abdulla, P., Aronis, S., Jonsson, B., and Sagonas, K., Optimal dynamic partial order reduction, SIGPLAN Not., 2014, vol. 49, no. 1, pp. 373\u2013384.","journal-title":"SIGPLAN Not."},{"key":"3561_CR2","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-60761-7","volume-title":"Partial-Order Methods for the Verification of Concurrent Systems: an Approach to the State-Explosion Problem","author":"P. Godefroid","year":"1996","unstructured":"Godefroid, P., Partial-Order Methods for the Verification of Concurrent Systems: an Approach to the State-Explosion Problem, Berlin, Heidelberg: Springer-Verlag, 1996."},{"key":"3561_CR3","doi-asserted-by":"crossref","unstructured":"Basler, G., Mazzucchi, M., Wahl, T., and Kroening, D., Symbolic counter abstraction for concurrent software, in Proc. 21st Int. Conf. on Computer Aided Verification, CAV\u201909, Berlin, Heidelberg: Springer-Verlag, 2009, pp.\u00a064\u201378.","DOI":"10.1007\/978-3-642-02658-4_9"},{"key":"3561_CR4","unstructured":"Beyer, D., Automatic verification of C and Java programs: SV-COMP 2019, in Tools and Algorithms for the Construction and Analysis of Systems, Beyer, D. Huisman, M. Kordon, F. and Steffen, B., Eds., Cham: Springer Int. Publ., 2019, pp. 133\u2013155."},{"key":"3561_CR5","doi-asserted-by":"crossref","unstructured":"Beyer, D., Henzinger, T.A., and Theoduloz, G., Program analysis with dynamic precision adjustment, in Proc. 23rd IEEE\/ACM Int. Conf. on Automated Software Engineering, ASE 2008, L\u2019Aquila, Sept. 2008, pp. 29\u201338.","DOI":"10.1109\/ASE.2008.13"},{"key":"3561_CR6","doi-asserted-by":"crossref","unstructured":"Flanagan C. and Qadeer, S., Thread-modular model checking, in Proc. 10th Int. Conf. on Model Checking Software, SPIN\u201903, Berlin, Heidelberg: Springer-Verlag, 2003, pp. 213\u2013224.","DOI":"10.1007\/3-540-44829-2_14"},{"key":"3561_CR7","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-45069-6_27","volume-title":"Thread-Modular Abstraction Refinement","author":"T. A. Henzinger","year":"2003","unstructured":"Henzinger, T. A., Jhala, R., Majumdar, R., and Qadeer, S., Thread-Modular Abstraction Refinement, Berlin, Heidelberg: Springer, 2003, pp. 262\u2013274."},{"key":"3561_CR8","doi-asserted-by":"publisher","first-page":"227","DOI":"10.1016\/j.tcs.2007.07.050","volume":"388","author":"B. Cook","year":"2007","unstructured":"Cook, B., Kroening, D., and Sharygina, N., Verification of boolean programs with unbounded thread creation, Theor. Comput. Sci., 2007, vol. 388, no. 1\u20133, pp.\u00a0227\u2013242.","journal-title":"Theor. Comput. Sci."},{"key":"3561_CR9","doi-asserted-by":"crossref","unstructured":"Gupta, A., Popeea, C., and Rybalchenko, A., Threader, a constraint-based verifier for multi-threaded programs, in Proc. 23rd Int. Conf. on Computer Aided Verification, CAV\u201911, Berlin, Heidelberg: Springer-Verlag, 2011, pp. 412\u2013417.","DOI":"10.1007\/978-3-642-22110-1_32"},{"key":"3561_CR10","doi-asserted-by":"crossref","unstructured":"Clarke, E.M., Grumberg, O., Jha, S., Lu, Y., and Veith, H., Counter example-guided abstraction refinement, Proc. CAV 2000: Computer Aided Verification, Chicago, 2000, pp. 154\u2013169.","DOI":"10.1007\/10722167_15"},{"key":"3561_CR11","series-title":"Construction of abstract state graphs with PVS","volume-title":"Computer Aided Verification","author":"S. Graf","year":"1997","unstructured":"Graf S. and Saidi, H., Construction of abstract state graphs with PVS, in Computer Aided Verification, Grumberg, O., Ed., Berlin, Heidelberg: Springer, 1997, pp. 72\u201383."},{"key":"3561_CR12","doi-asserted-by":"publisher","first-page":"27","DOI":"10.1145\/269005.266641","volume":"31","author":"S. Savage","year":"1997","unstructured":"Savage, S., Burrows, M., Nelson, G., Sobalvarro, P., and Anderson, T., Eraser: a dynamic data race detector for multi-threaded programs, SIGOPS Oper. Syst. Rev., 1997, vol. 31, no. 5, pp. 27\u201337.","journal-title":"SIGOPS Oper. Syst. Rev."},{"key":"3561_CR13","doi-asserted-by":"crossref","unstructured":"Bornat, R., Proving pointer programs in Hoare logic, in Proc. 5th Int. Conf. on Mathematics of Program Construction, MPC\u201900, London: Springer-Verlag, 2000, pp.\u00a0102\u2013126.","DOI":"10.1007\/10722010_8"},{"key":"3561_CR14","series-title":"Some techniques for proving correctness of programs which alter data structures","volume-title":"Machine Intelligence 7","author":"R.M. Burstall","year":"1972","unstructured":"Burstall, R.M., Some techniques for proving correctness of programs which alter data structures, in Machine Intelligence 7, Michie, D., Ed., New York: American Elsevier, 1972, pp. 23\u201350."},{"key":"3561_CR15","series-title":"CPA-BAM-BnB: block-abstraction memoization and region-based memory models for predicate abstractions","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"P. Andrianov","year":"2017","unstructured":"Andrianov, P., Friedberger, K., Mandrykin, M., Mutilin, V., and Volkov, A., CPA-BAM-BnB: block-abstraction memoization and region-based memory models for predicate abstractions, in Tools and Algorithms for the Construction and Analysis of Systems, Legay, A. and Margaria, T., Eds., Berlin, Heidelberg: Springer, 2017, pp. 355\u2013359."},{"key":"3561_CR16","series-title":"Towards automated static veri_cation of GNU C programs","volume-title":"Perspectives of System Informatics","author":"E. Novikov","year":"2018","unstructured":"Novikov, E. and Zakharov, I., Towards automated static veri_cation of GNU C programs, in Perspectives of System Informatics, Petrenko, A.K. and Voronkov, A., Eds., Cham: Springer Int. Publ., 2018, pp. 402\u2013416."},{"key":"3561_CR17","series-title":"Verification of operating system monolithic kernels without extensions","volume-title":"Leveraging Applications of Formal Methods, Verification and Validation. Industrial Practice","author":"E. Novikov","year":"2018","unstructured":"Novikov, E. and Zakharov, I., Verification of operating system monolithic kernels without extensions, in Leveraging Applications of Formal Methods, Verification and Validation. Industrial Practice, Margaria, T. and Steffen, B., Eds., Cham: Springer Int. Publ., 2018, pp.\u00a0230\u2013248."},{"key":"#cr-split#-3561_CR18.1","unstructured":"Beyer, D. and Friedberger, K., A light-weight approach for verifying multithreaded programs with CPAchecker, in Proc. 11th Doctoral Workshop on Mathematical and Engineering Methods in Computer Science (MEMICS 2016) Tel\u010d, Czechia, Oct. 21-23,"},{"key":"#cr-split#-3561_CR18.2","unstructured":"2016, Bouda, J., Hol\u00edk, L., Kofro\u00f1, J., Strej\u010dek, J., and Rambousek, A., Eds., 2016, pp. 61-71."},{"key":"#cr-split#-3561_CR19.1","doi-asserted-by":"crossref","unstructured":"Beyer, D. and L\u00f6we, S., Explicit-state software model checking based on CEGAR and interpolation, in Proc. 16th Int. Conf. on Fundamental Approaches to Software Engineering (FASE 2013, Rome, Italy, March 20-22,","DOI":"10.1007\/978-3-642-37057-1_11"},{"key":"#cr-split#-3561_CR19.2","unstructured":"2013), Heidelberg: Springer-Verlag, 2013, pp. 146-162."},{"key":"3561_CR20","unstructured":"Beyer, D., Keremoglu, M.E., and Wendler, P., Predicate abstraction with adjustableblock encoding, Proc. Formal Methods in Computer-Aided Design, FMCAD 2010, Lugano, 2010."},{"key":"3561_CR21","doi-asserted-by":"crossref","unstructured":"Biere, A., Cimatti, A., Clarke, E.M., and Zhu, Y., Symbolic model checking without bdds, in Proc. 5th Int. Conf. on Tools and Algorithms for Construction and Analysis of Systems, TACAS\u201999, London: Springer-Verlag, 1999, pp. 193\u2013207.","DOI":"10.1007\/3-540-49059-0_14"},{"key":"3561_CR22","unstructured":"Beyer, D., Henzinger, T.A., and Th\u00e9oduloz, G., Configurable software verification: concretizing the convergence of model checking and program analysis, in Proc. CAV, Berlin, Heidelberg: Springer-Verlag, 2007, pp.\u00a0504\u2013518."},{"key":"3561_CR23","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1007\/s10009-017-0469-y","volume":"21","author":"D. Beyer","year":"2019","unstructured":"Beyer, D., L\u00f6we, S., and Wendler, P., Reliable benchmarking: requirements and solutions. Int. J. Software Tools Technol. Transfer, 2019, vol. 21, no. 1, pp. 1\u201329.","journal-title":"Int. J. Software Tools Technol. Transfer"},{"key":"3561_CR24","series-title":"Context-bounded model checking of concurrent software","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"S. Qadeer","year":"2005","unstructured":"Qadeer S. and Rehof, J., Context-bounded model checking of concurrent software, in Tools and Algorithms for the Construction and Analysis of Systems, Halbwachs, N. and Zuck, L.D., Eds., Berlin, Heidelberg: Springer, 2005, pp. 93\u2013107."},{"key":"3561_CR25","doi-asserted-by":"crossref","unstructured":"Cordeiro, L., Morse, J., Nicole, D., and Fischer, B., Context-bounded model checking with esbmc 1.17, in Proc. 18th Int. Conf. on Tools and Algorithms for the Construction and Analysis of Systems, TACAS\u201912, Berlin, Heidelberg: Springer-Verlag, 2012, pp. 534\u2013537.","DOI":"10.1007\/978-3-642-28756-5_42"},{"key":"3561_CR26","doi-asserted-by":"publisher","first-page":"104","DOI":"10.1007\/s10703-008-0063-8","volume":"34","author":"A. Cohen","year":"2009","unstructured":"Cohen, A. and Namjoshi, K.S., Local proofs for global safety properties, Formal Methods Syst. Des., 2009, vol.\u00a034, no. 2, pp. 104\u2013125.","journal-title":"Formal Methods Syst. Des."},{"key":"3561_CR27","doi-asserted-by":"crossref","unstructured":"Henzinger, T.A., Jhala, R., and Majumdar, R., Race checking by context inference, in Proc. ACM SIGPLAN 2004 Conf. on Programming Language Design and Implementation, PLDI\u201904, New York: ACM, 2004, pp. 1\u201313.","DOI":"10.1145\/996841.996844"},{"key":"3561_CR28","series-title":"Thread-modular verification is cartesian abstract interpretation","volume-title":"Proc. Theoretical Aspects of Computing \u2013 ICTAC 2006","author":"A. Malkis","year":"2006","unstructured":"Malkis, A., Podelski, A., and Rybalchenko, A., Thread-modular verification is cartesian abstract interpretation, in Proc. Theoretical Aspects of Computing \u2013 ICTAC 2006, Barkaoui, K., Cavalcanti, A., and Cerone, A., Eds., Berlin, Heidelberg: Springer, 2006, pp.\u00a0183\u2013197."},{"key":"3561_CR29","doi-asserted-by":"publisher","first-page":"331","DOI":"10.1145\/1925844.1926424","volume":"46","author":"A. Gupta","year":"2011","unstructured":"Gupta, A., Popeea, C., and Rybalchenko, A., Predicate abstraction and refinement for verifying multi-threaded programs, SIGPLAN Not., 2011, vol. 46, no. 1, pp.\u00a0331\u2013344.","journal-title":"SIGPLAN Not."},{"key":"3561_CR30","doi-asserted-by":"publisher","first-page":"73","DOI":"10.1007\/s10703-009-0078-9","volume":"35","author":"A. Lal","year":"2009","unstructured":"Lal, A. and Reps, T., Reducing concurrent analysis under a context bound tosequential analysis, Formal Methods Syst. Des., 2009, vol. 35, no. 1, pp. 73\u201397.","journal-title":"Formal Methods Syst. Des."},{"key":"3561_CR31","series-title":"Reducing contextbounded concurrent reachability to sequential reachability","volume-title":"Computer Aided Verification","author":"S. La Torre","year":"2009","unstructured":"La Torre, S., Madhusudan, P., and Parlato, G., Reducing contextbounded concurrent reachability to sequential reachability, in Computer Aided Verification, Bouajjani, A. and Maler, O., Eds., Berlin, Heidelberg: Springer, 2009, pp. 477\u2013492."},{"key":"3561_CR32","series-title":"MU-CSeq: sequentialization of C programs by shared memory unwindings","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"E. Tomasco","year":"2014","unstructured":"Tomasco, E., Inverso, O., Fischer, B., La Torre, S., and Parlato, G., MU-CSeq: sequentialization of C programs by shared memory unwindings, in Tools and Algorithms for the Construction and Analysis of Systems, \u00c1brah\u00e1m, E. and Havelund, K., Eds., Berlin, Heidelberg: Springer, 2014, pp. 402\u2013404."},{"key":"3561_CR33","doi-asserted-by":"crossref","unstructured":"Deligiannis, P., Donaldson, A.F., and Rakamaric, Z., Fast and precise symbolic analysis of concurrency bugs in device drivers (t), in Proc. 30th IEEE\/ACM Int. Conf. on Automated Software Engineering, ASE\u201915, Washington: IEEE Computer Soc., 2015, pp. 166\u2013177.","DOI":"10.1109\/ASE.2015.30"},{"key":"3561_CR34","doi-asserted-by":"crossref","unstructured":"Lal, A., Qadeer, S., and Lahiri, S.K., A solver for reachability modulo theories, in Proc. 24th Int. Conf. on Computer Aided Verification, CAV\u201912, Berlin, Heidelberg: Springer-Verlag, 2012, pp. 427\u2013443.","DOI":"10.1007\/978-3-642-31424-7_32"},{"key":"3561_CR35","unstructured":"Voung, J.W., Jhala, R., and Lerner, S., RELAY: static race detection on millions of lines of code, in Proc. 6th Joint Meeting of the European Software Engineering Conf. and the ACM SIGSOFT Symp. on the Foundations of Software Engineering, ESEC-FSE\u201907, New York: ACM, 2007, pp. 205\u2013214."},{"key":"3561_CR36","unstructured":"Pratikakis, P., Foster, J.S., and Hicks, M., LOCKSMITH: context sensitive correlation analysis for race detection, in Proc. 27th ACM SIGPLAN Conf. on Programming Language Design and Implementation, PLDI\u201906, New York: ACM, 2006, pp. 320\u2013331."},{"key":"3561_CR37","doi-asserted-by":"crossref","unstructured":"Di, P. and Sui, Y., Accelerating dynamic data race detection using static thread interference analysis, in Proc. 7th Int. Workshop on Programming Models and Applications for Multicores and Manycores, PMAM\u201916, New York: ACM, 2016, pp. 30\u201339.","DOI":"10.1145\/2883404.2883405"},{"key":"3561_CR38","doi-asserted-by":"crossref","unstructured":"Kroening, D., Liang, L., Melham, T., Schrammel, P., and Tautschnig, M., Effective verification of low-level software with nested interrupts, Proc. ACM Design, Automation & Test in Europe Conf. & Exhibition (DATE 2015), Grenoble, March 2015, pp. 229\u2013234.","DOI":"10.7873\/DATE.2015.0360"},{"key":"3561_CR39","series-title":"Detecting all high-level dataraces in an RTOS kernel","volume-title":"Verification, Model Checking, and Abstract Interpretation","author":"S. Mukherjee","year":"2017","unstructured":"Mukherjee, S., Kumar, A., and D\u2019Souza, D., Detecting all high-level dataraces in an RTOS kernel, in Verification, Model Checking, and Abstract Interpretation, Bouajjani, A. and Monniaux, D., Eds., Cham: Springer Int. Publ., 2017, pp. 405\u2013423."},{"key":"3561_CR40","series-title":"Data races and static analysis for interrupt-driven kernels","volume-title":"Programming Languages and Systems","author":"N. Chopra","year":"2019","unstructured":"Chopra, N., Pai, R., and D\u2019Souza, D., Data races and static analysis for interrupt-driven kernels, in Programming Languages and Systems, Caires, L., Ed., Cham: Springer Int. Publ., 2019, pp. 697\u2013723."},{"key":"3561_CR41","unstructured":"Bai, J.-J., Lawall, J., Chen, Q.-L., and Hu, S.-M., Effective static analysis of concurrency use-after-free bugs in Linux device drivers, in Proc. USENIX Annu. Technical Conf. (USENIX ATC 19), Renton, WA: USENIX Assoc., July 2019, pp. 255\u2013268."},{"key":"3561_CR42","doi-asserted-by":"crossref","unstructured":"Beyer, D., Jakobs, M.-C., Lemberger, T., and Wehrheim, H., Reducer-based construction of conditional verifiers, in Proc. 40th Int. Conf. on Software Engineering, ICSE\u201918, New York: ACM, 2018, pp. 1182\u20131193.","DOI":"10.1145\/3180155.3180259"}],"container-title":["Programming and Computer Software"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1134\/S0361768820080022.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/article\/10.1134\/S0361768820080022\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1134\/S0361768820080022.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2020,12,22]],"date-time":"2020-12-22T12:08:51Z","timestamp":1608638931000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1134\/S0361768820080022"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2020,12]]},"references-count":44,"journal-issue":{"issue":"8","published-print":{"date-parts":[[2020,12]]}},"alternative-id":["3561"],"URL":"https:\/\/doi.org\/10.1134\/s0361768820080022","relation":{},"ISSN":["0361-7688","1608-3261"],"issn-type":[{"value":"0361-7688","type":"print"},{"value":"1608-3261","type":"electronic"}],"subject":[],"published":{"date-parts":[[2020,12]]},"assertion":[{"value":"13 February 2020","order":1,"name":"received","label":"Received","group":{"name":"ArticleHistory","label":"Article History"}},{"value":"10 March 2020","order":2,"name":"revised","label":"Revised","group":{"name":"ArticleHistory","label":"Article History"}},{"value":"2 April 2020","order":3,"name":"accepted","label":"Accepted","group":{"name":"ArticleHistory","label":"Article History"}},{"value":"22 December 2020","order":4,"name":"first_online","label":"First Online","group":{"name":"ArticleHistory","label":"Article History"}}]}}