home consortium project research publications training softwareprivate

Summer school





@ 2012 - Site Map - Credits


arrowoxford arrow

Wellington Square Oxford,

Phone:+44 (0)1865 283509

Team members
Marta Kwiatkowska

Marta Kwiatkowska


Hongyang Qu

Hongyang Qu

Post doc researcher

Chris Chilton

Chris Chilton

DPhil Student

The Chancellor, Masters and Scholars of the
University of Oxford

The University of Oxford is one of world’s best universities ( The distinctive college and tutorial system underpins a culture of close academic supervision and careful personal support for students. The University is represented by Oxford University Computing Laboratory (OUCL, OUCL research activities are broadly divided into five themes among which the Theory and Automated Verification theme.

Expertise brought to CONNECT

The Quantitative Analysis and Verification (QAV) group, embedded within the Theory and Automated Verification theme, brings to CONNECT its research expertise in formal methods for modeling and verification of concurrent systems, both theory and practice. The group has extensive experience in process algebraic models for probabilistic processes, algorithmic verification for probabilistic systems, as well as implementation techniques for automated verification tools and their application to real-world case studies. The world leading probabilistic model checker PRISM ( implemented by the group has been applied to model several wireless, security and anonymity protocols and analyze their non-functional properties, including dependability and QoS. Currently, the group is working on extending quantitative verification to ubiquitous/pervasive computing, focusing on context-aware software, mobility and adaptive behavior.

Contribution to CONNECT research

Within CONNECT, the QAV group contributes to the compositional algebra of connectors by contributing techniques to handle non-functional properties, extend quantitative automated verification techniques to the Connect setting, and investigate the foundations for assume-guarantee reasoning in the quantitative case. The QAV group also contributes by applying the developed toolset to analyze dependability of examples of CONNECT protocols and quantitative approaches to privacy and trust.

The CONNECT project acknowledges the financial support of the Future and Emerging Technologies (FET) programme within the ICT theme of the Seventh Framework Programme for Research of the European Commission.