Proposals for Master's projects (Examensarbete)

• Hierarchical model mining of Software Product Lines. Software is nowadays often developed as product lines, giving rise to whole families of products, each of them customized for a particular customer. In previous work [paper] we developed a method to verify temporal properties of such families as a whole, using hierarchical models of the families to push a devide-and-conquer style reasoning. We are now investigating how to extract such models from existing software families [paper]. The project will study various algorithms for model extraction and their applicability to different types of program analysis, and will result in a proof-of-concept model extraction tool.
  
• Verification of temporal properties of Object Reference Programs. The project studies a particular class of programs, called object reference programs (ORPs), which are programs with object references as the only data type. Their behaviour can be defined through pushdown automata, which allows algorithmic verification of behavioural properties expressed in temporal logic. The project will investigate whether and how existing pushdown automata model checkers can be adapted or extended for the verification of ORPs, and will explore the practical value of the approach on some small ORPs derived from real programs.
  

• Combining symbolic execution with pushdown system model checking for program verification
• Comparing program models and logics for verification of temporal properties
  
• Developing a pushdown automata model checker for the modal mu-calculus
  
• A product construction for efficient computation of maximal flow graphs [paper]