On learning assumptions for compositional verification of probabilistic systems

Thesis

Probabilistic model checking is a powerful formal verification method that can ensure the correctness of real-life systems that exhibit stochastic behaviour. The work presented in this thesis aims to solve the scalability challenge of probabilistic model checking, by developing, for the first time, fully-automated compositional verification techniques for probabilistic systems. The contributions are novel approaches for automatically learning probabilistic assumptions for three di...

Expand abstract

Authors: Feng, L

• Publication date: 2014
• Type of award: DPhil
• Level of award: Doctoral
• Awarding institution: University of Oxford
• Language: English
• Keywords: Computational learning; Assume-guarantee reasoning; Compositional verification; Probabilistic model checking
• Subjects: Applications and algorithms; Scalable systems; Software engineering; Computer science (mathematics); Theory and automated verification