Elvira Albert
Miguel Gómez-Zamalloa
ABSTRACT
Testing is a vital part of the software development process. In static testing, instead of executing the program on normal values (e.g., numbers), typically the program is executed on symbolic variables representing arbitrary values. Constraints on the symbolic variables are used to represent the conditions under which the execution paths are taken. Testing tools can uncover issues such as memory leaks, buffer overflows, and also concurrency errors like deadlocks or data races. Due to its inherent symbolic execution mechanism and the availability of constraint solvers, Constraint Logic Programming (CLP) has a big potential in the field of testing. In this talk, we will describe a fully CLP-based framework to testing of a today's imperative language. We will also discuss the extension of this framework to handle actor-based concurrency, used in languages such as Go, Actor-Foundry, Erlang, and Scala, among others.
- Parosh Aziz Abdulla, Stavros Aronis, Bengt Jonsson, and Konstantinos F. Sagonas. Optimal Dynamic Partial Order Reduction. In Proc. of POPL'14, pages 373--384. ACM, 2014. Google Scholar
Digital Library
- G. Agha. Actors: A Model of Concurrent Computation in Distributed Systems. MIT Press, Cambridge, MA, 1986. Google ScholarDigital Library
- E. Albert, P. Arenas, S. Genaim, G. Puebla, and D. Zanardini. Cost Analysis of Java Bytecode. In Procs. of ESOP'07, volume 4421 of LNCS, pages 157--172. Springer, 2007. Google ScholarDigital Library
- Elvira Albert, Puri Arenas, and Miguel Gómez-Zamalloa. Symbolic Execution of Concurrent Objects in CLP. In Proc. of PADL'12, volume 7149 of LNCS, pages 123--137. Springer, 2012. Google ScholarDigital Library
- Elvira Albert, Puri Arenas, and Miguel Gómez-Zamalloa. Actor- and Task-Selection Strategies for Pruning Redundant State-Exploration in Testing. In Proc. of FORTE'14, volume 8461 of LNCS, pages 49--65. Springer, 2014.Google Scholar
- Elvira Albert, Puri Arenas, and Miguel Gómez-Zamalloa. Test Case Generation of Actor Systems. In Proc. of ATVA'15, volume 9364 of LNCS, pages 259--275. Springer, 2015.Google Scholar
- Elvira Albert, Puri Arenas, Miguel Gómez-Zamalloa, and Peter Y.H. Wong. aPET: A Test Case Generation Tool for Concurrent Objects. In Proc. of ESEC/FSE'13, pages 595--598. ACM, 2013. Google ScholarDigital Library
- Elvira Albert, Israel Cabañas, Antonio Flores-Montoya, Miguel Gómez-Zamalloa, and Sergio Gutiérrez. jPET: an Automatic Test-Case Generator for Java. In Proc. of WCRE'11, pages 441--442. IEEE Computer Society, 2011. Google ScholarDigital Library
- Elvira Albert, María García de la Banda, Miguel Gómez-Zamalloa, José Miguel Rojas, and Peter Stuckey. A CLP Heap Solver for Test Case Generation. Theory and Practice of Logic Programming, 13(4-5):721--735, July 2013.Google ScholarCross Ref
- Elvira Albert, Miguel Gómez-Zamalloa, Laurent Hubert, and Germán Puebla. Verification of Java Bytecode using Analysis and Transformation of Logic Programs. In Proc. of PADL'07, volume 4354 of LNCS, pages 124--139. Springer, 2007. Google ScholarDigital Library
- Elvira Albert, Miguel Gómez-Zamalloa, and Miguel Isabel. Combining Static Analysis and Testing for Deadlock Detection. In Proc. of IFM'16, volume 9681 of LNCS, pages 409--424. Springer, 2016. Google ScholarDigital Library
- Elvira Albert, Miguel Gómez-Zamalloa, and Miguel Isabel. SYCO: A Systematic Testing Tool for Concurrent Objects. In Proc. of CC'16, pages 269--270. ACM, 2016. Google ScholarDigital Library
- Elvira Albert, Miguel Gómez-Zamalloa, and Germán Puebla. Test Data Generation of Bytecode by CLP Partial Evaluation. In Proc. of LOPSTR'08, volume 5438 of LNCS, pages 4--23. Springer, 2009. Google ScholarDigital Library
- Elvira Albert, Miguel Gómez-Zamalloa, and Germán Puebla. PET: A Partial Evaluation-based Test Case Generation Tool for Java Bytecode. In Proc. of PEPM'10, pages 25--28. ACM Press, 2010. Google ScholarDigital Library
- Maria Christakis, Alkis Gotovos, and Konstantinos F. Sagonas. Systematic Testing for Detecting Concurrency Errors in Erlang Programs. In Proc. of ICST'13, pages 154--163. IEEE Computer Society, 2013. Google ScholarDigital Library
- Lori A. Clarke. A System to Generate Test Data and Symbolically Execute Programs. IEEE Transactions on Software Engineering, 2(3):215--222, 1976. Google ScholarDigital Library
- F. Degrave, T. Schrijvers, and W. Vanhoof. Towards a Framework for Constraint-Based Test Case Generation. In Proc. of LOPSTR'09, volume 6037 of LNCS, pages 128--142. Springer, 2010. Google ScholarDigital Library
- C. Engel and R. Hähnle. Generating Unit Tests from Formal Proofs. In Proc. of TAP'07, volume 4454 of LNCS, pages 169--188. Springer, 2007. Google ScholarDigital Library
- J. Esparza. Model checking using net unfoldings. Sci. Comput. Program., 23(2-3):151--195, 1994. Google ScholarDigital Library
- Roger Ferguson and Bogdan Korel. The Chaining Approach for Software Test Data Generation. ACM Trans. Softw. Eng. Methodol., 5(1):63--86, 1996. Google ScholarDigital Library
- C. Flanagan and P. Godefroid. Dynamic Partial-Order Reduction for Model Checking Software. In Proc. of POPL'05, pages 110--121. ACM, 2005. Google ScholarDigital Library
- P. Godefroid. Using Partial Orders to Improve Automatic Verification Methods. In Proc. of CAV'91, volume 531 of LNCS, pages 176--185. Springer, 1991. Google ScholarDigital Library
- Patrice Godefroid. Partial-Order Methods for the Verification of Concurrent Systems - An Approach to the State-Explosion Problem, volume 1032 of LNCS. Springer, 1996. Google ScholarDigital Library
- M. Gómez-Zamalloa, E. Albert, and G. Puebla. Decompilation of Java Bytecode to Prolog by Partial Evaluation. JIST, 51:1409--1427, October 2009. Google ScholarDigital Library
- Miguel Gómez-Zamalloa, Elvira Albert, and Germán Puebla. Decompilation of Java Bytecode to Prolog by Partial Evaluation. Information and Software Technology, 51(10):1409--1427, October 2009. Google ScholarDigital Library
- Miguel Gómez-Zamalloa, Elvira Albert, and Germán Puebla. Test Case Generation for Object-Oriented Imperative Languages in CLP. Theory and Practice of Logic Programming, ICLP'10 Special Issue, 10(4-6):659--674, 2010. Google ScholarDigital Library
- A. Gotlieb, B. Botella, and M. Rueher. A CLP Framework for Computing Structural Test Data. In Proc. CL'00, volume 1861 of LNAI, pages 399--413. Springer, 2000. Google ScholarDigital Library
- Neelam Gupta, Aditya P. Mathur, and Mary Lou Soffa. Generating Test Data for Branch Coverage. In Proc. of ASE'00, pages 219--228. IEEE Computer Society, 2000. Google ScholarDigital Library
- P. Haller and M. Odersky. Scala Actors: Unifying Thread-based and Event-based Programming. Theor. Comput. Sci., 410(2-3):202--220, 2009. Google ScholarDigital Library
- James C. King. Symbolic Execution and Program Testing. Communications of the ACM, 19(7):385--394, 1976. Google ScholarDigital Library
- Steven Lauterburg, Rajesh K. Karmani, Darko Marinov, and Gul Agha. Evaluating Ordering Heuristics for Dynamic Partial-Order Reduction Techniques. In Proc. of FASE'10, volume 6013 of LNCS, pages 308--322. Springer, 2010. Google ScholarDigital Library
- Christophe Meudec. ATGen: Automatic Test Data Generation using Constraint Logic Programming and Symbolic Execution. Softw. Test., Verif. Reliab., 11(2):81--96, 2001.Google ScholarCross Ref
- Roger A. Müller, Christoph Lembeck, and Herbert Kuchen. A Symbolic Java Virtual Machine for Test Case Generation. In Proc. of IASTEDSE'04, pages 365--371. ACTA Press, 2004.Google Scholar
- Jose M. Rojas and Miguel Gómez-Zamalloa. A Framework for Guided Test Case Generation in Constraint Logic Programming. In Proc. of LOPSTR'12, volume 7844 of LNCS. Springer, 2013.Google Scholar
- N. Rungta, E.G. Mercer, and W. Visser. Efficient Testing of Concurrent Programs with Abstraction-Guided Symbolic Execution. In Proc. of SPIN'09, volume 5578 of LNCS. Springer, 2009. Google ScholarDigital Library
- Olli Saarikivi, Kari Kahkonen, and Keijo Heljanko. Improving Dynamic Partial Order Reductions for Concolic Testing. In Proc. of ACSD'12, pages 132--141. IEEE Computer Society, 2012. Google ScholarDigital Library
- Koushik Sen and Gul Agha. Automated Systematic Testing of Open Distributed Programs. In Proc. of FASE'06, volume 3922 of LNCS, pages 339--356. Springer, 2006. Google ScholarDigital Library
- S. Tasharofi, R. K. Karmani, S. Lauterburg, A. Legay, D. Marinov, and G. Agha. TransDPOR: A Novel Dynamic Partial-Order Reduction Technique for Testing Actor Programs. In Proc. of FMOODS/FORTE'12, volume 7273 of LNCS, pages 219--234. Springer, 2012. Google ScholarDigital Library
- H. Zhu, P. A. V. Hall, and J. H. R. May. Software Unit Test Coverage and Adequacy. ACM Comput. Surv., 29(4):366--427, 1997. Google ScholarDigital Library
Index Terms
- Testing of concurrent and imperative software using CLP
Recommendations
Sophisticated Testing of Concurrent Programs
SSBSE '10: Proceedings of the 2nd International Symposium on Search Based Software EngineeringSearch-based techniques were successfully applied to many different areas of testing but according to our knowledge there are no works that applies search-based techniques to testing of concurrent software, yet. This PhD paper describes plans and ...
Testing atomicity of composed concurrent operations
OOPSLA '11: Proceedings of the 2011 ACM international conference on Object oriented programming systems languages and applicationsWe address the problem of testing atomicity of composed concurrent operations. Concurrent libraries help programmers exploit parallel hardware by providing scalable concurrent operations with the illusion that each operation is executed atomically. ...
A Scala library for testing student assignments on concurrent programming
SCALA 2016: Proceedings of the 2016 7th ACM SIGPLAN Symposium on ScalaWe present a lightweight library for testing concurrent Scala programs by systematically exploring multiple interleavings between user-specified operations on shared objects. Our library is targeted at beginners of concurrent programming in Scala, runs ...
Comments