Registro:

Referencias:

• Alpern, B., Wegman, M.N., Zadeck, F.K.: Detecting equality of variables in programs. In Proceedings of the 15th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages; Belt, J., Robby. Deng, X.: Sireum/Topi LDP: a lightweight semi-decision procedure for optimizing symbolic execution-based analyses (2009) Proceedings of the 7th Joint Meeting of the European Software Engineering Conference and the ACM SIGSOFT Symposium on The foundations of software engineering, pp. 355–364. ACM
• Biere, A., Pre,icoSAT@SC’09. Solver description for sat competition 2009 (2009) In SAT 2009 Competitive Event Booklet
• Biere, A., Biere, A., Heule, M., van Maaren, H., Walsh, T., (2009) Handbook of Satisfiability: Volume 185 Frontiers in Artificial Intelligence and Applications, , IOS Press, Amsterdam:
• Blanc, N., Kroening, D., Sharygina, N., Scoot: A tool for the analysis of SystemC models (2008) Tools and Algorithms for the Construction and Analysis of Systems (TACAS 2008), LNCS, vol. 4963, pp. 467-470
• Boyapati, C., Khurshid, S., Marinov, D., Korat: automated testing based on java predicates (2002) Proceedings of the 2002 ACM SIGSOFT International Symposium on Software Testing and Analysis, pp. 123–133. ACM
• Chalin, P., Kiniry, J.R., Leavens, G.T., Poll, E., Beyond assertions: advanced specification and verification with jml and esc/java2 (2006) Proceedings of the 4th International Conference on Formal Methods for Components and Objects, pp. 342–363. Springer
• Clarke, E., Kroening, D., Lerda, F., A tool for checking ansi-c programs (2004) In Tools and Algorithms for the Construction and Analysis of Systems (TACAS 2004), LNCS, vol. 2988, pp. 168–176. Springer
• Clarke, E., Kroening, D., Sharygina, N., Yorav, K., SATABS: SAT-based predicate abstraction for ANSI-C (2005) Tools and Algorithms for the Construction and Analysis of Systems (TACAS 2005), Lecture Notes in Computer Science, vol. 3440, pp. 570–574. Springer
• Cousot, P., Cousot, R., Systematic design of program analysis frameworks (1979) Proceedings of the 6th ACM SIGACT-SIGPLAN Symposium on Principles of Programming Languages, pp. 269–282. ACM
• Cousot, P., Cousot, R., Abstract interpretation and application to logic programs (1992) J. Log. Program, 13 (2-3), pp. 103-179
• Crawford, J., Ginsberg, M., Luks, E., Roy, A., Symmetry-breaking predicates for search problems (1996) Principles of Knowledge Representation and Reasoning, pp. 148-159
• Dennis, G., Yessenov, K., Jackson, D., Bounded verification of voting software (2008) Proceedings of the 2nd International Conference on Verified Software: Theories, Tools, Experiments, pp. 130–145. Springer
• Dolby, J., Vaziri, M., Tip, F., Finding bugs efficiently with a sat solver (2007) Proceedings of the 6th Joint Meeting of the European Software Engineering Conference and the ACM SIGSOFT Symposium on The Foundations of Software Engineering, ESEC-FSE ’07, pp. 95-204. , New York, NY, USA: ACM
• Eén, N., Sörensson, N., An extensible sat-solver (2003) Giunchiglia, E., Tacchella, A., (eds.), SAT, Lecture Notes in Computer Science, vol. 2919, pp. 502–518. Springer
• Frias, M., Galeotti, J.P., López Pombo, C., Aguirre, N., Dynalloy: upgrading alloy with actions (2005) Proceedings of the 27th International Conference on Software Engineering, pp. 442–451. ACM
• Galeotti, J.P., (2010) Software Verification Using Alloy, , PhD thesis: University of Buenos Aires
• Galeotti, J.P., Rosner, N., López Pombo, C., Frias, M., Analysis of invariants for efficient bounded verification (2010) Proceedings of the 19th International Symposium on Software Testing and Analysis, pp. 25–36. ACM
• Harel, D., Kozen, D., Jerzy, T., (2000) Dynamic Logic, , The MIT Press, Cambridge:
• Ivancic, F., Yang, Z., Ganai, M.K., Gupta, A., Shlyakhter, I., Ashar, P., F-soft: Software verification platform (2005) In CAV’05, pp. 301-306
• Jackson, D., Alloy: a lightweight object modelling notation (2002) ACM Trans. Softw. Eng. Methodol, 11 (2), pp. 256-290
• Jackson, D., (2012) Software Abstractions: Logic, Language, and Analysis (Revised Edition), , The MIT Press, Cambridge:
• Jackson, D., Vaziri, M., Finding bugs with a constraint solver (2000) Proceedings of the 2000 ACM SIGSOFT International Symposium on Software Testing and Analysis, pp. 14–25. ACM
• Kildall, G.A., A unified approach to global program optimization (1973) Proceedings of the 1st Annual ACM SIGACT-SIGPLAN Symposium on Principles of Programming Languages, pp. 194–206. ACM
• Nielson, F., Nielson, H.R., Hankin, C., (1999) Principles of Program Analysis, , Springer, New York:
• Nielson, F., A denotational framework for data flow analysis (1982) Acta Inform, 18, pp. 265-287
• Post, H., Sinz, C., Küchlin, W., Towards automatic software model checking of thousands of linux modules—a case study with avinux (2009) Softw. Test. Verif. Reliab, 19 (2), pp. 155-172
• Shao, D., Gopinath, D., Khurshid, S., Perry, D.E., Optimizing incremental scope-bounded checking with data-flow analysis (2010) Proceedings of the 2010 IEEE 21st International Symposium on Software Reliability Engineering, pp. 408–417. IEEE Computer Society
• Sharma, R., Gligoric, M., Arcuri, A., Fraser, G., Marinov, D., Testing container classes: random or systematic? (2011) Proceedings of the 14th International Conference on Fundamental Approaches to Software Engineering: Part of the Joint European Conferences on Theory and Practice of Software, FASE’11/ETAPS’11, pp. 262–277. Springer
• Siddiqui, J.H., Khurshid, S., An empirical study of structural constraint solving techniques (2009) Proceedings of the 11th International Conference on Formal Engineering Methods: Formal Methods and Software Engineering, pp. 88–106. Springer
• Taghdiri, M., Seater, R., Jackson, D., Lightweight extraction of syntactic specifications (2006) Proceedings of the 14th ACM SIGSOFT International Symposium on Foundations of Software Engineering, pp. 276–286. ACM
• Torlak, E., Jackson, E., Kodkod: a relational model finder (2007) Proceedings of the 13th International Conference on Tools and Algorithms for the Construction and Analysis of Systems, pp. 632–647. Springer
• Visser, W., Pǎsǎreanu, C.S., Pelánek, R., Test input generation for java containers using state matching (2006) Proceedings of the 2006 International Symposium on Software Testing and Analysis, pp. 37–48. ACM
• Xie, Y., Aiken, A.: Saturn: a scalable framework for error detection using boolean satisfiability. ACM Trans. Program. Lang. Syst. 29, 16-es (2007); Yessenov, K., (2009) A light-weight specification language for bounded program verification, , Master’s thesis: MIT

Citas:

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

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

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

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