Registro:

Referencias:

• Abad, P., Aguirre, N., Bengolea, V., Ciolek, D., Frias, M.F., Galeotti, J., Maibaum, T., Vissani, I., Tight bounds + Incremental SAT = Better test generation under rich contracts (2013) Proceedings of Sixth IEEE International Conference on Software Testing, Verification and Validation (ICST)
• Abrial, J.R., (1996) The B-Book: Assigning Programs to Meanings, , Cambridge, UK, Cambridge University Press
• http://alloy.mit.edu/alloy/download.html; Biere, A., Lingeling plingeling PicoSAT and PrecoSAT at SAT race (2010) Solver Description, Special Track 1 (Parallel CNF), SAT-Race 2010, , http://baldur.iti.uka.de/sat-race-2010/descriptions/solver_1+2+3+6.pdf
• Boyapati, C., Khurshid, S., Marinov, D., Korat: Automated testing based on Java predicates (2002) ISSTA, pp. 123-133
• Cadar, C., Dunbar, D., Engler, D.R., KLEE: Unassisted and automatic generation of high-coverage tests for complex systems programs (2008) Proc. 8th Symposium on Operating Systems Design and Implementation (OSDI), pp. 209-224
• Chrabakh, W., Wolski, R., GrADSAT: A parallel SAT solver for the grid UCSB Computer Science Technical Report Number 2003-05
• Dennis, G., Chang, F., Jackson, D., Modular verification of code with SAT (2006) ISSTA'06, pp. 109-120
• Dijkstra, E.W., A belated proof of self-stabilization (1986) Distributed Computing, 1 (1), pp. 5-6
• Dolby, J., Vaziri, M., Tip, F., Finding bugs efficiently with a SAT solver (2007) ESEC/FSE'07, pp. 195-204. , ACM Press
• Een, N., Sörensson, N., An extensible SAT-solver (2003) SAT
• Funes, D., Siddiqui, J.H., Khurshid, S., Ranged model checking (2012) Proc. Java PathFinder Workshop (JPF)
• Galeotti, J.P., Rosner, N., López Pombo, C., Frias, M.F., Analysis of invariants for efficient bounded verification (2010) Proceedings of ISSTA 2010, pp. 25-36
• Galeotti, J.P., Rosner, N., López Pombo, C., Frias, M.F., TACO: Efficient SAT-based bounded verification using symmetry breaking and tight bounds IEEE Transactions on Software Engineering, , to appear
• Gil, L., Flores, P., Silveira, L.M., PMSat: A parallel version of MiniSAT (2008) Journal on Satisfiability, Boolean Modeling and Computation, 6, pp. 71-98
• Hamadi, Y., Jabbour, S., Sais, L., ManySAT: A parallel SAT solver (2009) International Journal on Satisfiability, Boolean Modeling and Computation (JSAT), 6. , Special Issue on Parallel SAT, IOS Press
• IEEE Standard for A High-Performance Serial Bus, , http://ieeexplore.ieee.org/servlet/opac?punumber=4659231
• Jackson, D., (2006) Software Abstractions, , MIT Press
• Kang, E., Jackson, D., Formal modeling and analysis of a flash filesystem in alloy LNCS, 5238, pp. 294-308. , Proceedings of ABZ 2008, Springer
• Kim, J.S., Garlan, D., Analyzing architectural styles Journal of Systems and Software, 83 (7), pp. 1216-1235. , Elsevier
• Leavens, G.T., Baker, A.L., Ruby, C., JML: A notation for detailed design (1999) Behavioral Specifications of Businesses and Systems, pp. 175-188. , Chapter 12, Amsterdam, Kluwer
• Leino, K.R.M., Mülcer, P., Using the spec# language, methodology, and tools to write bug-free programs (2009) Manuscript KRML 189, , http://specsharp.codeplex.com/wikipage?title=Tutorial, 17 September
• Marinov, D., Khurshid, S., TestEra: A novel framework for automated testing of java programs (2001) Proc. 16th IEEE Conference on Automated Software Engineering (ASE)
• Misailovic, S., Milicevic, A., Petrovic, N., Khurshid, S., Marinov, D., Parallel test generation and execution with Korat (2007) Proc. 6th Joint Meeting of the European Software Engineering Conference and the ACM SIGSOFT Symposium on the Foundations of Software Engineering (ESEC/FSE)
• Maoz, S., Ringert, J.O., Rumpe, B., CD2Alloy: Class diagrams analysis using alloy revisited LNCS, 6981, pp. 592-607. , Proceedings of MODELS 2011, Springer
• (2012) OCL Specification v 2.3.1, , http://www.omg.org/spec/OCL/2.3.1/PDF/, January 1st
• Ohmura, K., Ueda, K., C-sat: A parallel SAT solver for clusters (2009) LNCS, 5585. , SAT 2009
• Rosner, N., Galeotti, J.P., Bermúdez, S., Marucci Blas, G., Perez De Rosso, S., Pizzagalli, L., Zemín, L., Frias, M.F., Parallel bounded analysis in code with rich invariants by refinement of field bounds (2013) Proceedings of ISSTA 2013, pp. 23-33. , to appear
• Rosner, N., López Pombo, C.G., Aguirre, N., Jaoua, A., Mili, A., Frias, M.F., Parallel bounded verification of alloy models by TranScoping Proceedings of VSTTE 2013, , to appear
• Shlyakhter, I., Generating effective symmetry-breaking predicates for search problems (2001) Electronic Notes in Discrete Mathematics, 9. , Proceedings of LICS 2001 Workshop on Theory and Applications of Satisfiability Testing, June 2001, Boston, MA. Henry Kautz and Bart Selman (eds.)
• Siddiqui, J.H., Khurshid, S., PKorat: Parallel generation of structurally complex test inputs (2009) 2nd International Conference on Software Testing, Verification, and Validation (ICST 2009), , Denver, CO. Apr
• Siddiqui, J.H., Khurshid, S., Scaling symbolic execution using ranged analysis (2012) Proc. 27th ACM SIGPLAN Conference on Object-Oriented Programming, Systems, Languages and Applications (OOPSLA)
• Shao, D., Gopinath, D., Khurshid, S., Perry, D.E., Optimizing incremental scope-bounded checking with data-flow analysis (2010) ISSRE, pp. 408-417
• Shao, D., Khurshid, S., Perry, D.E., An incremental approach to scope- bounded checking using a lightweight formal method (2009) FM, pp. 757-772
• Spivey, J.M., (1992) The Z Notation: A Reference Manual, , 2nd ed. Upper Saddle River, NJ, Prentice Hall
• Stoica, I., Morris, R., Liben-Nowell, D., Karge, D., Kaashoek, M.F., Balakrishnan, H., Chord: A scalable peer-to-peer lookup service for internet applications (2003) IEEE Transactions on Networking, 11
• Torlak, E., Jackson, D., Kodkod: A relational model finder LNCS, 4425, pp. 632-647. , TACAS '07
• Visser, W., Havelund, K., Brat, G., Park, S., Model checking programs (2000) Proc. 15th Conference on Automated Software Engineering (ASE), , Grenoble, France
• Visser, W., Pǎsǎreanu, C.S., Pelánek, R., Test input generation for java containers using state matching (2006) ISSTA 2006, pp. 37-48
• Zave, P., Compositional binding in network domains LNCS, 4085, pp. 332-347. , Proceedings of FM 2006. SpringerA4 - IEEE Computer Society; Association for Computing Machinery, Special Interest Group on Software Engineering (ACM SIGSOFT); IEEE Technical Council on Software Engineering (TCSE); ACM SIGART; NASA

Citas:

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

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

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

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