AG 1, AG 2, AG 3, INET, AG 4, AG 5, D6, SWS, RG1, MMCI   Info

AG Audience

English

30 Minutes

The software industry today is defined by complex systems like parallel and distributed programs, with more integrated components and sophisticated features. The scale and complexity of such systems are growing rapidly, and the pace of development has never been faster. However, this progress comes at a cost. With larger, more complex software, issues like unreliability, vulnerabilities, and unintended behaviors also increase. Ensuring the safety and correctness of parallel and distributed systems is as important as adding new features. By performing rigorous verification of software systems, we can reduce the risks that lead to catastrophic failures. However, traditional software verification methods often struggle with scalability due to state space explosion. Stateless model checking and dynamic partial order reduction have emerged as promising techniques to address these challenges. The JMC project, developed by the RSE group at MPI-SWS, focuses on building a model checker for concurrent and distributed Java programs using these techniques. During my summer research internship at MPI-SWS, I contributed to the JMC project by extending its capabilities to support some fundamental concurrent primitives like synchronized methods, thread parking and unparking, and a message-passing API for modeling distributed protocols, considering DPOR semantics. In this presentation, I will provide an overview of the JMC project and discuss my contributions to this project.

Ina Geisler

+49 681 9325 1802

--email hidden

Zoom

passcode not visible

logged in users only