Master thesis projects: Model-based software analytics

Cyrille Artho

Our lives are controlled by software in many ways, from digital services to control and safety systems in cars, trains, and airplanes. Good specifications are vital to assess these systems but are hard to write and understand.
Model-based methods provide a visual, general way of reasoning about systems and their security. Within this domain, we offer a variety of thesis projects on software technology
and its applications in model-based analytics:

1. Visual analytics of software systems and models: Seeing is believing! Visualizations let us assess large data sets at a glance and let us see patterns in systems that in turn lead to better models.
2. Test generation: Models can describe millions of possible tests, and our tool Modbat has been used in the past to generate tests that found bugs in Java 8 and Apache ZooKeeper. gitlab.com/cartho/modbat
3. Smart contracts are a domain where large financial resources are at stake. Yet, ensuring their security before they are deployed remains a challenge. Model-based approaches combine usability with rigor and can prevent exploits.
4. Concurrency in parallel programs creates complexity that overwhelms human experts. JPF, an open-source tool originally released by NASA in 2005, allows us to systematically explore all behaviors in programs and protocols. github.com/javapathfinder/jpf-core
5. Other ideas regarding programming languages and application domains are welcome! Contact me at artho@kth.se  to start a discussion.