| [1] |
Amin, N.; Leino, KRM; Rompf, T.; Seidl, M. (ed.); Tillmann, N. (ed.), Computing with an SMT solver, 20-35 (2014), Berlin |
| [2] |
Almási G, Padua D (2002) MaJIC: compiling MATLAB for speed and responsiveness. SIGPLAN Not 37(5): 294-303 · doi:10.1145/543552.512564 |
| [3] |
Burdy L, Cheon Y, Cok D, Ernst M, Kiniry J, Leavens GT, Leino KRM, Poll E (2005) An overview of JML tools and applications. Int J Softw Tools Technol Transfer 7(3): 212-232 · doi:10.1007/s10009-004-0167-4 |
| [4] |
Barnett M, Chang BYE, Deline R, Jacobs B, Leino KRM (2006) Boogie: a modular reusable verifier for object-oriented programs. In: de Boer, FS, Bonsangue MM, Graf S, de Roever W-P (eds) FMCO’05, vol 4111. LNCS. Springer, Berlin, pp 364-387 |
| [5] |
Barnett M, Fähndrich M, Leino KRM, Müller P, Schulte W, Venter H (2011) Specification and verification: the Spec# experience. Commun ACM 54(6): 81-91 · doi:10.1145/1953122.1953145 |
| [6] |
Boström, P.; Qin, S. (ed.); Qiu, Z. (ed.), Contract-based verification of Simulink models, 291-306 (2011), Berlin |
| [7] |
Boström P, Wiik J (2015) Contract-based verification of discrete-time multi-rate Simulink models. Softw Syst Model. doi:10.1007/s10270-015-0477-x · Zbl 1338.65116 |
| [8] |
Jay CCB, Steckler P (1998) The functional imperative: Shape! In: Hankin C (ed) ESOP’98, vol 1381. LNCS. Springer, Berlin, pp 139-153 |
| [9] |
Cuoq, P.; Kirchner, F.; Kosmatov, N.; Prevosto, V.; Signoles, J.; Yakobowski, B.; Eleftherakis, G. (ed.); Hinchey, M. (ed.); Holcombe, M. (ed.), Frama-C: a software analysis perspective, 233-247 (2012), Berlin |
| [10] |
Chalin P, Kiniry JR, Leavens GT, Poll E (2006) Beyond assertions: advanced specification and verification with JML and ESC/Java2. In: de Boer, FS, Bonsangue MM, Graf S, de Roever W-P (eds) FMCO’06, vol 4111. LNCS. Springer, Berlin, pp 342-363 |
| [11] |
Cook B, Podelski A, Rybalchenko A (2011) Proving program termination. Commun ACM 54(5): 88-98 · doi:10.1145/1941487.1941509 |
| [12] |
de Moura L, Bjørner N (2008) Z3: an efficient SMT solver. In: Ramakrishnan CR, Rehof J (eds) TACAS’08, vol 4963. LNCS. Springer, Berlin, pp 337-340 |
| [13] |
Donaldson, AF; Haller, L.; Kroening, D.; Rümmer, P.; Yahav, E. (ed.), Software verification using k-induction, 351-368 (2011), Berlin |
| [14] |
de Moura L, Bjørner N (2009) Generalized, efficient array decision procedures. In: FMCAD’09. IEEE, New York, pp 45-52 · Zbl 0388.68003 |
| [15] |
de Rose L, Padua D (1999) Techniques for the translation of MATLAB programs into Fortran 90. ACM TOPLAS 21(2): 286-323 · doi:10.1145/316686.316693 |
| [16] |
Fähndrich, M.; Logozzo, F.; Beckert, B. (ed.); Marché, C. (ed.), Static contract checking with abstract interpretation, 10-30 (2011), Berlin · Zbl 1308.68033 |
| [17] |
Fuh Y-C, Mishra P (1990) Type inference with subtypes. Theor Comput Sci 73(2): 155-175 · Zbl 0701.68012 · doi:10.1016/0304-3975(90)90144-7 |
| [18] |
Filliatre, JC; Paskevich, A.; Gardner, P. (ed.); Felleisen, M. (ed.), Why3—where programs meet provers, 125-128 (2013), Berlin · Zbl 1435.68366 |
| [19] |
Ge Y, de Moura L (2009) Complete instantiation for quantified formulas in satisfiability modulo theories. In: Bouajjani A, Maler O (eds) CAV’09, vol 5643. LNCS. Springer, Berlin, pp 306-320 · Zbl 1242.68280 |
| [20] |
Garoche, PL; Kahsai, T.; Tinelli, C.; Brat, G. (ed.); Rungta, N. (ed.); Venet, A. (ed.), Incremental invariant generation using logic-based automatic abstract transformers, 139-154 (2013), Berlin |
| [21] |
Henzinger, TA; Hottelier, T.; Kovács, L.; Voronkov, A.; Barthe, G. (ed.); Hermenegildo, M. (ed.), Invariant and type inference for matrices, 163-179 (2010), Berlin · Zbl 1273.68083 |
| [22] |
Joisha PG, Banerjee P (2006) An algebraic array shape inference system for MATLAB. ACM TOPLAS 28(5): 848-907 · doi:10.1145/1152649.1152651 |
| [23] |
Juhasz U, Kassios IT, Muller P, Novacek M, Schwerhoff M, Summers AJ (2014) Viper: a verification infrastructure for permission-based reasoning. Technical report, ETH Zurich |
| [24] |
Leino, KRM; Clarke, EM (ed.); Voronkov, A. (ed.), Dafny: an automatic program verifier for functional correctness, 348-370 (2010), Berlin · Zbl 1253.68095 |
| [25] |
Leino KRM, Monahan R (2009) Reasoning about comprehensions with first-order SMT-solvers. In: SAC’09. ACM, New York, pp 615-622 |
| [26] |
Mathworks Inc. (2014) Simulink. http://www.mathworks.com |
| [27] |
Milner R (1978) A theory of type polymorphism in programming. J Comput Syst Sci 17(3): 348-375 · Zbl 0388.68003 · doi:10.1016/0022-0000(78)90014-4 |
| [28] |
Reynolds, A.; Kuncak, V.; D’Souza, D. (ed.); Lal, A. (ed.); Larsen, KG (ed.), Induction for SMT solvers, 80-98 (2015), Berlin · Zbl 1432.68418 |
| [29] |
Robinson JA (1965) A machine-oriented logic based on the resolution principle. J ACM 12(1): 23-41 · Zbl 0139.12303 · doi:10.1145/321250.321253 |
| [30] |
Suter, P.; Köksal, AS; Kuncak, V.; Yahav, E. (ed.), Satisfiability modulo recursive programs, 298-315 (2011), Berlin |
| [31] |
Traytel, D.; Berghofer, S.; Nipkow, T.; Yang, H. (ed.), Extending Hindley-Milner type inference with coercive structural subtyping, 89-104 (2011), Berlin |
| [32] |
Wiik, J.; Boström, P.; Merz, S. (ed.); Pang, J. (ed.), Contract-based verification of MATLAB and Simulink matrix-manipulating code, 396-412 (2014), Berlin |
| [33] |
Wiik J, Boström P (2014) Contract-based verification of MATLAB and Simulink matrix-manipulating code. Technical report 1107, TUCS · Zbl 1338.65116 · doi:10.1007/978-3-319-11737-9_26 |
| [34] |
Xi H (1999) Dependent types in practical programming. In: POPL’99. ACM, New York, pp 214-227 |
| [35] |
Xi H (2007) Dependent ML: an approach to practical programming with dependent types. J Funct Program 17(2): 215-286 · Zbl 1125.68033 · doi:10.1017/S0956796806006216 |
