{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,3,6]],"date-time":"2026-03-06T08:15:31Z","timestamp":1772784931914,"version":"3.50.1"},"reference-count":35,"publisher":"Springer Science and Business Media LLC","issue":"4","license":[{"start":{"date-parts":[[2012,12,9]],"date-time":"2012-12-09T00:00:00Z","timestamp":1355011200000},"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,8]]},"DOI":"10.1007\/s10009-012-0267-5","type":"journal-article","created":{"date-parts":[[2012,12,8]],"date-time":"2012-12-08T14:01:16Z","timestamp":1354975276000},"page":"291-303","source":"Crossref","is-referenced-by-count":10,"title":["From tests to proofs"],"prefix":"10.1007","volume":"15","author":[{"given":"Ashutosh Kumar","family":"Gupta","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Rupak","family":"Majumdar","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Andrey","family":"Rybalchenko","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2012,12,9]]},"reference":[{"key":"267_CR1","doi-asserted-by":"crossref","unstructured":"Ball, T., Rajamani, S.K.: The Slam project: Debugging system software via static analysis, In: Proc. POPL. ACM, pp. 1\u20133 (2002)","DOI":"10.1145\/565816.503274"},{"key":"267_CR2","doi-asserted-by":"crossref","unstructured":"Beyer, D., Henzinger, T., Majumdar, R., RybalchenkoA.: Invariant synthesis for combined theories. In: Proc. VMCAI. LNCS 4349. Springer, pp. 378\u2013394 (2007a)","DOI":"10.1007\/978-3-540-69738-1_27"},{"key":"267_CR3","doi-asserted-by":"crossref","unstructured":"Beyer, D., Henzinger, T. A., Majumdar, R., Rybalchenko, A.: Path invariants. In: Proc. PLDI. ACM Press, pp. 300\u2013309 (2007b)","DOI":"10.1145\/1273442.1250769"},{"key":"267_CR4","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: Proc. PLDI. ACM, pp. 196\u2013207 (2003)","DOI":"10.1145\/780822.781153"},{"key":"267_CR5","doi-asserted-by":"crossref","unstructured":"Col\u00f3n, M., Sankaranarayanan, S., Sipma, H.: Linear invariant generation using non-linear constraint solving. In: Proc. CAV. LNCS 2725. Springer, pp. 420\u2013432 (2003)","DOI":"10.1007\/978-3-540-45069-6_39"},{"key":"267_CR6","doi-asserted-by":"crossref","unstructured":"Cousot, P.: Proving program invariance and termination by parametric abstraction, lagrangian relaxation and semidefinite programming. In: Proc. VMCAI. Springer, pp. 1\u201324 (2005)","DOI":"10.1007\/978-3-540-30579-8_1"},{"key":"267_CR7","doi-asserted-by":"crossref","unstructured":"Cousot, P., Halbwachs, N.: Automatic discovery of linear restraints among variables of a program. In: POPL\u201978. ACM Press, pp. 84\u201396 (1978)","DOI":"10.1145\/512760.512770"},{"key":"267_CR8","doi-asserted-by":"crossref","unstructured":"de Moura, L.M., Bj\u00f8rner, N.: Z3: An efficient SMT solver. In: Proc. TACAS. LNCS 4963. Springer, pp. 337\u2013340 (2008)","DOI":"10.1007\/978-3-540-78800-3_24"},{"key":"267_CR9","doi-asserted-by":"crossref","unstructured":"Ernst, M.D., Cockrell, J., Griswold, W.G., Notkin, D.: Dynamically discovering likely program invariants to support program evolution. IEEE Trans. Software Eng. 27(2), 1\u201325 (2001)","DOI":"10.1109\/32.908957"},{"key":"267_CR10","doi-asserted-by":"crossref","unstructured":"Floyd, R.W.: Assigning meanings to programs. In: Mathematical Aspects of Computer Science. AMS, pp. 19\u201332 (1967)","DOI":"10.1090\/psapm\/019\/0235771"},{"key":"267_CR11","doi-asserted-by":"crossref","unstructured":"Godefroid, P.: Compositional dynamic test generation. In: Proc. POPL. ACM, pp. 47\u201354 (2007)","DOI":"10.1145\/1190215.1190226"},{"key":"267_CR12","doi-asserted-by":"crossref","unstructured":"Godefroid, P., Klarlund, N., Sen, K.: Dart: Directed automated random testing. In: Proc. PLDI. ACM, pp. 213\u2013223 (2005)","DOI":"10.1145\/1064978.1065036"},{"key":"267_CR13","doi-asserted-by":"crossref","unstructured":"Gonnord, L., Halbwachs, N.: Combining widening and acceleration in Linear Relation Analysis. In: Proc. SAS. LNCS 4134. Springer, pp. 144\u2013160 (2006)","DOI":"10.1007\/11823230_10"},{"key":"267_CR14","doi-asserted-by":"crossref","unstructured":"Gopan, D., Reps, T.: Lookahead widening. In: Proc. CAV. LNCS 4144. Springer, pp. 452\u2013466 (2006)","DOI":"10.1007\/11817963_41"},{"key":"267_CR15","doi-asserted-by":"crossref","unstructured":"Gulavani, B.S., Chakraborty, S., Nori, A.V., Rajamani, S.K.: Automatically refining abstract interpretations. In: Proc. TACAS. LNCS 4963. Springer, pp. 443\u2013458 (2008)","DOI":"10.1007\/978-3-540-78800-3_33"},{"key":"267_CR16","doi-asserted-by":"crossref","unstructured":"Gulwani, S., Srivastava, S., Venkatesan, R.: Program analysis as constraint solving. In: PLDI. ACM, pp. 281\u2013292 (2008)","DOI":"10.1145\/1375581.1375616"},{"key":"267_CR17","doi-asserted-by":"crossref","unstructured":"Gupta, A., Majumdar, R., Rybalchenko, A.: From tests to proofs. In: Proc. TACAS (2009)","DOI":"10.1007\/978-3-642-00768-2_24"},{"key":"267_CR18","doi-asserted-by":"crossref","unstructured":"Gupta, A., Rybalchenko, A.: InvGen: an efficient invariant generator. (2009) http:\/\/www7.in.tum.de\/guptaa\/invgen\/","DOI":"10.1007\/978-3-642-02658-4_48"},{"key":"267_CR19","doi-asserted-by":"crossref","unstructured":"Henzinger, T., Jhala, R., Majumdar, R., McMillan, K.: Abstractions from proofs. In: POPL 04: Principles of Programming Languages. ACM, pp. 232\u2013244 (2004)","DOI":"10.1145\/982962.964021"},{"key":"267_CR20","doi-asserted-by":"crossref","unstructured":"Henzinger, T., Jhala, R., Majumdar, R., Sutre, G.: Lazy abstraction. In: Proc. POPL. ACM, pp. 58\u201370 (2002)","DOI":"10.1145\/565816.503279"},{"key":"267_CR21","doi-asserted-by":"crossref","first-page":"576","DOI":"10.1145\/363235.363259","volume":"12","author":"CAR Hoare","year":"1969","unstructured":"Hoare, C.A.R.: An axiomatic basis for computer programming. Commun. ACM 12, 576\u2013580 (1969)","journal-title":"Commun. ACM"},{"key":"267_CR22","unstructured":"Holzbaur, C.: OFAI clp(q, r) Manual, Edition 1.3.3. Austrian Research Institute for Artificial Intelligence, Vienna, tR-95-09 (1995)"},{"key":"267_CR23","doi-asserted-by":"crossref","unstructured":"Jain, H., Ivancic, F., Gupta, A., Shlyakhter, I., Wang, C.: Using statically computed invariants inside the predicate abstraction and refinement loop. In: CAV. LNCS 4144. Springer, pp. 137\u2013151 (2006)","DOI":"10.1007\/11817963_15"},{"key":"267_CR24","unstructured":"Kapur, D.: Automatically generating loop invariants using quantifier elimination. Tech. Rep. 05431 (Deduction and Applications), IBFI Schloss Dagstuhl (2006)"},{"key":"267_CR25","doi-asserted-by":"crossref","unstructured":"Ku, K., Hart, T., Chechik, M., Lie, D.: A buffer overflow benchmark for software model checkers. In: Proc. ASE (2007)","DOI":"10.1145\/1321631.1321691"},{"key":"267_CR26","unstructured":"Lalire, G., Argoud, M., Jeannet, B.: The interproc analyzer (2009) http:\/\/pop-art.inrialpes.fr\/people\/bjeannet\/bjeannet-forge\/interproc\/index.html"},{"key":"267_CR27","doi-asserted-by":"crossref","unstructured":"Manna, Z., Pnueli, A.: Temporal Verification of Reactive Systems: Safety. Springer (1995)","DOI":"10.1007\/978-1-4612-4222-2"},{"key":"267_CR28","unstructured":"Min\u00e9, A.: The octagon abstract domain. Higher-Order and Symb. Comp. 19, 31\u2013100 (2006)"},{"key":"267_CR29","doi-asserted-by":"crossref","unstructured":"Necula, G. C., McPeak, S., Rahul, S. P., Weimer, W.: CIL: Intermediate language and tools for analysis and transformation of C programs. In: Proc. CC. Springer, pp. 213\u2013228 (2002)","DOI":"10.1007\/3-540-45937-5_16"},{"key":"267_CR30","doi-asserted-by":"crossref","unstructured":"Sankaranarayanan, S., Sipma, H., Manna, Z.: Constraint-based linear-relations analysis. In: Proc. SAS. LNCS 3148. Springer, pp. 53\u201368 (2004a)","DOI":"10.1007\/978-3-540-27864-1_7"},{"key":"267_CR31","doi-asserted-by":"crossref","unstructured":"Sankaranarayanan, S., Sipma, H., Manna, Z.: Non-linear loop invariant generation using Gr\u00f6bner bases. In: Proc. POPL. ACM, pp. 318\u2013329 (2004b)","DOI":"10.1145\/982962.964028"},{"key":"267_CR32","doi-asserted-by":"crossref","unstructured":"Sankaranarayanan, S., Sipma, H., Manna, Z.: Scalable analysis of linear systems using mathematical programming. In: Proc. VMCAI. LNCS 3385. Springer, pp. 25\u201341 (2005)","DOI":"10.1007\/978-3-540-30579-8_2"},{"key":"267_CR33","volume-title":"Theory of Linear and Integer Programming","author":"A Schrijver","year":"1986","unstructured":"Schrijver, A.: Theory of Linear and Integer Programming. Wiley, \u00a0 (1986)"},{"key":"267_CR34","doi-asserted-by":"crossref","unstructured":"Sen, K., Marinov, D., Agha, G.: Cute: A concolic unit testing engine for C. In: Proc. FSE. ACM, pp. 263\u2013272 (2005)","DOI":"10.21236\/ADA482657"},{"key":"267_CR35","unstructured":"The Intelligent Systems Laboratory.: SICStus Prolog User\u2019s Manual. Swedish Institute of Computer Science, release 3.8.7 (2001)"}],"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-012-0267-5.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/article\/10.1007\/s10009-012-0267-5\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s10009-012-0267-5","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,7,6]],"date-time":"2019-07-06T17:15:33Z","timestamp":1562433333000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/s10009-012-0267-5"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2012,12,9]]},"references-count":35,"journal-issue":{"issue":"4","published-print":{"date-parts":[[2013,8]]}},"alternative-id":["267"],"URL":"https:\/\/doi.org\/10.1007\/s10009-012-0267-5","relation":{},"ISSN":["1433-2779","1433-2787"],"issn-type":[{"value":"1433-2779","type":"print"},{"value":"1433-2787","type":"electronic"}],"subject":[],"published":{"date-parts":[[2012,12,9]]}}}