PhD Thesis Defense Presentation

This presentation was used for the defense of the PhD thesis on static program verification with a focus on composing reachability tasks to improve efficiency and scalability.

The thesis addresses the challenge of verifying complex, real-world software systems that must satisfy a large number of functional and non-functional requirements. Instead of verifying each requirement independently, the proposed approach enables simultaneous verification of multiple requirements, reducing redundant analysis and improving resource utilization.

The developed methods extend model checking–based verification techniques by reusing intermediate results and overcoming the limitation of stopping after the first detected violation. Their applicability and effectiveness are demonstrated on Linux kernel modules, showing that requirement composition is a practical and promising direction for scalable static verification.