About

I received my Bachelor's degree from University of Bojnord, Iran and Master's degree from University of Zanjan, Iran in Computer Engineering in 2014 and 2017, respectively. In my Master's thesis, I worked on parallelizing graph algorithms on GPUs. Since 2018, I have joined the Formal Methods and Tools group at the University of Twente to work on Mercedes project. In this project, I am working on developing automated verification techniques to reason about data race freedom and functional correctness of GPU programs. For more, you can download my CV.

Publications

  • M. Safari and A. Ebnenasir "Locality-Based Relaxation: An Efficient Method for GPU-Based Computation of Shortest Path". In International Conference on Topics in Theoretical Computer Science (TTCS), pp. 41-56, LNCS, Springer, 2017.

  • S. Joosten, W. Oortwijn, M. Safari and M. Huisman "An Exercise in Verifying Sequential Programs with VerCors". In Companion Proceedings for the ISSTA/ECOOP Workshop (FTfJP), pp. 40-45, 2018.

  • M. Huisman, S. Blom, S. Darabi and M. Safari "Program Correctness by Transformation". In International Symposium On Leveraging Applications of Formal Methods, Verification and Validation (ISoLA), pp. 365-380, LNCS, Springer, 2018.

  • M. Safari, W. Oortwijn, S. Joosten and M. Huisman "Formal Verification of Parallel Prefix Sum". In NASA Formal Methods Symposium (NFM), pp. 170-186, LNCS, Springer, 2020.

  • M. Safari and M. Huisman "A Generic Approach to the Verification of the Permutation Property of Sequential and Parallel Swap-Based Sorting Algorithms". In International Conference on Integrated Formal Methods (iFM), pp. 257-275, LNCS, Springer, 2020.

  • M. Safari and M. Huisman "Formal Verification of Parallel Stream Compaction and Summed- Area Table Algorithms". In International Colloquium on Theoretical Aspects of Computing (ICTAC), pp. 181-199, LNCS, Springer, 2020.

  • M. Safari, W. Oortwijn and M. Huisman "Automated Verification of the Parallel Bellman–Ford Algorithm". In International Static Analysis Symposium (SAS), pp. 346-358, Springer, Cham, 2021.

  • S. Blom, M. Huisman, S. Darabi and M. Safari "Correct Program Parallelisations". In International Journal on Software Tools for Technology Transfer (STTT), pp.1-23, 2021.

Research

Parallel Computing: GPGPU Computing, Parallelizing Data Structures and Algorithms

Formal Methods: GPGPU Correctness, Deductive Program Verification

Contact

Address: University of Twente, Faculty EEMCS, Formal Methods and Tools, Zilverling Building, room 3082, P.O. Box 217 7500 AE Enschede, The Netherlands.

Email: m.safari@utwente.nl

Elements

Text

This is bold and this is strong. This is italic and this is emphasized. This is superscript text and this is subscript text. This is underlined and this is code: for (;;) { ... }. Finally, this is a link.


Heading Level 2

Heading Level 3

Heading Level 4

Heading Level 5
Heading Level 6

Blockquote

Fringilla nisl. Donec accumsan interdum nisi, quis tincidunt felis sagittis eget tempus euismod. Vestibulum ante ipsum primis in faucibus vestibulum. Blandit adipiscing eu felis iaculis volutpat ac adipiscing accumsan faucibus. Vestibulum ante ipsum primis in faucibus lorem ipsum dolor sit amet nullam adipiscing eu felis.

Preformatted

i = 0;

while (!deck.isInOrder()) {
    print 'Iteration ' + i;
    deck.shuffle();
    i++;
}

print 'It took ' + i + ' iterations to sort the deck.';

Lists

Unordered

  • Dolor pulvinar etiam.
  • Sagittis adipiscing.
  • Felis enim feugiat.

Alternate

  • Dolor pulvinar etiam.
  • Sagittis adipiscing.
  • Felis enim feugiat.

Ordered

  1. Dolor pulvinar etiam.
  2. Etiam vel felis viverra.
  3. Felis enim feugiat.
  4. Dolor pulvinar etiam.
  5. Etiam vel felis lorem.
  6. Felis enim et feugiat.

Icons

Actions

Table

Default

Name Description Price
Item One Ante turpis integer aliquet porttitor. 29.99
Item Two Vis ac commodo adipiscing arcu aliquet. 19.99
Item Three Morbi faucibus arcu accumsan lorem. 29.99
Item Four Vitae integer tempus condimentum. 19.99
Item Five Ante turpis integer aliquet porttitor. 29.99
100.00

Alternate

Name Description Price
Item One Ante turpis integer aliquet porttitor. 29.99
Item Two Vis ac commodo adipiscing arcu aliquet. 19.99
Item Three Morbi faucibus arcu accumsan lorem. 29.99
Item Four Vitae integer tempus condimentum. 19.99
Item Five Ante turpis integer aliquet porttitor. 29.99
100.00

Buttons

  • Disabled
  • Disabled

Form