TAU and Carnegie Mellon Join Forces to Host New School

For the first time, Carnegie Mellon University (CMU) and Tel Aviv University (TAU) held a joint international school this summer at TAU for software engineers.

The program, which was funded by The Lowy International School and ran for six days, was focused on formal specifications and analysis – in other words, improving quality control in the software development process.

The first three days of the program were lecture-based and covered foundational as well as recent research advancements, while the second half of the program was dedicated to a hackathon – where student teams worked on mini projects under the guidance of professors.

The school welcomed 13 graduate students from abroad (from the USA, Canada, Portugal, Argentina, Italy and Singapore), as well as four graduate students from TAU. Below, find out what four of these students had to say about the program!

Logan Murphy

PhD Student, Department of Computer Science, University of Toronto

1. Why did you decide to apply to the school and why is formal specifications & analysis important?

Software systems are playing an increasingly crucial role in our societies — for commerce, finance, medicine, defence, transportation, or any number of domains. If these systems fail, or behave in ways they shouldn’t, there can be really significant consequences. As a result, it’s really important to ask: what does it mean for software to be correct? And how can we check whether the software we build meets this standard? 

Formal specification and analysis — which are built on a rich foundation of mathematical logic — are the most valuable tools to help us answer such questions. Attending the SPECS summer school allowed me to learn more about the state of the art from leading experts in the field, and to discuss new ideas and emerging results with other graduate students.

2. What was your experience of the CMU-TAU SPECS International Summer School?

It was really an amazing experience. The city and campus were beautiful, and lots of fun to explore. The lectures were interesting, and the discussions between students and lecturers were very engaging and insightful. I especially enjoyed the second portion of the summer school, where we designed and conducted a mini-project inspired by the lecture material. This was a really great way for us to internalize the ideas that were presented, and allowed us to make tangible contributions to cutting-edge research topics.

3. Can you share a favourite memory from your time participating in the school?

I greatly enjoyed collaborating with another student for the mini-project. It was really cool to combine our different ideas and knowledge to identify interesting problems and to explore potential solutions. 

I also really liked exploring Tel Aviv with other students from all over the world. Since it was a new environment for all of us, we got to share in the curiosity and excitement of discovering such a unique city together.

4. Will your experience at the summer school be helpful for your own PhD research? If so, how?

Absolutely! At a basic level, I was able to absorb new ideas and techniques that will be invaluable in my own research going forward. But what’s more important are the relationships and collaborations I was able to begin with the students I met at the summer school. At the time of writing, we are still working together to build on the ideas we initiated during the summer school, with the hope of eventually turning them into full research publications. I’m super excited about these new directions, and I hope to maintain and build on these relationships well into the future.

Ana Jovanovic

PhD Candidate, Software Engineering, University of Texas at Arlington

1. Why did you decide to apply to the school and why is formal specifications & analysis important?

Formal specifications and analysis help us build quality software that satisfies the requirements declared by user and as a result does what the user intended in a correct way. These specifications help users validate and verify the system. Compared to machine learning, cybersecurity and AI, and software engineering more specifically, the field of formal specification is an underrepresented field. So logically, there aren’t that many opportunities to attend a school of this kind. As I am the only student in my school that is actively exploring this field, I was thrilled to see that there is a summer school and I applied immediately. 

2. What was your experience of the CMU-TAU SPECS International Summer School?

The whole experience was absolutely incredible! First of all, the organization was impeccable. We had all the necessary information prior arriving to Tel Aviv. People were extremely kind, helpful, and available to assist us at all times. The lectures were orchestrated in the same manner, where we had the opportunity to listen to experts from the field that gave us wonderful insights into their research, and as well encouraged us to participate in discussions. Just being there and soaking up the knowledge and ideas that were being thrown made a big impact on us as individual researchers. It’s definitely a unique feeling sitting in a room with people that are sharing the same research passion as you are and that are sincerely motivating and encouraging you to pursue the research path that you’ve chosen.

3. Can you share a favourite memory from your time participating in the school?

My favorite memory occurred on one of the last days. All of us gathered and went to explore the beach and the neighborhood of Neve Tzedek. As we were enjoying the sights, we participated in casual research discussions. I’ll never forget how each of us was showing happiness for feeling understood, appreciated and just being thankful for having the opportunity to brainstorm and talk about our research.

4. Will your experience at the summer school be helpful for your own PhD research? If so, how?

I can honestly say that being there, and sharing this experience with fellow formal specifications researchers inspired me to approach my research from another angle, and that gave me even more ideas to explore. As a researcher, this couldn’t be more exciting! On top of this, there aren’t that many students exploring Alloy, so being there with a few of them, and listening to two of the professors who are actively contributing to Alloy, made me feel extremely grateful for this experience.

