Review Comments ICT4S

Reviewer 1

• However, I would suggest moving the motivating example paragraph immediately after the paragraph you define your scope. It is at this point the user can benefit from a tangible example of a software controlling an external device. Your last paragraph in the introduction should be the one that starts with, "Our contribution is threefold."
• In methodology, "Our system summarizes..." should say "Our symbolic execution engine summarizes..."
• the authors need to briefly explain what is symbolic execution, and why THEY needed to create one. This goes back to my comment in the introduction -- be explicit on how your system differs from simulations and why your system is better. This is not clear except to readers who understand the intricate nuances of this field already.
• The authors need to better motivate the reason for merging skylines. The example in Figure 3 is really too simple to be compelling

Reviewer 2

• Figure 1 : whats is the unit of y axis/power draw ? Does it represents an average value ?
• In Figure 3 legend : y -axis is not described at all
• Section : define SECA when it is used for the first time

Reviewer 3

• The authors did not properly describe the required assumptions/limitations of the kind of systems to be considered. The great majority of power charge control systems depend on a varied set of external factors.
• The acronym SMT (Satisfiability Modulo Theories) is not presented. The target audience might not know what it is.