{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,1,30]],"date-time":"2026-01-30T05:28:37Z","timestamp":1769750917386,"version":"3.49.0"},"publisher-location":"Berlin, Heidelberg","reference-count":32,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"value":"9783642277047","type":"print"},{"value":"9783642277054","type":"electronic"}],"license":[{"start":{"date-parts":[[2012,1,1]],"date-time":"2012-01-01T00:00:00Z","timestamp":1325376000000},"content-version":"unspecified","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2012]]},"DOI":"10.1007\/978-3-642-27705-4_10","type":"book-chapter","created":{"date-parts":[[2012,1,25]],"date-time":"2012-01-25T12:18:06Z","timestamp":1327493886000},"page":"114-129","source":"Crossref","is-referenced-by-count":5,"title":["A Lightweight Technique for Distributed and Incremental Program Verification"],"prefix":"10.1007","author":[{"given":"Martin","family":"Brain","sequence":"first","affiliation":[]},{"given":"Florian","family":"Schanda","sequence":"additional","affiliation":[]}],"member":"297","reference":[{"key":"10_CR1","unstructured":"Altran Praxis: SPARK Pro. (2009), \n                  \n                    http:\/\/www.adacore.com\/home\/products\/sparkpro"},{"key":"10_CR2","unstructured":"Barnes, J.: High Integrity Software - The SPARK Approach to Saftey and Security, 2nd edn. Addison Wesley (2006)"},{"key":"10_CR3","doi-asserted-by":"publisher","first-page":"37","DOI":"10.1145\/2363.2366","volume":"7","author":"Bergeretti","year":"1985","unstructured":"Bergeretti, Carr\u00e9.: Information-flow and data-flow analysis of while programs. ACM Transactions on Programming Languages and Systems\u00a07, 37\u201361 (1985)","journal-title":"ACM Transactions on Programming Languages and Systems"},{"key":"10_CR4","unstructured":"Bergeretti, J.F.: An algebraic approach to program analysis: Foundations of a practical analysis system. Ph.D. thesis, University of Southampton, Faculty of Engineering and Applied Science, Department of Electronics (1979)"},{"key":"10_CR5","unstructured":"Berghofer, S.: Verification of Dependable Software using SPARK and Isabelle. In: Brauer, J., Roveri, M., Tews, H. (eds.) Proceedings of the 6th International Workshop on Systems Software Verification (SSV 2011). pp. 48\u201365. TU Dresden (August 2011); technical report TUDIFI11"},{"key":"10_CR6","unstructured":"Bobot, F., Filli\u00e2tre, J.C., March\u00e9, C., Paskevich, A.: Why3: Shepherd your herd of provers. In: Rustan, et al. [32], pp. 53\u201364"},{"key":"10_CR7","unstructured":"Brain, M., Schanda, F.: The Riposte counter example generator (2011), \n                  \n                    http:\/\/forge.open-do.org\/projects\/riposte"},{"key":"10_CR8","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"23","DOI":"10.1007\/978-3-642-03359-9_2","volume-title":"Theorem Proving in Higher Order Logics","author":"E. Cohen","year":"2009","unstructured":"Cohen, E., Dahlweid, M., Hillebrand, M., Leinenbach, D., Moskal, M., Santen, T., Schulte, W., Tobies, S.: Vcc: A Practical System for Verifying Concurrent C. In: Berghofer, S., Nipkow, T., Urban, C., Wenzel, M. (eds.) TPHOLs 2009. LNCS, vol.\u00a05674, pp. 23\u201342. Springer, Heidelberg (2009)"},{"key":"10_CR9","unstructured":"Conchon, S., Contejean, E., Kanig, J.: Ergo: A theorem prover for polymorphic first-order logic modulo theories (2006), \n                  \n                    http:\/\/ergo.lri.fr\/papers\/ergo.ps"},{"key":"10_CR10","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"449","DOI":"10.1007\/11513988_45","volume-title":"Computer Aided Verification","author":"C.L. Conway","year":"2005","unstructured":"Conway, C.L., Namjoshi, K.S., Dams, D., Edwards, S.A.: Incremental Algorithms for Inter-Procedural Analysis of Safety Properties. In: Etessami, K., Rajamani, S.K. (eds.) CAV 2005. LNCS, vol.\u00a03576, pp. 449\u2013461. Springer, Heidelberg (2005)"},{"key":"10_CR11","unstructured":"CVC3: An automatic theorem prover for Satisfiability Modulo Theories (SMT) (2006), \n                  \n                    http:\/\/www.cs.nyu.edu\/acsys\/cvc3"},{"issue":"7","key":"10_CR12","doi-asserted-by":"publisher","first-page":"1165","DOI":"10.1109\/TCAD.2008.923410","volume":"27","author":"V. D\u2019Silva","year":"2008","unstructured":"D\u2019Silva, V., Kroening, D., Weissenbacher, G.: A survey of automated techniques for formal software verification. IEEE Transactions on Computer-Aided Design of Integrated Circuits and Systems\u00a027(7), 1165\u20131178 (2008)","journal-title":"IEEE Transactions on Computer-Aided Design of Integrated Circuits and Systems"},{"key":"10_CR13","unstructured":"Dutertre, B., de\u00a0Moura, L.: The YICES SMT Solver (2006), \n                  \n                    http:\/\/yices.csl.sri.com\/tool-paper.pdf"},{"key":"10_CR14","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"109","DOI":"10.1007\/978-3-540-69611-7_7","volume-title":"Practical Aspects of Declarative Languages","author":"M. Eichberg","year":"2006","unstructured":"Eichberg, M., Kahl, M., Saha, D., Mezini, M., Ostermann, K.: Automatic Incrementalization of Prolog Based Static Analyses. In: Hanus, M. (ed.) PADL 2007. LNCS, vol.\u00a04354, pp. 109\u2013123. Springer, Heidelberg (2006)"},{"key":"10_CR15","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"173","DOI":"10.1007\/978-3-540-73368-3_21","volume-title":"Computer Aided Verification","author":"J.C. Filli\u00e2tre","year":"2007","unstructured":"Filli\u00e2tre, J.C., March\u00e9, C.: The Why\/Krakatoa\/Caduceus Platform for Deductive Program Verification. In: Damm, W., Hermanns, H. (eds.) CAV 2007. LNCS, vol.\u00a04590, pp. 173\u2013177. Springer, Heidelberg (2007)"},{"key":"10_CR16","unstructured":"Fitzpatrick, B., et\u00a0al.: Memcached - a distributed memory object caching system (2003), \n                  \n                    http:\/\/memcached.org"},{"key":"10_CR17","unstructured":"Gelernter, D., Carriero, N., Chandran, S., Chang, S.: Parallel programming in Linda. In: ICPP, pp. 255\u2013263 (1985)"},{"key":"10_CR18","unstructured":"Guitton, J., Kanig, J., Moy, Y.: Why hi-lite ada? In: Rustan, et al. [32], pp. 27\u201339"},{"key":"10_CR19","unstructured":"Hennessy, J.L., Patterson, D.: Computer Architecture, A Quantitative Approach, 4th edn. Morgan Kaufmann (2007)"},{"key":"10_CR20","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"332","DOI":"10.1007\/978-3-540-39910-0_16","volume-title":"Verification: Theory and Practice","author":"T.A. Henzinger","year":"2004","unstructured":"Henzinger, T.A., Jhala, R., Majumdar, R., Sanvido, M.A.A.: Extreme Model Checking. In: Dershowitz, N. (ed.) Verification: Theory and Practice. LNCS, vol.\u00a02772, pp. 332\u2013358. Springer, Heidelberg (2004)"},{"key":"10_CR21","doi-asserted-by":"publisher","first-page":"92","DOI":"10.1145\/1052883.1052895","volume":"39","author":"D. Hovemeyer","year":"2004","unstructured":"Hovemeyer, D., Pugh, W.: Finding bugs is easy. SIGPLAN Not.\u00a039, 92\u2013106 (2004), \n                  \n                    http:\/\/doi.acm.org\/10.1145\/1052883.1052895","journal-title":"SIGPLAN Not."},{"key":"10_CR22","unstructured":"Jackson, P.B., Passmore, G.O.: Proving SPARK Verification Conditions with SMT solvers (December 2009), \n                  \n                    http:\/\/homepages.inf.ed.ac.uk\/pbj\/papers\/vct-dec09-draft.pdf"},{"key":"10_CR23","doi-asserted-by":"crossref","unstructured":"James, P.R., Chalin, P.: Esc4: A modern caching ESC for Java. In: Huisman, M. (ed.) Proceedings of the 8th International Workshop on Specification and Verification of Component-Based Systems, pp. 19\u201326. Association for Computing Machinery (2009)","DOI":"10.1145\/1596486.1596491"},{"issue":"1-2","key":"10_CR24","doi-asserted-by":"publisher","first-page":"145","DOI":"10.1007\/s10817-009-9134-9","volume":"44","author":"P.R. James","year":"2010","unstructured":"James, P.R., Chalin, P.: Faster and more complete extended static checking for the java modeling language. Journal of Automated Reasoning\u00a044(1-2), 145\u2013174 (2010)","journal-title":"Journal of Automated Reasoning"},{"key":"10_CR25","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"509","DOI":"10.1007\/978-3-642-02658-4_38","volume-title":"Computer Aided Verification","author":"S.K. Lahiri","year":"2009","unstructured":"Lahiri, S.K., Qadeer, S., Rakamari\u0107, Z.: Static and Precise Detection of Concurrency Errors in Systems Code using SMT Solvers. In: Bouajjani, A., Maler, O. (eds.) CAV 2009. LNCS, vol.\u00a05643, pp. 509\u2013524. Springer, Heidelberg (2009)"},{"key":"10_CR26","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1145\/1127878.1127884","volume":"31","author":"G.T. Leavens","year":"2006","unstructured":"Leavens, G.T., Baker, A.L., Ruby, C.: Preliminary design of jml: a behavioral interface specification language for java. SIGSOFT Softw. Eng. Notes\u00a031, 1\u201338 (2006), \n                  \n                    http:\/\/doi.acm.org\/10.1145\/1127878.1127884","journal-title":"SIGSOFT Softw. Eng. Notes"},{"key":"10_CR27","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"348","DOI":"10.1007\/978-3-642-17511-4_20","volume-title":"Logic for Programming, Artificial Intelligence, and Reasoning","author":"K. Leino","year":"2010","unstructured":"Leino, K.: Dafny: An Automatic Program Verifier for Functional Correctness. In: Clarke, E.M., Voronkov, A. (eds.) LPAR-16 2010. LNCS, vol.\u00a06355, pp. 348\u2013370. Springer, Heidelberg (2010)"},{"key":"10_CR28","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"340","DOI":"10.1007\/978-3-642-18275-4_24","volume-title":"Verification, Model Checking, and Abstract Interpretation","author":"N.P. Lopes","year":"2011","unstructured":"Lopes, N.P., Rybalchenko, A.: Distributed and Predictable Software Model Checking. In: Jhala, R., Schmidt, D. (eds.) VMCAI 2011. LNCS, vol.\u00a06538, pp. 340\u2013355. Springer, Heidelberg (2011)"},{"key":"10_CR29","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"337","DOI":"10.1007\/978-3-540-78800-3_24","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"L. Moura de","year":"2008","unstructured":"de Moura, L., Bj\u00f8rner, N.S.: Z3: An Efficient SMT Solver. In: Ramakrishnan, C.R., Rehof, J. (eds.) TACAS 2008. LNCS, vol.\u00a04963, pp. 337\u2013340. Springer, Heidelberg (2008)"},{"key":"10_CR30","unstructured":"Moy, Y.: Automatic Modular Static Safety Checking for C Programs. Ph.D. thesis, Universit\u00e9 Paris-Sud (January 2009)"},{"key":"10_CR31","unstructured":"Ranise, S., Tinelli, C.: The SMT-LIB format: An initial proposal. In: Workshop on Pragmatics of Decision Procedures in Automated Reasoning (2003)"},{"key":"10_CR32","unstructured":"Rustan, K., Leino, M., Moskal, M. (eds.): First International Workshop on Intermediate Verification Languages (August 2011)"}],"container-title":["Lecture Notes in Computer Science","Verified Software: Theories, Tools, Experiments"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-642-27705-4_10","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,4,25]],"date-time":"2019-04-25T12:39:11Z","timestamp":1556195951000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-642-27705-4_10"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2012]]},"ISBN":["9783642277047","9783642277054"],"references-count":32,"URL":"https:\/\/doi.org\/10.1007\/978-3-642-27705-4_10","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[2012]]}}}