The advent of Massive Open Online Courses makes it essential to develop tools and techniques that automatically support computer science students in solving programming assignments. Complementing existing tools for automatically checking the correctness of students' programs, we have developed and evaluated an incremental hint system for programming exercises. The hint system displays, upon request from a student, a series of hints on how to approach a solution. The hints are created in advance from the source code of the exercise's reference solution using our hint generation tool. This tool can run in fully automatic mode, where hints reveal more and more parts of the solution code; in manual mode, where teachers can customize hints by annotating the input source code; and in a combination of the two modes. We evaluated the hint system throughout our Introduction to Programming course which provides a companion online course. The findings suggest that students who needed assistance with an exercise used the hint system and found it helpful to guide them through the process of building a solution.

Reachability from a program variable v to a program variable w states that from v , it is possible to follow a path of memory locations that leads to the object bound to w . We present a new abstract domain for the static analysis of possible reachability between program variables or, equivalently, definite unreachability between them. This information is important for improving the precision of other static analyses, such as side-effects, field initialization, cyclicity and path-length analysis, as well as more complex analyses built upon them, such as nullness and termination analysis. We define and prove correct our reachability analysis for Java bytecode, defined as a constraint-based analysis, where the constraint is a graph whose nodes are the program points and whose arcs propagate reachability information in accordance to the abstract semantics of each bytecode instruction. For each program point p , our reachability analysis produces an overapproximation of the ordered pairs of variables 〈 v , w 〉 such that v might reach w at p . Seen the other way around, if a pair 〈 v , w 〉 is not present in the overapproximation at p , then v definitely does not reach w at p . We have implemented the analysis inside the Julia static analyzer. Our experiments of analysis of nontrivial Java and Android programs show the improvement of precision due to the presence of reachability information. Moreover, reachability analysis actually reduces the overall cost of nullness and termination analysis.

Reliable and secure system design requires an increasing number of methods, algorithms, and tools for automatic program manipulation. Any program change corresponds to a transformation that affects the semantics at some given level of abstraction. We call these techniques model deformations. In this paper we propose a mathematical foundation for completeness-driven deformations of transition systems w.r.t. a given abstraction, and we introduce an algorithm for systematic deformation of Kripke structures for inducing strong preservation in abstract model checking. We prove that our model deformations are deeply related with must and may transitions in modal transition systems.