Ilia Shevrin

PhD Student, Computer Science, Tel Aviv University

1. Why did you decide to apply to the school and why is formal specifications & analysis important?

I applied to the summer school because formal specifications are at the core of my research. Having the chance to connect and collaborate with other researchers in this field is particularly valuable and a great opportunity for me. Moreover, as my supervisor Prof. Shahar Maoz was one of the organizers, I had the chance to assist in the preparations for the summer school and give a presentation to the attendees. In general, how to write good formal specifications is a long-standing, still undeciphered question in software engineering, and the summer school is an excellent initiative towards answering it.

2. What was your experience of the CMU-TAU SPECS International Summer School?

I greatly enjoyed the summer school. First of all, I met students from around the globe, made connections, discussed cultural differences, and overall broadened my cultural perspective. Also, I had the chance to cooperate with many of the students on a professional level and participate in fruitful brainstorming. Finally, through their lectures, the summer school was an opportunity to hear from some leading researchers in the field.

3. Can you share a favorite memory from your time participating in the school?

I recall very positively the hackathon experience in the last two and a half days of the summer school. During those days, the theoretical lectures and discussions boiled down to hands-on programming of tools related to formal specification analysis. It was challenging and engaging to see how we can team up and apply in practice the ideas that we talked about a few days earlier. It was also very interesting to listen to the ideas of the other teams at the end of the school.

4. Will your experience at the summer school be helpful for your own PhD research? If so, how?

I can say that I already have a prospect for several exciting research directions concerning further use cases of reactive synthesis specifications, in collaboration with one of the participants in the summer school. Furthermore, I gained some experience in presenting, and in teaching and illustrating reactive synthesis to various audiences.

Ian Dardik

PhD Student, Software Engineering, Carnegie Mellon University

1. Why did you decide to apply to the school and why is formal specifications & analysis important?

Formal specification and analysis (formal methods) are important because they yield principled and systematic analyses of software systems. A classic comparison to formal methods is “software testing”—while testing is simple and powerful, it is generally unclear where a system’s “blind spots” are from testing alone. Formal methods offer more systematic techniques such as theorem proving, which lacks blind spots (under certain assumptions), and robustness analysis, which identifies blind spots.

I decided to apply to the summer school for two primary reasons. 1) to learn about Alloy and Spectra, two formal methods tools which the school focused on, and 2) to network with formal methods researchers around the globe and learn about their work.

2. What was your experience of the CMU-TAU SPECS International Summer School?

I had an excellent experience at SPECS. During the day we listened to lectures or participated in the hackathon. In the evening we went out for dinner and drinks and got to know each other.

One of my favorite aspects of the school was the ample opportunity for active—as opposed to passive—learning. Lectures often seemed more like a discussion rather than a person at a podium talking. I give lots of credit to the professors at the school for continually asking great questions. There were ample snack breaks in which we got to network, mingle, and get to know each other. We were a group of (probably) less than 15 students, so I definitely knew everyone by the end of the week. Finally, I thought the hackathon at the end was an awesome way for us to engage in our newly learned skills.

A huge advantage of active learning and discussions was that it helped us get to know each other very quickly. I very much enjoyed interacting with my peers and I forged relationships that I expect to continue in the future.

3. Can you share a favourite memory from your time participating in the school?

My favorite memory from the school was on the second (middle) day of the hackathon. I had been trying to hack up a modified version of the Alloy tool for our project for almost two whole days. I had looked at the Alloy codebase for the first time the day before, so I didn’t expect to succeed. However, after two days of coding and talking with Eunsuk, Alcino, and my group members, we finally got the project working at like 5 or 6 p.m. We showed our working project to everyone in the room and Eunsuk said “well, should we call it a day and get a beer?” Of course, we all said yes :D

4. Will your experience at the summer school be helpful for your own PhD research? If so, how?

This is a very interesting question. Certainly, my experience will be indirectly useful for my research since it has exposed me to new tools and concepts related to formal methods.

My experience at the summer school is not directly related to the research projects I am working on at the moment, however it is certainly possible that we could continue the work we started in the hackathon project and potentially write a paper. In this aspect, the school would not have just seeded the idea for the paper, but also introduced me to the other members who I would be working with.

During Claudio’s second lecture, he introduced the concept of a “topological proof.” This concept seems similar to the “robustness” notion that I am currently researching, and it is possible that “topological proofs” can help us in the future. There may even be room for collaboration.