Information Technology Reference
In-Depth Information
5. Signoles, J.: E-ACSL: Executable ANSI/ISO C Specification Language (May 2013),
6. Delahaye, M., Kosmatov, N., Signoles, J.: Common specification language for static
and dynamic analysis of C programs. In: The 28th Annual ACM Symposium on
Applied Computing (SAC 2013), pp. 1230-1235. ACM (2013)
7. Signoles, J.: E-ACSL User Manual (May 2013),
8. Meyer, B.: Object-Oriented Software Construction. Prentice-Hall, Inc. (1988)
9. Leavens, G.T., Cheon, Y., Clifton, C., Ruby, C., Cok, D.R.: How the design of
JML accommodates both runtime assertion checking and formal verification. Sci.
Comput. Program. 55(1-3), 185-208 (2005)
10. Barnett, M., Leino, K.R.M., Schulte, W.: The Spec# programming system: An
overview. In: Barthe, G., Burdy, L., Huisman, M., Lanet, J.-L., Muntean, T. (eds.)
CASSIS 2004. LNCS, vol. 3362, pp. 49-69. Springer, Heidelberg (2005)
11. AdaCore and Altran UK Ltd: SPARK 2014 Reference Manual (2013),
12. Kosmatov, N., Prevosto, V., Signoles, J.: A lesson on proof of programs with Frama-
C. Invited tutorial paper. In: Veanes, M., Vigano, L. (eds.) TAP 2013. LNCS,
vol. 7942, pp. 168-177. Springer, Heidelberg (2013)
13. Kosmatov, N., Petiot, G., Signoles, J.: Optimized memory monitoring for runtime
assertion checking of C programs. In: The 4th International Conference on Runtime
Verification (RV 2013). LNCS. Springer (2013) (to appear)
14. Botella, B., Delahaye, M., Hong-Tuan-Ha, S., Kosmatov, N., Mouy, P., Roger,
M., Williams, N.: Automating structural testing of C programs: Experience with
PathCrawler.In:The4th Int.Workshop on Automation ofSoftwareTest(AST2009),
pp. 70-78. IEEE Computer Society (2009)
15. Cousot, P.R.: Abstract interpretation: a unified lattice model for static analysis of
programs by construction or approximation of fixpoints. In: POPL, pp. 238-252
(1977)
16. Dijkstra, E.W.: A constructive approach to program correctness. BIT Numerical
Mathematics (1968)
17. Conchon, S., et al.: The Alt-Ergo Automated Theorem Prover,
