Registro:

Referencias:

• Andoni, A., Daniliuc, D., Khurshid, S., Marinov, D., (2013) Evaluating the 'Small Scope Hypothesis', , http://sdg.csail.mit.edu/publications.html
• Babic, D., Hu, A.J., Calysto: Scalable and precise extended static checking (2008) Proc. 30th Int'l Conf. Software Eng.
• Barnett, M., Chang, B.-Y.E., DeLine, R., Jacobs, B., Leino, K.R.M., Boogie: A modular reusable verifier for object-oriented programs (2006) Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics), 4111 LNCS, pp. 364-387. , Formal Methods for Components and Objects - 4th International Symposium, FMCO 2005, Revised Lectures
• Belt Robby, J., Deng, X., Sireum/topi ldp: A lightweight semi-decision procedure for optimizing symbolic execution-based analyses (2009) Proc. Seventh Joint Meeting of the European Software Eng. Conf. and the, pp. 355-364. , ACM SIGSOFT Symp. The Foundations of Software Eng
• Bouillaguet, C., Kuncak, V., Wies, T., Zee, K., Rinard, M., Using first-order theorem provers in the jahob data structure verification system (2007) Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics), 4349 LNCS, pp. 74-88. , Verification, Model Checking, and Abstract Interpretation, - 8th International Conference, VMCAI 2007, Proceedings
• Boyapati, C., Khurshid, S., Marinov, D., Korat: Automated testing based on java predicates (2002) Proc. ACM SIGSOFT Int'l Symp. Software Testing and Analysis, pp. 123-133
• Cohen, E., Dahlweid, M., Hillebrand, M., Leinenbach, D., Moskal, M., Santen, T., Schulte, W., Tobies, S., VCC: A practical system for verifying concurrent c (2009) Proc. 22nd Int'l Conf. Theorem Proving in Higher Order Logics
• Cousot, P., Cousot, R., Systematic design of program analysis frameworks (1979) Proc. Sixth ACM SIGACT-SIGPLAN Symp. Principles of Programming Languages, pp. 269-282
• Chalin, P., Kiniry, J.R., Leavens, G.T., Poll, E., Beyond assertions: Advanced specification and verification with jml and esc/java2 (2005) Proc. Fourth Int'l Conf. Formal Methods for Components and Objects, pp. 342-363
• Clarke, E., Kroening, D., Lerda, F., A tool for checking ansi-c programs (2004) Proc. Int'l Conf. Tools and Algorithms for the Construction and Analysis of Systems, pp. 168-176
• Cook, S., The complexity of theorem-proving procedures (1971) Proc. Third Ann. ACM Symp. Theory of Computing, pp. 151-158
• Demillo, R.A., Lipton, R.J., Sayward, F.G., Hints on test data selection: Help for the practicing programmer (1978) Computer, 11 (4), pp. 34-41. , Apr
• Deng Robby, X., Hatcliff, J., Towards a case-optimal symbolic execution algorithm for analyzing strong properties of object-oriented programs (2007) Proc. Fifth IEEE Int'l Conf. Software Eng. and Formal Methods, pp. 273-282
• Dennis, G., (2009) A Relational Framework for Bounded Program Verification, , PhD thesis, MIT Press, Sept
• Dennis, G., Chang, F., Jackson, D., Modular verification of code with sat (2006) Proc. Int'l Symp. Software Testing and Analysis, pp. 109-120
• Moura De L.Mendonca, Bjørner, N., Z3: An efficient smt solver (2008) Proc. 12th Int'l Conf. Tools and Algorithms for the Construction and Analysis of Systems, pp. 337-340
• Distefano, D., O'Hearn, P.W., Yang, H., A local shape analysis based on separation logic (2006) Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics), 3920 LNCS, pp. 287-302. , DOI 10.1007/11691372-19, Tools and Algorithms for the Construction and Analysis of Systems - 12th International Conference, TACAS 2006. Held as Part of the Joint European Conf. on Theory and Practice of Software, ETAPS 2006
• Distefano, D., Parkinson, M., Jstar: Towards practical verification for java (2008) Proc. 23rd ACM SIGPLAN Conf. Object-Oriented Programming Systems Languages and Applications, pp. 213-226
• Dennis, G., Yessenov, K., Jackson, D., Bounded verification of voting software (2008) Proc. Second Int'l Conf. Verified Software: Theories, Tools, Experiments, , Oct
• Dolby, J., Vaziri, M., Tip, F., Finding bugs efficiently with a sat solver (2007) Proc. Sixth Joint Meeting of the European Software Eng. Conf. and the ACM SIGSOFT Symp the Foundations of Software Eng., pp. 195-204
• Edwards, J., Jackson, D., Torlak, E., Yeung, V., Subtypes for constraint decomposition (2004) Proc. Int'l Symp. Software Testing and Analysis, , July
• Flanagan, C., Leino, K.R.M., Lillibridge, M., Nelson, G., Saxe, J.B., Stata, R., Extended static checking for Java (2002) Proceedings of the ACM SIGPLAN Conference on Programming Language Design and Implementation (PLDI), pp. 234-245
• Frias, M.F., Galeotti, J.P., Lopez Pombo, C.G., Aguirre, N., DynAlloy: Upgrading alloy with actions (2005) Proc. 27th Int'l Conf. Software Eng., pp. 442-450
• Frias, M.F., Lopez Pombo, C.G., Galeotti, J.P., Aguirre, N., Efficient analysis of dynalloy specifications (2007) ACM Trans. Software Eng. and Methodology, 17 (1)
• Galeotti, J.P., Frias, M.F., DynAlloy as a formal method for the analysis of java programs (2006) Proc. IFIP Working Conf. Software Eng. Techniques
• Galeotti, J.P., Rosner, N., Lopez Pombo, C.G., Frias, M.F., Analysis of invariants for efficient bounded verification Proc. 19th Int'l Symp. Software Testing and Analysis, 2010, pp. 25-36
• Iosif, R., Symmetry reduction criteria for software model checking (2002) Proc. Ninth Int'l SPIN Workshop Model Checking of Software, pp. 22-41
• Ivancic, F., Yang, Z., Ganai, M.K., Gupta, A., Shlyakhter, I., Ashar, P., F-SOFT: Software verification platform (2005) Lecture Notes in Computer Science, 3576, pp. 301-306. , Computer Aided Verification: 17th International Conference, CAV 2005. Proceedings
• Jackson, D., (2006) Software Abstractions, , MIT Press
• Jackson, D., Vaziri, M., Finding bugs with a constraint solver (2000) Proc. ACM SIGSOFT Int'l Symp. Software Testing and Analysis, pp. 14-25
• Khurshid, S., (2003) Generating Structurally Complex Tests from Declarative Constraints, , http://sdg.csail.mit.edu/pubs/theses/khurshid.phd.pdf, PhD thesis, MIT, Feb
• Khurshid, S., Marinov, D., Jackson, D., An analyzable annotation language (2002) Proc. 17th ACM SIGPLAN Conf. Object-Oriented Programming, Systems, Languages, and Applications, pp. 231-245
• Khurshid, S., Marinov, D., Shlyakhter, I., Jackson, D., A case for efficient solution enumeration (2003) Proc. Sixth Int'l Conf. Theory and Applications of Satisfiability Testing, pp. 272-286
• Khurshid, S., Marinov, D., TestEra: Specification-based testing of java programs using sat (2004) Automated Software Eng. J., 11 (4), pp. 403-434
• Leino, K.R.M., Specification and verification of object-oriented software (2008) Marktoberdorf Int'l Summer School
• Harel, D., Kozen, D., Tiuryn, J., (2000) Dynamic Logic, Foundations of Computing, , MIT Press
• Ma, Y.-S., Offutt, J., Kwon, Y.R., MuJava: An automated class mutation system (2005) Software Testing Verification and Reliability, 15 (2), pp. 97-133. , DOI 10.1002/stvr.308
• Musuvathi, M., Dill, D.L., An incremental heap canonicalization algorithm (2005) Lecture Notes in Computer Science, 3639, pp. 28-42. , Model Checking Software: 12th International SPIN Workshop. Proceedings
• Milicevic, A., Rayside, D., Yessenov, K., Jackson, D., Unifying execution of imperative and declarative code (2011) Proc. 33rd Int'l Conf. Software Eng, , May
• Rugina, R., Rinard, M., Symbolic bounds analysis of pointers, array indices, and accessed memory regions (2000) Proceedings of the ACM SIGPLAN Conference on Programming Language Design and Implementation (PLDI), pp. 182-195
• Siddiqui, J.H., Khurshid, S., An empirical study of structural constraint solving techniques (2009) Proc. 11th Int'l Conf. Formal Eng. Methods: Formal Methods and Software Eng., pp. 88-106
• Torlak, E., Jackson, D., Kodkod: A relational model finder (2007) Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics), 4424 LNCS, pp. 632-647. , Tools and Algorithms for the Construction and Analysis of Systems - 13th International Conference, TACAS 2007. Part of the Joint European Conferences on Theory and Practice of Software, ETAPS 2007
• Vaziri, M., Jackson, D., Checking properties of heap-manipulating procedures with a constraint solver (2003) Proc. Ninth Int'l Conf. Tools and Algorithms for the Construction and Analysis of Systems, pp. 505-520
• Visser, W., Havelund, K., Brat, G., Park, S., Lerda, F., Model checking programs (2003) Automated Software Eng., 10 (2), pp. 203-232
• Visser, W., Pasareanu, C.S., Pelanek, R., Test input generation for java containers using state matching (2006) Proc. Int'l Symp. Software Testing and Analysis, pp. 37-48
• Visser, W., , 2010. , private communication, second, Feb; Xie, Y., Aiken, A., Saturn: A scalable framework for error detection using boolean satisfiability (2007) ACM Trans. Programming Languages and Systems, 29 (3)

Citas:

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

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

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

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