Tomasz Mazur

Mr Tomasz Krzysztof Mazur

Doctoral Student

Former Member

College Lecturer, St Catherine's College

Student, St Catherine's College

Themes:

• Automated Verification

Completed Projects:

• CSP Model Checking

Interests

I do research on the thoery of concurrency and computer-aided formal verification. As the main modeling language I use CSP (Communicating Sequential Processes), a process algebra invented by C.A.R. Hoare (you can download his book on the topic here and a more comprehensive Theory and Practice of Concurrency by Bill Roscoe here).

My major interests are the possible ways of extending the current abilities of computer-aided model checking using counter abstraction, counterexample-guided abstraction refinement, predicate abstraction, process division and others. At the moment I specifically look at possible automatic partial solutions to the undecidable Paramaterised Model Checking Problem (PMCP) and the more general Paramaterised Verification Problem (PVP).

See also

• TomCAT - a tool for automatic creation of CSP counter abstraction models

Selected Publications

View AllManage publications

• Formal verification of not fully symmetric systems using counter abstraction

  Tomasz Mazur

  In Proceedings of the MOdelling and VErifying Process (MOVEP'08). 2008.

  Details about Formal verification of not fully symmetric systems using counter abstraction | BibTeX data for Formal verification of not fully symmetric systems using counter abstraction | Download (pdf) of Formal verification of not fully symmetric systems using counter abstraction

• Counter Abstraction in the CSP/FDR setting

  Tomasz Mazur and Gavin Lowe

  In Proceedings of the Seventh International Workshop on Automated Verification of Critical Systems (AVoCS'07). 2007.

  Details about Counter Abstraction in the CSP/FDR setting | BibTeX data for Counter Abstraction in the CSP/FDR setting | Download (pdf) of Counter Abstraction in the CSP/FDR setting

Activities

• Concurrency