Information Technology Reference
In-Depth Information
5. de Moura, L., Bjørner, N.: Z3: An efficient SMT solver. In: Ramakrishnan, C.R., Rehof, J.
(eds.) TACAS 2008. LNCS, vol. 4963, pp. 337-340. Springer, Heidelberg (2008)
6. Furia, C.A., Meyer, B., Velder, S.: Loop invariants: Analysis, classification, and examples
(2012),
http://arxiv.org/abs/1211.4470
7. Jackson, D.: Software Abstractions: Logic, Language, and Analysis. MIT Press (2006)
8. Jacobs, B., Piessens, F.: The VeriFast program verifier. Technical Report CW-520, Depart-
ment of Computer Science, Katholieke Universiteit Leuven (August 2008)
9. Kiselyov, O., Shan, C.-C., Friedman, D.P., Sabry, A.: Backtracking, interleaving, and termi-
nating monad transformers (functional pearl). In: ICFP, pp. 192-203. ACM (2005)
10. Klebanov, V., et al.: The 1st verified software competition: Experience report. In: Butler, M.,
Schulte, W. (eds.) FM 2011. LNCS, vol. 6664, pp. 154-168. Springer, Heidelberg (2011)
11. Klein, G., Elphinstone, K., Heiser, G., Andronick, J., Cock, D., Derrin, P., Elkaduwe, D.,
Engelhardt, K., Kolanski, R., Norrish, M., Sewell, T., Tuch, H., Winwood, S.: seL4: Formal
verification of an OS kernel. In: SOSP, pp. 207-220. ACM (2009)
12. Köksal, A., Kuncak, V., Suter, P.: Constraints as control. In: POPL, pp. 151-164 (2012)
13. Kuncak, V., Mayer, M., Piskac, R., Suter, P.: Complete functional synthesis. In: PLDI,
pp. 316-329. ACM (2010)
14. Le Goues, C., Leino, K.R.M., Moskal, M.: The boogie verification debugger (Tool paper).
In: Barthe, G., Pardo, A., Schneider, G. (eds.) SEFM 2011. LNCS, vol. 7041, pp. 407-414.
Springer, Heidelberg (2011)
15. Leavens, G.T., Cheon, Y., Clifton, C., Ruby, C., Cok, D.R.: How the design of JML ac-
commodates both runtime assertion checking and formal verification. Sci. Comput. Pro-
gram. 55(1-3), 185-208 (2005)
16. Leinenbach, D., Santen, T.: Verifying the microsoft hyper-V hypervisor with VCC. In:
Cavalcanti, A., Dams, D.R. (eds.) FM 2009. LNCS, vol. 5850, pp. 806-809. Springer,
Heidelberg (2009)
17. Leino, K.R.M.: This is Boogie 2 (2008),
http://goo.gl/QsH6g
18. Leino, K.R.M.: Dafny: An automatic program verifier for functional correctness. In: Clarke,
E.M., Voronkov, A. (eds.) LPAR-16 2010. LNCS, vol. 6355, pp. 348-370. Springer,
Heidelberg (2010)
19. Leino, K.R.M., Moskal, M.: Usable auto-active verification. In: Usable Verification Work-
shop (2010),
http://fm.csl.sri.com/UV10/
20. Milicevic, A., Rayside, D., Yessenov, K., Jackson, D.: Unifying execution of imperative and
declarative code. In: ICSE, pp. 511-520. ACM (2011)
21. Müller, P., Ruskiewicz, J.N.: Using debuggers to understand failed verification attempts. In:
Butler, M., Schulte, W. (eds.) FM 2011. LNCS, vol. 6664, pp. 73-87. Springer, Heidelberg
(2011)
22. Pattis, R.E.: Textbook errors in binary searching. In: SIGCSE, pp. 190-194. ACM (1988)
23. Polikarpova, N., Furia, C.A., Pei, Y., Wei, Y., Meyer, B.: What good are strong specifications?
In: ICSE, pp. 257-266. ACM (2013)
24. Suter, P., Köksal, A.S., Kuncak, V.: Satisfiability modulo recursive programs. In: Yahav, E.
(ed.) SAS 2011. LNCS, vol. 6887, pp. 298-315. Springer, Heidelberg (2011)
25. Tschannen, J., Furia, C.A., Nordio, M., Meyer, B.: Usable verification of object-oriented
programs by combining static and dynamic techniques. In: Barthe, G., Pardo, A., Schneider,
G. (eds.) SEFM 2011. LNCS, vol. 7041, pp. 382-398. Springer, Heidelberg (2011)
26. Tschannen, J., Furia, C.A., Nordio, M., Meyer, B.: Verifying Eiffel programs with Boogie.
In: BOOGIE Workshop (2011),
http://arxiv.org/abs/1106.4700
27. Tschannen, J., Furia, C.A., Nordio, M., Meyer, B.: Program checking with less hassle. In:
VSTTE (to appear, 2013)
28. Zee, K., Kuncak, V., Taylor, M., Rinard, M.C.: Runtime checking for program verifica-
tion. In: Sokolsky, O., Tasıran, S. (eds.) RV 2007. LNCS, vol. 4839, pp. 202-213. Springer,
Heidelberg (2007)
