Verifying Parallel Code After Refactoring Using Equivalence Checking

1. Parkhurst, J., Darringer, J., Grundmann, B.: From single core to multi-core: preparing for a new exponential. In: Proceedings of the 2006 IEEE/ACM International Conference on Computer-Aided Design, ICCAD’06, pp. 67–72. ACM, New York (2006)

2. Sutter, H.: The free lunch is over: a fundamental turn toward concurrency in software. Dr. Dobb’s J. 30(3), 202–210 (2005)

   Google Scholar 

3. Dig, D., Marrero, J., Ernst, M.D.: Refactoring sequential Java code for concurrency via concurrent libraries. In: Proceedings of the 31st International Conference on Software Engineering, ICSE’09, pp. 397–407. IEEE Computer Society, Washington, DC (2009)

4. Aldinucci, M., Torquati, M., Meneghin, M.: Fastflow: efficient parallel streaming applications on multi-core. CORR (2009). arXiv:0909.1187

5. Broquedis, F., Diakhaté, F., Thibault, S., Aumage, O., Namyst, R., Wacrenier, P.-A.: Scheduling dynamic openMP applications over multicore architectures. In: Eigenmann, R., Supinski, B. (eds.) OpenMP in a New Era of Parallelism. Lecture Notes in Computer Science, vol. 5004, pp. 170–180. Springer, Berlin (2008)

   Chapter  Google Scholar 

6. Lea, D.: A Java fork/join framework. In: Proceedings of the ACM 2000 Conference on Java Grande, JAVA’00, pp. 36–43. ACM, New York (2000)

7. Pheatt, C.: Intel\({}^{\textregistered }\) threading building blocks. J. Comput. Sci. Coll. 23(4), 298–298 (2008)

   Google Scholar 

8. Janjic, V., Brown, C., Mackenzie, K., Hammond, K., Danelutto, M., Aldinucci, M., Garcia, J.D.: RPL: a domain-specific language for designing and implementing parallel C++ applications. In: 2016 24th Euromicro International Conference on Parallel, Distributed, and Network-Based Processing (PDP), pp. 288–295. IEEE (2016)

9. Chen, F., Yang, H., Chu, W.C.C., Xu, B.: A program transformation framework for multicore software reengineering. In: 2012 12th International Conference on Quality Software, pp. 270–275 (Aug. 2012)

10. Godefroid, P., Klarlund, N., Sen, K.: DART: directed automated random testing. In: ACM Sigplan Notices, vol. 40, pp. 213–223. ACM (2005)

11. Sen, K., Agha, G.: CUTE and jCUTE: concolic unit testing and explicit path model-checking tools. In: Ball T., Jones R.B. (eds.) Computer Aided Verification (CAV), pp. 419–423. Springer, Berlin (2006). https://doi.org/10.1007/11817963_38

12. Cadar, C., Godefroid, P., Khurshid, S., Păsăreanu, C.S., Sen, K., Tillmann, N., Visser, W.: Symbolic execution for software testing in practice: preliminary assessment. In: Proceedings of the 33rd International Conference on Software Engineering, pp. 1066–1071. ACM (2011)

13. Păsăreanu, C.S., Visser, W.: A survey of new trends in symbolic execution for software testing and analysis. Int. J. Softw. Tools Technol. Transf. 11(4), 339–353 (2009)

    Article  Google Scholar 

14. Cadar, C., Dunbar, D., Engler, D.R.: KLEE: unassisted and automatic generation of high-coverage tests for complex systems programs. OSDI 8, 209–224 (2008)

    Google Scholar 

15. Barner, S., Eisner, C., Glazberg, Z., Kroening, D., Rabinovitz, I.: ExpliSAT: guiding SAT-based software verification with explicit states. In: Hardware and Software, Verification and Testing, pp. 138–154. Springer (2007)

16. Chockler, H., Pidan, D., Ruah, S.: Improving representative computation in ExpliSAT. In: Hardware and Software: Verification and Testing, pp. 359–364. Springer (2013)

17. Torquati, M.: Single-producer/single-consumer queues on shared cache multi-core systems. CoRR (2010). arXiv:1012.1824

18. The mandelbrot set in C++11. http://solarianprogrammer.com/2013/02/28/mandelbroot-set-cpp-11

19. Escape time algorithm. https://en.wikipedia.org/wiki/Mandelbrot_set#Escape_time_algorithm

20. Boyer, R.S., Elspas, B., Levitt, K.N.: Select—a formal system for testing and debugging programs by symbolic execution. In: Proceedings of the International Conference on Reliable Software, pp. 234–245

21. King, J.C.: Symbolic execution and program testing. Commun. ACM 19(7), 385–394 (1976)

    Article  MathSciNet  MATH  Google Scholar 

22. Chaki, S., Gurfinkel, A., Strichman, O.: Regression verification for multi-threaded programs. In: International Workshop on Verification, Model Checking, and Abstract Interpretation, pp. 119–135. Springer (2012)

23. Fedyukovich, G., Sery, O., Sharygina, N.: eVolCheck: incremental upgrade checker for C. In: Piterman N., Smolka S.A. (eds.) 19th International Conference on Tools and Algorithms for the Construction and Analysis of Systems, pp. 292–307. Springer, Berlin (2013)

24. Schuts, M., Hooman, J., Vaandrager, F.: Refactoring of legacy software using model learning and equivalence checking: an industrial experience report. In: International Conference on Integrated Formal Methods, pp. 311–325. Springer (2016)

25. Cranen, S., Groote, J.F., Keiren, J.J., Stappers, F.P., de Vink, E.P., Wesselink, W., Willemse, T.A.: An overview of the mCRL2 toolset and its recent advances. In: International Conference on Tools and Algorithms for the Construction and Analysis of Systems, pp. 199–213. Springer (2013)

26. Siegel, S.F., Mironova, A., Avrunin, G.S., Clarke, L.A.: Using model checking with symbolic execution to verify parallel numerical programs. In: Proceedings of the 2006 International Symposium on Software Testing and Analysis, pp. 157–168. ACM (2006)

27. Siegel, S.F., Zirkel, T.K.: Automatic formal verification of MPI-based parallel programs. SIGPLAN Not. 46(8), 309–310 (2011)

    Article  Google Scholar 

Download references