Final grades | |
All assignments were returned, and final grades were submitted. If you have any questions or an appeal, please email Anna. |
פורסם ב-1/10/2017, 01:46:27 Created on 1/10/2017, 01:46:27 Создано1/10/2017, 01:46:27 تم النشر ب-1/10/2017, 01:46:27 |
Materials for today's lecture and tutorial are online |
פורסם ב-3/7/2017, 13:06:36 Created on 3/7/2017, 13:06:36 Создано3/7/2017, 13:06:36 تم النشر ب-3/7/2017, 13:06:36 |
Homework assignment #5 is now available |
פורסם ב-26/6/2017, 20:02:53 Created on 26/6/2017, 20:02:53 Создано26/6/2017, 20:02:53 تم النشر ب-26/6/2017, 20:02:53 |
Materials for today's lecture and tutorial are online |
פורסם ב-26/6/2017, 12:31:05 Created on 26/6/2017, 12:31:05 Создано26/6/2017, 12:31:05 تم النشر ب-26/6/2017, 12:31:05 |
Materials for today's lecture and tutorial are online |
פורסם ב-19/6/2017, 06:16:23 Created on 19/6/2017, 06:16:23 Создано19/6/2017, 06:16:23 تم النشر ب-19/6/2017, 06:16:23 |
Homework #2 returned | |
The assignments with comments and grades are available on gr. |
פורסם ב-18/6/2017, 13:58:46 Created on 18/6/2017, 13:58:46 Создано18/6/2017, 13:58:46 تم النشر ب-18/6/2017, 13:58:46 |
Materials for today's lecture and tutorial are online | |
Also, you are invited to a lecture tomorrow: Time+Place : Tuesday 13/06/2017 14:30 room 337 Taub Bld. Speaker : Mooly Sagiv - COLLOQUIUM LECTURE - RESCHEDULED Affiliation: Tel-Aviv University, School of Computer Science Host : Yuval Filmus Title : Effective deductive verification of safety of distributed protocols in unbounded systems Abstract : Safety of a distributed protocol means that the protocol never reaches a bad state, e.g., a state where two nodes become leaders in a leader-election protocol. Proving safety is obviously undecidable since such protocols are run by an unbounded number of nodes, and their safety needs to be established for any number of nodes. I will describe a deductive approach for proving safety, based on the concept of universally quantified inductive invariants --- an adaptation of the mathematical concept of induction to the domain of programs. In the deductive approach, the programmer specifies a candidate inductive invariant and the system automatically checks if it is inductive. By restricting the invariants to be universally quantified, this approach can be effectively implemented with a SAT solver. This is a joint work with Ken McMillan (MSR), Oded Padon (TAU), Aurojit Panda (Berkeley), and Sharon Shoham(TAU) and was integrated into the IVY system http://www.cs.tau.ac.il/~odedp/ivy/ The work is inspired by Shachar Itzhaky's thesis available from http://people.csail.mit.edu/shachari/ Short Bio: ========== Mooly Sagiv is a professor in the School of Computer Science at Tel-Aviv University. He graduated from the Technion in 1991. He is a leading researcher in the area of large scale (inter-procedural) program analysis, and one of the key contributors to shape analysis. His fields of interests include programming languages, compilers, abstract interpretation, profiling, pointer analysis, shape analysis, inter-procedural dataflow analysis, program slicing, and language-based programming environments. Sagiv is a recipient of a 2013 senior ERC research grant for Verifying and Synthesizing Software Composition. Prof. Sagiv served as Member of the Advisory Board of Panaya Inc acquired by Infosys. He received best-paper awards at PLDI'11 and PLDI'12 for his work on composing concurrent data structures and a ACM SIGSOFT Retrospective Impact Paper Award (2011) for program slicing. He is an ACM fellow and a recipient of Microsoft Research Outstanding Collaborator Award 2016. ========================================== Refreshments will be served from 14:15 Lecture starts at 14:30 |
פורסם ב-12/6/2017, 12:52:27 Created on 12/6/2017, 12:52:27 Создано12/6/2017, 12:52:27 تم النشر ب-12/6/2017, 12:52:27 |
Correction: tomorrow's lecture and tutorial |
פורסם ב-4/6/2017, 18:04:30 Created on 4/6/2017, 18:04:30 Создано4/6/2017, 18:04:30 تم النشر ب-4/6/2017, 18:04:30 |
Materials for today's lecture and tutorial are online |
פורסם ב-4/6/2017, 17:57:59 Created on 4/6/2017, 17:57:59 Создано4/6/2017, 17:57:59 تم النشر ب-4/6/2017, 17:57:59 |
Homework assignment #4 is now available |
פורסם ב-1/6/2017, 12:34:10 Created on 1/6/2017, 12:34:10 Создано1/6/2017, 12:34:10 تم النشر ب-1/6/2017, 12:34:10 |
Reminder - there will be no 3rd hour tomorrow | |
The material for tomorrow in under Tutorial 8 |
פורסם ב-28/5/2017, 13:31:35 Created on 28/5/2017, 13:31:35 Создано28/5/2017, 13:31:35 تم النشر ب-28/5/2017, 13:31:35 |
Homework assignment #3 submition delayed | |
Homework assignment #3 due date is now 1.6.2017 The materials for today's tutorial were updated |
פורסם ב-22/5/2017, 18:37:01 Created on 22/5/2017, 18:37:01 Создано22/5/2017, 18:37:01 تم النشر ب-22/5/2017, 18:37:01 |
Materials for today's lecture and tutorial are online |
פורסם ב-22/5/2017, 11:37:33 Created on 22/5/2017, 11:37:33 Создано22/5/2017, 11:37:33 تم النشر ب-22/5/2017, 11:37:33 |
Lecture on "Modular Verification of Concurrent Programs via Sequential Model Checking" | |
You are kindly invited to the M.Sc. thesis seminar by Dan Rasin, if you are interested. Time and Place: Wednesday, 24.5.2017, 11:00 in Taub 601 Speaker: Dan Rasin Title: Modular Verification of Concurrent Programs via Sequential Model Checking Supervisor: Prof. Orna Grumberg and Dr. Sharon Shoham Abstract: Verification of concurrent programs is known to be extremely difficult. On top of the challenges inherent in verifying sequential programs, it adds the need to consider a high (typically unbounded) number of thread interleavings. In this work, we utilize the plethora of work on verification of sequential programs for the purpose of verifying concurrent programs. We introduce a technique which reduces the verification of a concurrent program to a series of verification tasks of sequential programs, without explicitly encoding all the possible interleavings. Our approach is modular in the sense that each sequential verification task roughly corresponds to the verification of a single thread, with some additional information about the environment in which it operates. Information regarding the environment is gathered during the run of the algorithm, by need. A unique aspect of our approach is that it exploits a hierarchical structure of the program in which one of the threads, considered main, is being verified as a sequential program. Its verification process initiates queries to its environment (which may contain multiple threads). Those queries are answered by sequential verification, if the environment consists of a single thread, or, otherwise, by applying the same hierarchical algorithm on the environment. Our technique is fully automatic, and allows us to use any off-the-shelf sequential model-checker. We implemented our technique in a tool called CoMuS and evaluated it against existing tools for concurrent verification. |
פורסם ב-15/5/2017, 21:12:07 Created on 15/5/2017, 21:12:07 Создано15/5/2017, 21:12:07 تم النشر ب-15/5/2017, 21:12:07 |
Lecture 6 slides are now available |
פורסם ב-15/5/2017, 13:16:08 Created on 15/5/2017, 13:16:08 Создано15/5/2017, 13:16:08 تم النشر ب-15/5/2017, 13:16:08 |
Homework assignment #3 is now available |
פורסם ב-9/5/2017, 14:46:59 Created on 9/5/2017, 14:46:59 Создано9/5/2017, 14:46:59 تم النشر ب-9/5/2017, 14:46:59 |
Homework #2 clarification | |
I've added the definition of R_T to q2 in hw2. |
פורסם ב-7/5/2017, 15:10:46 Created on 7/5/2017, 15:10:46 Создано7/5/2017, 15:10:46 تم النشر ب-7/5/2017, 15:10:46 |
Homework #1 returned | |
The assignments with comments and grades are available on gr. |
פורסם ב-3/5/2017, 20:44:47 Created on 3/5/2017, 20:44:47 Создано3/5/2017, 20:44:47 تم النشر ب-3/5/2017, 20:44:47 |
Homework #2 example | |
An example was added to q2 |
פורסם ב-3/5/2017, 16:42:23 Created on 3/5/2017, 16:42:23 Создано3/5/2017, 16:42:23 تم النشر ب-3/5/2017, 16:42:23 |
Homework #2 correction | |
I've added a definition to q2 (marked yellow). The due date was postponed to 8.5. |
פורסם ב-24/4/2017, 18:42:16 Created on 24/4/2017, 18:42:16 Создано24/4/2017, 18:42:16 تم النشر ب-24/4/2017, 18:42:16 |
Homework assignment #2 is now available |
פורסם ב-17/4/2017, 12:29:16 Created on 17/4/2017, 12:29:16 Создано17/4/2017, 12:29:16 تم النشر ب-17/4/2017, 12:29:16 |
Homework #1 comment | |
I've added a comment to question 1a, please prove any statement that was not proven (although given) in class. |
פורסם ב-29/3/2017, 13:41:03 Created on 29/3/2017, 13:41:03 Создано29/3/2017, 13:41:03 تم النشر ب-29/3/2017, 13:41:03 |
Homework assignment #1 is now available | |
Also, a summery of tutorial 1 is available under course material. |
פורסם ב-26/3/2017, 15:40:45 Created on 26/3/2017, 15:40:45 Создано26/3/2017, 15:40:45 تم النشر ب-26/3/2017, 15:40:45 |