{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,11,10]],"date-time":"2026-11-10T21:03:49Z","timestamp":1794344629344,"version":"4.9.0"},"publisher-location":"Boston, MA","reference-count":18,"publisher":"Springer US","isbn-type":[{"value":"9780387393872","type":"print"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"DOI":"10.1007\/978-0-387-39388-9_24","type":"book-chapter","created":{"date-parts":[[2007,1,16]],"date-time":"2007-01-16T12:55:34Z","timestamp":1168952134000},"page":"249-260","source":"Crossref","is-referenced-by-count":9,"title":["DynAlloy as a Formal Method for the Analysis of Java Programs"],"prefix":"10.1007","author":[{"given":"Juan P.","family":"Galeotti","sequence":"first","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Marcelo F.","family":"Frias","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"297","reference":[{"key":"24_CR1","unstructured":"Ball, T, A Theory of Predicate-Complete Test Coverage and Generation. Technical Report MSR-TR-2004-28, Microsoft Research, Redmond, WA, April 20004."},{"key":"24_CR2","doi-asserted-by":"crossref","unstructured":"Dijkstra E. W. and Scholten C. S., Predicate calculus and program semantics, Springer-Verlag, 1990.","DOI":"10.1007\/978-1-4612-3228-5"},{"key":"24_CR3","doi-asserted-by":"publisher","first-page":"442","DOI":"10.1109\/ICSE.2005.1553587","volume-title":"Proceedings of the 27th. International Conference on Software Engineering","author":"M. F. Frias","year":"2005","unstructured":"Frias, M. F., Galeotti, J. P., Lopez Pombo, C. G., and Aguirre, N. M. DynAlloy: Upgrading Alloy with actions. In Proceedings of the 27th. International Conference on Software Engineering, G-C. Roman, Ed. Association for the Computer Machinery and IEEE Computer Society, ACM Press, St. Louis, Missouri, USA, 2005, 442\u2013450."},{"issue":"4","key":"24_CR4","doi-asserted-by":"publisher","first-page":"478","DOI":"10.1145\/1101815.1101819","volume":"14","author":"M.F. Frias","year":"2005","unstructured":"Frias M.F., Lopez Pombo C.G., Baum G.A., Aguirre N.M. and Maibaum T.S.E., Reasoning About Static and Dynamic Properties in Alloy: A Purely Relational Approach, in ACM-Transactions on Software Engineering and Methodology (TOSEM), 14(4), 478\u2013526, 2005.","journal-title":"ACM-Transactions on Software Engineering and Methodology (TOSEM)"},{"key":"24_CR5","doi-asserted-by":"crossref","unstructured":"Godefroid P., Klarlund N. and Sen K., DART: Directed Automated Random Testing, in Proceedings of the ACM SIGPLAN 2005 Conference on Programming Languages Design and Implementation (PLDI), 2005.","DOI":"10.1145\/1065010.1065036"},{"key":"24_CR6","first-page":"142","volume-title":"Proceedings of the conference on Design, automation and test in Europe","author":"E. Goldberg","year":"2000","unstructured":"Goldberg, E. and Novikov, Y. BerkMin: A fast and robust sat-solver. In Proceedings of the conference on Design, automation and test in Europe, C. D. Kloos and J. da Franca, Eds. IEEE Computer Society, Paris, France, 142\u2013149, 2000."},{"key":"24_CR7","doi-asserted-by":"crossref","unstructured":"Gotlieb A., Denmat T. and Botella B., Constraint-Based Test Data Generation in the Presence of Stack-Directed Pointers, in Proceedings of ASE\u201905, Long Beach, CA, USA, ACM Press.","DOI":"10.1145\/1101908.1101958"},{"key":"24_CR8","doi-asserted-by":"crossref","unstructured":"Harel D., Kozen D. and Tiuryn J., Dynamic Logic, MIT Press, October 2000.","DOI":"10.7551\/mitpress\/2516.001.0001"},{"issue":"2","key":"24_CR9","doi-asserted-by":"publisher","first-page":"256","DOI":"10.1145\/505145.505149","volume":"11","author":"D. Jackson","year":"2002","unstructured":"Jackson, D. Alloy: a lightweight object modeling notation. ACM Transactions on Software Engineering and Methodology 11,2, 2002, 256\u2013290.","journal-title":"ACM Transactions on Software Engineering and Methodology"},{"key":"24_CR10","doi-asserted-by":"crossref","unstructured":"Jackson D., Schechter I. and Shlyakhter I., Alcoa: the Alloy Constraint Analyzer, Proceedings of the International Conference on Software Engineering, Limerick, Ireland, June 2000.","DOI":"10.1145\/337180.337616"},{"key":"24_CR11","doi-asserted-by":"crossref","unstructured":"Jackson D. and Vaziri, M., Finding Bugs with a Constraint Solver, in Proceedings of the International Symposium on Software Testing and Analysis (ISSTA), August 21\u201324, 2000, Portland, OR, USA. ACM, 2000, pp. 14\u201325.","DOI":"10.1145\/347324.383378"},{"key":"24_CR12","unstructured":"JUnit: http:\/\/www.junit.org."},{"issue":"4","key":"24_CR13","doi-asserted-by":"publisher","first-page":"403","DOI":"10.1023\/B:AUSE.0000038938.10589.b9","volume":"11","author":"S. Khurshid","year":"2004","unstructured":"Khurshid S. and Marinov D., TestEra: Specification-Based Testing of Java Programs Using SAT., Automated Software Engineering 11(4): 403\u2013434 (2004)","journal-title":"Automated Software Engineering"},{"key":"24_CR14","unstructured":"Gary T. Leavens, Albert L. Baker, and Clyde Ruby, Preliminary Design of JML: A Behavioral Interface Specification Language for Java. TR 98-06-rev27, Iowa State University, Department of Computer Science, April 2005."},{"key":"24_CR15","first-page":"530","volume-title":"Proceedings of the 38th conference on Design automation","author":"M. W. Moskewicz","year":"2001","unstructured":"Moskewicz, M. W., Madigan, C. F., Zhao, Y., Zhang, L., and Malik, S. Chaff: engineering an efficient SAT solver. In Proceedings of the 38th conference on Design automation, J. Rabaey, Ed. ACM Press, Las Vegas, Nevada, United States, 2001, 530\u2013535."},{"key":"24_CR16","doi-asserted-by":"crossref","unstructured":"Sen K., Marinov D. and Agha G., CUTE: A Concolic Unit Testing Engine for C, in Proceedings of the ACM SIGSOFT Conference on Foundations of Software Engineering, Lisbon, Portugal, 2005.","DOI":"10.1145\/1081706.1081750"},{"key":"24_CR17","doi-asserted-by":"crossref","unstructured":"Visser W., Pasareanu C., Khurshid S., Test Input Generation with Java PathFinder, in Proceedings of the ACM\/SIGSOFT International Symposium on Software Testing and Analysis, ISSTA 2004, Boston, Massachusetts, USA, July 11\u201314, 2004. ACM 2004, pp. 97\u2013107.","DOI":"10.1145\/1007512.1007526"},{"key":"24_CR18","doi-asserted-by":"crossref","unstructured":"Xie T., Marinov D., Schulte D. and Notkin D., Symtra: A Framework for Generating Object-Oriented Unit Tests Using Symbolic Execution, in Proceedings of TACAS 2005.","DOI":"10.1007\/978-3-540-31980-1_24"}],"container-title":["IFIP International Federation for Information Processing","Software Engineering Techniques: Design for Quality"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-0-387-39388-9_24.pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2021,4,27]],"date-time":"2021-04-27T22:05:24Z","timestamp":1619561124000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-0-387-39388-9_24"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[null]]},"ISBN":["9780387393872"],"references-count":18,"URL":"https:\/\/doi.org\/10.1007\/978-0-387-39388-9_24","relation":{"is-part-of":[{"id-type":"doi","id":"https:\/\/doi.org\/10.1007\/978-0-387-39388-9","asserted-by":"object"}]},"subject":[]}}