{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,11,18]],"date-time":"2025-11-18T12:14:13Z","timestamp":1763468053945},"publisher-location":"Berlin, Heidelberg","reference-count":28,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783642288906"},{"type":"electronic","value":"9783642288913"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2012]]},"DOI":"10.1007\/978-3-642-28891-3_15","type":"book-chapter","created":{"date-parts":[[2012,3,30]],"date-time":"2012-03-30T08:53:01Z","timestamp":1333097581000},"page":"147-161","source":"Crossref","is-referenced-by-count":23,"title":["PVS Linear Algebra Libraries for Verification of Control Software Algorithms in C\/ACSL"],"prefix":"10.1007","author":[{"given":"Heber","family":"Herencia-Zapana","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Romain","family":"Jobredeaux","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Sam","family":"Owre","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Pierre-Lo\u00efc","family":"Garoche","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Eric","family":"Feron","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Gilberto","family":"Perez","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Pablo","family":"Ascariz","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","reference":[{"key":"15_CR1","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"23","DOI":"10.1007\/978-3-642-11957-6_3","volume-title":"Programming Languages and Systems","author":"A. Adj\u00e9","year":"2010","unstructured":"Adj\u00e9, A., Gaubert, S., Goubault, E.: Coupling Policy Iteration with Semi-definite Relaxation to Compute Accurate Numerical Invariants in Static Analysis. In: Gordon, A.D. (ed.) ESOP 2010. LNCS, vol.\u00a06012, pp. 23\u201342. Springer, Heidelberg (2010)"},{"key":"15_CR2","unstructured":"Ahn, K.Y., Denney, E.: Testing first-order logic axioms in program verification"},{"key":"15_CR3","unstructured":"Alegre, F., Feron, E., Pande, S.: Using ellipsoidal domains to analyze control systems software. CoRR abs\/0909.1977 (2009)"},{"key":"15_CR4","doi-asserted-by":"crossref","DOI":"10.1007\/b97662","volume-title":"Linear Algebra Done Right","author":"S. Axler","year":"1997","unstructured":"Axler, S.: Linear Algebra Done Right, 2nd edn. Springer, Heidelberg (1997)","edition":"2"},{"key":"15_CR5","unstructured":"Baudin, P., Filli\u00e2tre, J.C., March\u00e9, C., Monate, B., Moy, Y., Prevosto, V.: ACSL: ANSI\/ISOC specification language. Preliminary design (version 1.5)"},{"key":"15_CR6","doi-asserted-by":"crossref","unstructured":"Boyd, S., El Ghaoui, L., Feron, E., Balakrishnan, V.: Linear Matrix Inequalities in System and Control Theory. Studies in Applied Mathematics, vol.\u00a015. SIAM (June 1994)","DOI":"10.1137\/1.9781611970777"},{"key":"15_CR7","unstructured":"Burghardt, J., Gerlach, J., Hartig, K.: ACSL by example towards a verified C standard library version 4.2.0 for Frama-C beryllium 2 (2010)"},{"key":"15_CR8","volume-title":"Linear System Theory and Design","author":"C.T. Chen","year":"1998","unstructured":"Chen, C.T.: Linear System Theory and Design, 3rd edn. Oxford University Press, USA (1998)","edition":"3"},{"key":"15_CR9","unstructured":"Correnson, L., Cuoq, P., Puccetti, A., Signoles, J.: Frama-C user manual"},{"key":"15_CR10","unstructured":"Dijkstra, E.: A Discipline of Programming. Prentice-Hall (1976)"},{"issue":"2","key":"15_CR11","doi-asserted-by":"publisher","first-page":"242","DOI":"10.1109\/TC.2010.128","volume":"60","author":"F. Dinechin de","year":"2011","unstructured":"de Dinechin, F., Quirin Lauter, C., Melquiond, G.: Certifying the floating-point implementation of an elementary function using Gappa. IEEE Trans. Computers\u00a060(2), 242\u2013253 (2011)","journal-title":"IEEE Trans. Computers"},{"key":"15_CR12","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"24","DOI":"10.1007\/978-3-642-16901-4_4","volume-title":"Formal Methods and Software Engineering","author":"J. Eriksson","year":"2010","unstructured":"Eriksson, J., Back, R.-J.: Applying PVS Background Theories and Proof Strategies in Invariant Based Programming. In: Dong, J.S., Zhu, H. (eds.) ICFEM 2010. LNCS, vol.\u00a06447, pp. 24\u201339. Springer, Heidelberg (2010)"},{"key":"15_CR13","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"33","DOI":"10.1007\/978-3-540-24725-8_4","volume-title":"Programming Languages and Systems","author":"J. Feret","year":"2004","unstructured":"Feret, J.: Static Analysis of Digital Filters. In: Schmidt, D. (ed.) ESOP 2004. LNCS, vol.\u00a02986, pp. 33\u201348. Springer, Heidelberg (2004)"},{"key":"15_CR14","doi-asserted-by":"crossref","unstructured":"Feron, E.: From control systems to control software. IEEE Control Systems\u00a030(6) (2010)","DOI":"10.1109\/MCS.2010.938196"},{"key":"15_CR15","unstructured":"Feron, E., Alegre, F.: Control software analysis, part I open-loop properties. CoRR abs\/0809.4812 (2008)"},{"key":"15_CR16","unstructured":"Friedberg, S., Insel, A., Spence, L.: Linear Algebra, 3rd edn. Prentice-Hall (1997)"},{"key":"15_CR17","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"327","DOI":"10.1007\/978-3-642-03359-9_23","volume-title":"Theorem Proving in Higher Order Logics","author":"F. Garillot","year":"2009","unstructured":"Garillot, F., Gonthier, G., Mahboubi, A., Rideau, L.: Packaging Mathematical Structures. In: Berghofer, S., Nipkow, T., Urban, C., Wenzel, M. (eds.) TPHOLs 2009. LNCS, vol.\u00a05674, pp. 327\u2013342. Springer, Heidelberg (2009), http:\/\/hal.inria.fr\/inria-00368403\/en\/"},{"key":"15_CR18","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"103","DOI":"10.1007\/978-3-642-22863-6_10","volume-title":"Interactive Theorem Proving","author":"G. Gonthier","year":"2011","unstructured":"Gonthier, G.: Point-Free, Set-Free Concrete Linear Algebra. In: van Eekelen, M., Geuvers, H., Schmaltz, J., Wiedijk, F. (eds.) ITP 2011. LNCS, vol.\u00a06898, pp. 103\u2013118. Springer, Heidelberg (2011)"},{"key":"15_CR19","doi-asserted-by":"publisher","DOI":"10.1007\/978-1-4612-6387-6","volume-title":"Finite-Dimensional Vector Spaces","author":"P. Halmos","year":"1974","unstructured":"Halmos, P.: Finite-Dimensional Vector Spaces. Springer, Heidelberg (1974)"},{"key":"15_CR20","unstructured":"Harrison, J.: The HOL light formalization of euclidean space. In: AMS Special Session on Formal Mathematics for Mathematicians (2011)"},{"key":"15_CR21","doi-asserted-by":"publisher","first-page":"576","DOI":"10.1145\/363235.363259","volume":"12","author":"C.A.R. Hoare","year":"1969","unstructured":"Hoare, C.A.R.: An axiomatic basis for computer programming. Comm. ACM\u00a012, 576\u2013580 (1969)","journal-title":"Comm. ACM"},{"key":"15_CR22","unstructured":"Izerrouken, N., Thirioux, X., Pantel, M., Strecker, M.: Certifying an Automated Code Generator Using Formal Tools: Preliminary Experiments in the GeneAuto Project. In: ERTS (2008)"},{"key":"15_CR23","unstructured":"Jonsson, U.T.: A lecture on the S-procedure (2001)"},{"key":"15_CR24","unstructured":"Moy, Y.: Union and cast in deductive verification"},{"key":"15_CR25","doi-asserted-by":"crossref","unstructured":"Mu\u00f1oz, C., Narkawicz, A.: Formalization of an efficient representation of Bernstein polynomials and applications to global optimization. J. of Automated Reasoning (2011)","DOI":"10.1007\/s10817-012-9256-3"},{"key":"15_CR26","series-title":"LNAI","first-page":"748","volume-title":"Automated Deduction - CADE-11","author":"S. Owre","year":"1992","unstructured":"Owre, S., Rushby, J.M., Shankar, N.: PVS: A Prototype Verification System. In: Kapur, D. (ed.) CADE 1992. LNCS (LNAI), vol.\u00a0607, pp. 748\u2013752. Springer, Heidelberg (1992)"},{"key":"15_CR27","unstructured":"Owre, S., Shankar, N.: Theory interpretations in PVS. Tech. Rep. SRI-CSL-01-01, Computer Science Laboratory. SRI International (April 2001)"},{"key":"15_CR28","unstructured":"Owre, S., Shankar, N., Rushby, J.M., Stringer-Calvert, D.W.J.: PVS Language Reference. Computer Science Laboratory. SRI International (September 1999)"}],"container-title":["Lecture Notes in Computer Science","NASA Formal Methods"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-642-28891-3_15.pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2022,1,9]],"date-time":"2022-01-09T03:11:00Z","timestamp":1641697860000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-642-28891-3_15"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2012]]},"ISBN":["9783642288906","9783642288913"],"references-count":28,"URL":"https:\/\/doi.org\/10.1007\/978-3-642-28891-3_15","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2012]]}}}