Guest Talk: Certified Concurrent and Distributed Systems by Dr. Mohsen Lesani

Dear All,

On Sunday, December 21th, Dr. Mohsen Lesani was the guest speaker on the topic of “Certified Concurrent and Distributed Systems”. The session held in Kharazmi Conference Hall at Computer Engineering Department, Sharif University of Technology.

photo329607820954675374

 

You can check the abstract, and a brief bio of Dr. Lesani below.

Abstract:
Aspects of concurrency and distribution pervasively appear in modern computing systems, including personal devices, data centers, aircrafts and medical devices. Due to complicated interactions between processes, concurrent and distributed systems are subtle and prone to bugs. Such bugs have led to death of patients and blackouts with millions of dollars financial loss. Can we build concurrent and distributed systems with static safety and security guarantees?

In this talk, I present how we can exploit advances in formal methods to develop correct-by-construction concurrent and distributed systems. In particular, I show how proof techniques for specific classes of algorithms can simplify and automate the proof of correctness of those classes. First, I introduce a proof technique called condensability and a tool called Snowflake to verify linearizability of composing concurrent data-structures in Java. Snowflake generates proof obligations for condensability and discharges them using the Z3 SMT solver. Snowflake successfully verified a large fraction of composing methods in several open-source applications. Second, I present a framework in Coq called Chapar for development and modular verification of causally consistent replicated key-value store implementations and their clients. Chapar includes a novel proof technique for causal consistency of key-value store implementations that was used to verify two key-value store implementations from the literature. Extraction from Coq to OCaml resulted in two executable stores with the static causal consistency guarantee. Finally, I describe my future plans to build certified byzantine fault-tolerant replicated stores.
Bio:
   Mohsen Lesani is an assistant professor at the Computer Science and Engineering Department of the University of California, Riverside. He spent his postdoc at MIT and obtained his PhD from UCLA. He is a BS and MS graduate from the University of Tehran and Sharif University of Technology. He has research experience with Scalable Synchronization Lab at Oracle (Sun) Labs and HP Labs. He is always looking for motivated students.   The overarching goal of his research is to make computing systems more reliable and efficient. He is broadly interested in formal methods and concurrent and distributed computing. He applies program analysis and verification techniques to specify and verify concurrent and distributed systems.
http://www.cs.ucr.edu/~lesani/

Posted in Uncategorized | Leave a comment

9th Seminar , 1395-06-28 (2016-09-18)

Dear All,

Ninth seminar was held on Sunday, 1395-06-14 (2016-09-04), at SQRLab Laboratory. Outline of session follows:

1- Ms. Mafi research talk about “Fastest: A Model-Based testing tool for Z Notation ”: about 30 min
2- Question, and Discussion: 30 min
3-Next seminar: Mr Varmarzyar
People attended this seminar are:
PhD: Zohreh Mafi, Mojtaba Varmazyar
MSc: Khashayar Etemadi, Sajad Jalali
Next seminar was also set on next two week. Mr. Varmarzyar will manage that session.

Related Resources can be reached in the link below:

Fastest: A Model-Based testing tool for Z Notation

Posted in Uncategorized | Leave a comment

8th Seminar , 1395-06-14 (2016-09-04)

Dear All,

Eighth seminar was held on Sunday, 1395-06-14 (2016-09-04), at SQRLab Laboratory. Outline of session follows:

1- Mr. Kholdi and Mr. Sekhavat (Bachelor students of Dr. mirian) research talk about “Decoupling Scenarios from Behavior-Driven Tests ”: about 30 min
2- Question, and Discussion: 30 min
3-Next seminar: Ms. Mafi
People attended this seminar are:
PhD: Zohreh Mafi, Mohammad salehe, Mojtaba Varmazyar
MSc: Khashayar Etemadi
Next seminar was also set on next two week at 9:00, Sunday. Mr. Etemadi will manage that session.

Related Slides can be reached in the link below:

Decoupling Scenarios from Behavior-Driven Tests

Posted in Uncategorized | Leave a comment

7th Seminar , 1395-05-24 (2016-08-14)

Dear All,

Seventh seminar was held on Sunday, 1395-05-24 (2016-08-14), at SQRLab Laboratory. Outline of session follows:

