Registro:

Referencias:

• Dijkstra, E.W., Feijen, W.H.J., (1988) A Method of Programming, , Addison-Wesley Series in Computer Science. Addison-Wesley: Boston, MA, United States
• Atlee, J.M., Leblanc, R.J.J., Lethbridge, T.C., Sobel, A., Thompson, J.B., Software engineering 2004: ACM/IEEE-CS guidelines for undergraduate programs in software engineering (2005) Proceedings of the 27th International Conference on Software Engineering, pp. 623-624. , In. ACM: New York, NY, United States
• Cassel, L.N., Caspersen, M., Davies, G., McCauley, R., McGettrick, A., Pyster, A., Sloan, R., Curriculum update from the ACM education board: CS2008 and a report on masters degrees (2008) ACM SIGCSE Bulletin, 40, pp. 530-531. , In, ACM: New York, NY, United States
• D'Silva, V., Kroening, D., Weissenbacher, G., A survey of automated techniques for formal software verification (2008) Computer-Aided Design of Integrated Circuits and Systems, 27 (7), pp. 1165-1178
• Flanagan, C., Leino, K.R.M., Lillibridge, M., Nelson, G., Saxe, J.B., Stata, R., Extended static checking for Java (2002) Proceedings of the Conference on Programming Language Design and Implementation (PLDI '02), pp. 234-245. , Berlin, Germany
• Barnett, M., Leino, K.R.M., Schulte, W., The Spec# programming system: An overview (2005) Construction and Analysis of Safe, Secure and Interoperable Smart Devices, pp. 49-69. , In. Springer: New York, NY, United States
• Leino, K.R.M., Dafny: An automatic program verifier for functional correctness (2010) Proceedings of the 16th International Conference on Logic for Programming, Artificial Intelligence, and Reasoning, pp. 348-370. , In. Springer: New York, NY, United States
• Leino, K.R.M., Monahan, R., Automatic verification of textbook programs that use comprehensions (2007) Formal Techniques for Java-like Programs (FTFJP '07), , Berlin, Germany
• De Caso, G., Garbervetsky, D., Gorín, D., PEST: From the lab to the classroom (2011) Proceedings of the 1st Workshop on Developing Tools As Plug-ins, pp. 5-8. , In. ACM: New York, NY, United States
• De Millo, R.A., Lipton, R.J., Perlis, A.J., Social processes and proofs of theorems and programs (1979) Communications of the ACM, 22 (5), pp. 271-280
• Good, D.I., London, R.L., Bledsoe, W.W., An interactive program verification system (1975) ACM SIGPLAN Notices, 10, pp. 482-492. , In, ACM: New York, NY, United States
• Leavens, G.T., Baker, A.L., Ruby, C., JML: A notation for detailed design (1999) Behavioral Specifications of Businesses and Systems, pp. 175-188. , In. Kluwer Academic Publishers: Berlin, Heidelberg, Germany
• Chatterjee, S., Lahiri, S.K., Qadeer, S., Rakamaric, Z., A reachability predicate for analyzing low-level software (2007) International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS'07), pp. 19-33. , Braga, Portugal
• Xu, D.N., Extended static checking for Haskell (2006) ACM Sigplan Workshop on Haskell, pp. 48-59. , Portland, Oregon, United States
• De Caso, G., Garbervetsky, D., Gorín, D., (2012) PEST Formal Specification (v1.1), , Technical Report, Universidad de Buenos Aires
• De Caso, G., Gorín, D., Garbervetsky, D., Reducing the number of annotations in a verification-oriented imperative language (2009) The Symposium on Automatic Program Verification (APV'09), , Río Cuarto, Argentina
• Dijkstra, E.W., (1997) A Discipline of Programming, , Prentice Hall PTR: Upper Saddle River, NJ, USA
• Damas, L., Milner, R., Principal type-schemes for functional programs (1982) Proceedings of the 9th ACM Sigplan-Sigact Symposium on Principles of Programming Languages, pp. 207-212. , In. ACM: New York, NY, United States
• Eclipse Integrated Development Framework, , http://www.eclipse.org, [last accessed 16 September 2011]
• De Moura, L., Bjãrner, N., Z3: An efficient SMT solver (2008) Tools and Algorithms for the Construction and Analysis of Systems, pp. 337-340. , In. Springer-Verlag: Berlin, Germany
• Barrett, C., Berezin, S., CVC lite: A new implementation of the Cooperating Validity Checker (2004) Proceedings of the 16th International Conference on Computer Aided Verification (CAV '04), pp. 515-518. , Boston, MA, United States
• Dutertre, B., De Moura, L., The Yices SMT Solver, , http://yices.csl.sri.com/, [last accessed August 2006]
• Ranise, S., Tinelli, C., (2006) The SMT-LIB Standard: Version 1.2, , Department of Computer Science, The University of Iowa, Tech. Rep
• Barnett, M., Deline, R., Fähndrich, M., Leino, K.R.M., Schulte, W., Verification of object-oriented programs with invariants (2004) Journal of Object Technology, 3 (6), pp. 27-56
• Monahan, R., (2011) Teaching Using SPEC# in Europe: An Experience Report from University Teaching and Various Verification Tutorials, , July. Microsoft Research Faculty Summit 2011, Oral communication
• Leino, K.R.M., Monahan, R., Reasoning about comprehensions with first-order SMT solvers (2009) Annual ACM Symposium on Applied Computing (SAC '09), pp. 615-622. , Honolulu, HI, United States
• Kassios, I., (2006) Dynamic Frames: In Support for Framing, Dependencies and Sharing Without Restrictions, pp. 268-283. , FM 2006: Formal Methods, Springer: New York, NY, United States
• Garbervetsky, D., Gorín, D., Neisen, A., Enforcing structural invariants using dynamic frames (2011) Tools and Algorithms for the Construction and Analysis of Systems, pp. 65-80. , Springer, New York, NY, United States
• Le Goues, C., Leino, K., Moskal, M., The boogie verification debugger (tool paper) (2011) Software Engineering and Formal Methods, pp. 407-414. , Springer, New York, NY, United States
• Poll, E., Teaching program specification and verification using JML and ESC/Java2 (2009) Conference on Teaching Formal Methods (TFM'09), pp. 92-104. , Eindhoven, Netherlands
• Cok, D.R., Kiniry, J.R., ESC/Java2: Uniting ESC/Java and JML (2005) Construction and Analysis of Safe, Secure, and Interoperable Smart Devices, pp. 108-128. , Springer, New York, NY, United States
• Back, R.J., Invariant based programming: Basic approach and teaching experiences (2009) Formal Aspects of Computing, 21, pp. 227-244. , DOI: 10.1007/s00165-008-0070-y
• Owre, S., Rushby, J., Shankar, N., PVS: A prototype verification system (1992) 11th International Conference on Automated Deduction, 607, pp. 748-752. , In, Lecture Notes in Artificial Intelligence. Springer: New York, NY, United States
• Back, R.J., Eriksson, J., Myreen, M., Testing and verifying invariant based programs in the SOCOS environment (2007) Tests and Proofs, pp. 61-78
• Detlefs, D., Nelson, G., Saxe, J.B., Simplify: A theorem prover for program checking (2005) Journal of the ACM, 52 (3), pp. 365-473
• Noble, J., Vitek, J., Potter, J., Flexible alias protection (1998) European Conference on Object-Oriented Programming (ECOOP '98), pp. 158-185

Citas:

---------- APA ----------

---------- CHICAGO ----------

---------- MLA ----------

---------- VANCOUVER ----------