References

• 1. 1)
     • 1. Horowitz, M., Indermaur, T., Gonzalez, R.: ‘Low-power digital design’. IEEE Symp. on Low Power Electronics, San Diego, CA, USA, 1994, pp. 8–11.
  2. 2)
     • 2. Turjan, A.: ‘Compiling nested loop programs to process networks’. PhD thesis, Leiden University, 2007.
  3. 3)
     • 3. Turjan, A., Kienhuis, B., Deprettere, E.: ‘Translating affine nested-loop programs to process networks’. CASES'04, Washington DC, USA, 2004, pp. 220–229.
  4. 4)
     • 4. Kahn, G.: ‘The semantics of a simple language for parallel programming’. Proc. of IFIP Congress, Stockholm, Sweden, 1974, pp. 471–475.
  5. 5)
     • 5. Compaan, 2000.
  6. 6)
     • 6. Artemis, 2005. Available at http://ce.et.tudelft.nl/artemis/.
  7. 7)
     • 7. Daedalus, 2008. Available at http://daedalus.liacs.nl/Site/Daedalus home.html.
  8. 8)
     • 8. Metropilis, 2008. http://embedded.eecs.berkeley.edu/metropolis/.
  9. 9)
     • 9. Nikolov, H., Stefanov, T., Deprettere, E.: ‘Systematic and automated multiprocessor system design, programming, and implementation’, IEEE TCAD ICS, 2008, 27, (3), pp. 542–555.
  10. 10)
      • 10. Davare, A., Zhu, Q., Sangiovanni-Vincentelli, A.: ‘A platform-based design flow for kahn process networks’. Technical Report 2006-30, UC Berkeley, March 2006.
  11. 11)
      • 11. Fei, Y., Ravi, S., Raghunathan, A., et al: ‘Energy-optimizing source code transformations for operating system-driven embedded software’, Trans. Embedded Comput. Syst., 2007, 7, (1), pp. 1–26.
  12. 12)
      • 12. Meijer, S., Nikolov, H., Stefanov, T.: ‘On compile-time evaluation of process partitioning transformations for kahn process networks’. CODES-ISSS'09, Grenoble, France, 2009, pp. 31–40.
  13. 13)
      • 13. Meijer, S., Nikolov, H., Stefanov, T.: ‘Throughput modeling to evaluate process merging transformations in polyhedral process networks’. Proc. of Int. Conf. Design, Automation and Test in Europe (DATE'10), Dresden, Germany, 2010, pp. 747–752.
  14. 14)
      • 14. Kundu, S., Tatlock, Z., Lerner, S.: ‘Proving optimizations correct using parameterized program equivalence’. PLDI ‘09, Dublin, Ireland, 2009, pp. 327–337.
  15. 15)
      • 15. Kundu, S., Lerner, S., Gupta, R.: ‘Translation validation of high-level synthesis’, IEEE Trans. CAD ICS, 2010, 29, (4), pp. 566–579.
  16. 16)
      • 16. Shashidhar, K.C.: ‘Efficient automatic verification of loop and data-flow transformations by functional equivalence checking’. PhD thesis, Department of Computer Science, Katholieke Universiteit Leuven, Belgium, 2008.
  17. 17)
      • 17. Karfa, C., Banerjee, K., Sarkar, D., et al: ‘Verification of loop and arithmetic transformations of array-intensive behaviors’, IEEE Trans. CAD ICS, 2013, 32, (11), pp. 1787–1800.
  18. 18)
      • 18. Karfa, C., Sarkar, D., Mandal, C.: ‘Verification of KPN level transformations’. 26th Int. Conf. on VLSI Design, Pune, India, 2013, pp. 338–343.
  19. 19)
      • 19. Kumar, A., Fernando, S., Ha, Y., et al: ‘Multiprocessor systems synthesis for multiple use-cases of multiple applications on fpga’, ACM Trans. Des. Autom. Electron. Syst., 2008, 13, (3), pp. 40:1–40:27.
  20. 20)
      • 20. Milner, R.: ‘A calculus of communicating systems’ (Springer-Verlag, Berlin, Heidelberg, 1982).
  21. 21)
      • 21. Hoare, C.A.R.: ‘Communicating sequential processes’, Commun. ACM, 1978, 21, (8), pp. 666–677.
  22. 22)
      • 22. Bergstra, J., Klop, J.: ‘Process algebra for synchronous communication’, Inf. Control, 1984, 60, (1), pp. 109–137.
  23. 23)
      • 23. Hennessy, M., Milner, R.: ‘On observing nondeterminism and concurrency’. Proc. of the 7th Colloquium on Automata, Languages and Programming, Berlin, Heidelberg, 1980, pp. 299–309.
  24. 24)
      • 24. Park, D.: ‘Concurrency and automata on infinite sequences’. Proc. of the 5th GI-Conf. on Theoretical Computer Science, London, UK, 1981, pp. 167–183.
  25. 25)
      • 25. Pnueli, A.: ‘The temporal logic of programs’. 18th Annual Symp. on Foundations of Computer Science (sfcs 1977), San Diego, California, USA, October 1977, pp. 46–57.
  26. 26)
      • 26. Clarke, E.M., Emerson, E.A.: ‘Design and synthesis of synchronization skeletons using branching-time temporal logic’. Logic of Programs, Workshop, Berlin, Heidelberg, 1982, pp. 52–71.
  27. 27)
      • 27. Queille, J.-P., Sifakis, J.: ‘Specification and verification of concurrent systems in cesar’. Proc. of the 5th Colloquium on Int. Symp. on Programming, London, UK, 1982, pp. 337–351.
  28. 28)
      • 28. Holzmann, G.J.: ‘The model checker spin’, IEEE Trans. Softw. Eng., 1997, 23, pp. 279–295.
  29. 29)
      • 29. McMillan, K.L.: ‘Symbolic model checking’ (Kluwer Academic Publishers, Norwell, MA, USA, 1993).
  30. 30)
      • 30. Fernandez, J.-C., Garavel, H., Kerbrat, A., et al: ‘Cadp – a protocol validation and verification toolbox’. Proc. of the 8th Int. Conf. on Computer Aided Verification, CAV ‘96, London, UK, 1996, pp. 437–440.
  31. 31)
      • 31. Burch, J.R., Clarke, E.M., Long, D.E., et al: ‘Symbolic model checking for sequential circuit verification’, IEEE Trans. Comput.-Aided Des. Integr. Circuits Syst., 1994, 13, (4), pp. 401–424.
  32. 32)
      • 32. Godefroid, P.: ‘Using partial orders to improve automatic verification methods’. Proc. of the 2Nd Int. Workshop on Computer Aided Verification, CAV ‘90, Berlin, Heidelberg, 1991, pp. 176–185.
  33. 33)
      • 33. Dams, D., Gerth, R., Grumberg, O.: ‘Abstract interpretation of reactive systems’, ACM Trans. Program. Lang. Syst., 1997, 19, (2), pp. 253–291.
  34. 34)
      • 34. Clarke, E.M., Enders, R., Filkorn, T., et al: ‘Exploiting symmetry in temporal logic model checking’, Form. Methods Syst. Des., 1996, 9, (1–2), pp. 77–104.
  35. 35)
      • 35. Abadi, M., Lamport, L.: ‘Conjoining specifications’, ACM Trans. Program. Lang. Syst., 1995, 17, (3), pp. 507–535.
  36. 36)
      • 36. Strehl, K., Thiele, L.: ‘Interval diagrams for efficient symbolic verification of process networks’, IEEE Trans. CAD ICS, 2000, 19, (8), pp. 939–956.
  37. 37)
      • 37. Raudvere, T., Sander, I., Jantsch, A.: ‘Application and verification of local nonsemantic-preserving transformations in system design’, IEEE Trans. CAD ICS, 2008, 27, (6), pp. 1091–1103.
  38. 38)
      • 38. Chen, X., Hsieh, H., Balarin, F., et al: ‘Formal verification for embedded system designs’, Des. Autom. Embedded Syst., 2003, 8, pp. 139–153.
  39. 39)
      • 39. Kienhuis, B., Rijpkema, E., Deprettere, E.F.: ‘Compaan: deriving process networks from matlab for embedded signal processing architectures’. CODES'00, San Diego, CA, USA, 2000, pp. 13–17.
  40. 40)
      • 40. Manna, Z.: ‘Mathematical theory of computation’ (McGraw-Hill Kogakusha, Tokyo, 1974).
  41. 41)
      • 41. lp_solve, 2010. http://lpsolve.sourceforge.net/5.5/.
  42. 42)
      • 42. The Yices SMT Solver. Available at http://yices.csl.sri.com/.
  43. 43)
      • 43. Kelly, W., Rosser, E., Pugh, B., et al: ‘The omega calculator and library’, version 2.1, 2008. Available at http://www.cs.umd.edu/projects/omega/.
  44. 44)
      • 44. Cheung, E., Chen, X., Hsieh, H., et al: ‘Runtime deadlock analysis for system level design’, Des. Autom. Embedded Syst., 2009, 13, pp. 287–310.
  45. 45)
      • 45. Jiang, B., Deprettere, E., Kienhuis, B.: ‘Hierarchical run time deadlock detection in process networks’. IEEE Workshop on Signal Processing Systems, Washington DC, USA, 2008, pp. 239–244.
  46. 46)
      • 46. Olson, A., Evans, B.: ‘Deadlock detection for distributed process networks’. IEEE Int. Conf. on Acoustics, Speech, and Signal Processing, Philadelphia, PA, USA, 2005, vol. 5, pp. v/73–v/76.
  47. 47)
      • 47. Parks, T.M.: ‘Bounded scheduling of process networks’. PhD thesis, EECS Department, University of California, Berkeley, 1995.
  48. 48)
      • 48. Oppen, D.C.: ‘A 222pn upper bound on the complexity of presburger arithmetic’, J. Comput. Syst. Sci., 1978, 16, (3), pp. 323–332.