1- Mr. Etemadi’s research talk about “Mutation operators for testing Android apps ”: about 30 min
2- Question, and Discussion: 30 min
3-Next seminar: Mr. Kholdi and Mr. Sekhavat (Bachelor students of Dr. mirian)
People attended this seminar are:
PhD: Zohreh Mafi , Mehran Rivadeh, Mohammad salehe, Mojtaba Varmazyar
MSc: Khashayar Etemadi, Ali Nosrati
Next seminar was also set on next two week at 9:00, Sunday. Mr. Etemadi will manage that session.

Mr. Etemadi’s Slides can be reached in the link below:

Mutation operators for testing Android apps

Posted in Uncategorized | Leave a comment

6th Seminar , 1395-03-17 (2016-06-06)

Dear All,

Fifth seminar was held on Monday, 1395-02-27 (2016-05-16), at SQRLab Laboratory. Outline of session follows:

1- Mr. Salehe’s research talk about “Software Clones”: about 30 min
2- Question, and Discussion: 30 min
3-Next seminar: Mr. Etemadi
People attended this seminar are (in Alphabetical order):
  1. PhD: Zohreh Mafi, Mostafa Mahdie , Mehran Rivadeh, Mohammad salehe,  Mojtaba Varmazyar
  2. MSc: Sadjad Jalali, Ali Nosrati, Khashayar Etemadi

Next seminar was also set on next two week at 9:00. Mr. Salehe will manage that session.

Posted in Uncategorized | Leave a comment

5th Seminar , 1395-02-27 (2016-05-16)

Dear All,

Fifth seminar was held on Monday, 1395-02-27 (2016-05-16), at SQRLab Laboratory. Outline of session follows:

1- Mr. Nosrati and Mr. Jalali’s research talk about “Bug prediction”: about 30 min
2- Question, and Discussion: 30 min
3-Next seminar: Mr. Salehe
People attended this seminar are (in Alphabetical order):
  1. PhD: Zohreh Mafi, Mostafa Mahdie , Mehran Rivadeh, Mohammad salehe,  Mojtaba Varmazyar
  2. MSc: Sadjad Jalali, Ali Nosrati

Next seminar was also set on next two week at 8:00. Mr. Nosrati will manage that session.

 

Posted in Uncategorized | Leave a comment

4th Seminar , 1395-02-13 (2016-05-02)

Dear All,

Forth seminar was held on Monday, 1395-02-13 (2016-05-02), at SQRLab Laboratory. Outline of session follows:

1- Mr. Rivadeh’s research talk about “Business Process Management Systems”: about 30 min
2- Question, and Discussion: 30 min
3-Next seminar: Mr. Nosrati, and Mr. JalaliNedooshan
People attended this seminar are (in Alphabetical order):
  1. PhD: Zohreh Mafi,Mehran Rivadeh, Mojtaba Varmazyar
  2. MSc: Sadjad Jalali, Ali Nosrati

Next seminar was also set on next two week at 8:00. Mr. Rivadeh will manage that session.

Presentation Slides:(Business Process Management Systems) Link will be here asap.

Regards,

Zohreh Mafi

Posted in Rivadeh, Seminar | Leave a comment

Happy Teacher’s Day

IMG_3989Happy Teacher’s Day

1395/02/13

2016/05/02

Posted in Uncategorized | 1 Comment

1395/02/06 Meeting

Today’s meeting was postponed to next week.

Monday, 1395/02/11 @ 8:00 AM

Regards,

Zohreh Mafi

Posted in Uncategorized | Leave a comment

3rd Seminar ,1395-01-23 (2016-04-11)

Dear All,

Third seminar was held on Monday, 1395-01-23 (2016-04-11), at SQRLab Laboratory. Outline of session follows:

1- I talk about Test Driven Development: about 30 min
2- The last version of  Logo was unveiled. (thanking Mr Varmazyar)
3-Next seminar: Mr Rivadeh
People attended this seminar are (in Alphabetical order):
  1. PhD: Zohreh Mafi, Mostafa Mahdieh, Mehran Rivadeh,  Mojtaba Varmazyar
  2. MSc: Babak Barati, Sadjad Jalali, Ali Nosrati

Next seminar was also set on next two week.

Regards,

Zohreh Mafi

 

Presentation Slides : Test Driven Development (TDD)

Posted in Mafi, Seminar | Leave a comment