Dissemination of ExCAPE's view is done via multiple channels. We have held a summer school at Berkeley in June 2013, and plan another summer school in MIT in June 2015. We have turned the ExCAPE's meetings into mini-workshops, attended by many researchers in academia and industry outside ExCAPE, and have organized various workworshop, conferences, and competitions around ExCAPE's themes. Our monthly webinar provides an excellent opportunity for the community to learn about different aspects of synthesis on a regular basis. Each talk is attended by aroud 50 participants from all over the country.
Above that, we have realized that technology for formal verification and synthesis can contribute to online learning by analyzing students’ solutions to provide meaningful personalized explanation of their mistakes, and also by automatic grading. We have built such tools for representative topics in three undergraduate courses: introduction to programming, theory of computation, and design of cyber-physical systems. The design of these tools not only uses computational engines built for synthesis by ExCAPE researchers, but also integrates HCI research on user interaction and tool evaluation. These tools are already deployed in MOOCs as well as classrooms, and have been used outside ExCAPE institutions. For example, the tool AutomataTutor was used by 300 undergraduate students at Reykjavik University in Iceland in Spring 2014, and received glowing reviews. See more on this in the personalized education page.
ExCAPE Summer School was held on Berkeley Campus from June 12 to June 15, 2013. The summer school goal was to expose graduate students and junior researchers to new ideas in program synthesis. The school started with three tutorials with hands on sessions:
- Reactive Synthesis by Vardi and Ehlers,
- Synthesizing Programs with Constraint Solvers by Bodik and Torlak,
- Synthesis for Cyber-Phisical Systems by Tabuada and Rungger.
Supporting lectures were given by ExCAPE PIs Tripakis, Seshia, Lafortune, Solar-Lezama. We had three invited speakers:
- Sumit Gulwani (Microsoft Research): Synthesis for computer-aided education,
- Richard Murray (Caltech): Syntehsis for embedded control software and
- Alexandre Donze (Berkeley): Requirement Synthesis for Industrial-Scale Control Systems.
The school attracted 89 attendees, ranging from undergraduate students to faculty, from over twelve different countries. The feedback we received was overwhelming: 80% of the participants ranked the school as very good or excellent, and the tutorials were rated as effective or extremely effective by the majority of participants. We plan to hold similar such summer schools on 2015 and 2017.
In the past year we held three main meetings:
- ExCAPE Annual Meeting, Berkeley, June 10-11, 2013,
- NSF Site Visit, Penn, Aug 20, 2013, and
- ExCAPE Spring Meeting, joint with ARiSE, Berkeley, Mar 10-11, 2014.
All meetings where organized with sessions around ExCAPE’s themes. In the annual meeting the challenge problems were organized in parallel sessions, and there was a poster session with 22 posters, and a panel session about Software Design Methodology Research in the Age of Big Data and Flying Robots with panelists Patrice Godefroid (Microsoft Research), Aarti Gupta (NEC Labs), Moshe Vardi (Rice University), Mark Wegman (IBM Research), Pieter Mosterman (Mathworks). The Spring meeting was joint with the Austrian Society for Rigorous Systems Engineering ARiSE. It consisted of 50 short talks, including the following invited talks:
- Edwawrd Lee (Berkeley): The TerraSwarm Research Center
- Sumit Gulwani (Microsoft): Inductive Meta-Synthesizers
- Patrice Godefroid (Microsoft): Dynamic Program Verification + Micro Execution
- Jyo Deshmukh (Tema Toyota): Simulation-Guided Formal Analysis
- Susmit Jha (Intel): Adaptive Computing using Automated Synthesis
the first of which was designated as keynote speaker. In addition the last part of the meeting was dedicated to discussing possible directions for new collaborations. The third meeting was the largest of all three, attended by more than 70 participants, including all ExCAPE PIs, researchers from ARiSE and industry.
ExCAPE Robotics Workshop was held on Rice campus from November 20 to 22, 2013. The workshop was designed for the groups involved with the ExCAPE robotics challenge to get together, give tutorials on their computational tools, and have focused discussions. The purpose of the workshop was threefold: (1) hands-on tutorial on synthesis tools for robotic systems, (2) project updates through presentations, and (3) discussions on the possible future directions and collaborations. On the first day of the workshop, hands-on tool tutorials were given. The tutorials were on Open Motion Planning Library (OMPL) developed by Kavraki’s group, Linear Temporal Logic MissiOn Planning (LTLMoP) developed by Kress-Gazit’s group, and Pessoa, a tool for embedded control software synthesis, developed by Tabuada’s group. The second day of the workshop was dedicated to project updates, discussions, and comments. On the last day, subgroups were formed to further discuss joint projects and explore possible collaborations based on the themes emerged on the previous day. As a result, new collaborations were initiated on five designated topics, each topic explored by different subgroups of the researchers at Cornell, Michigan, Penn, Rice and UCLA.
Online education is becoming a dominating media for acquiring knowledge. Several challenges have emerged in the development of online courses, among which are automated feedback, automated grading and automated exercises generation. We have found that the ExCAPE synthesis algorithmic ideas can be used for the development of tools for such tasks and have implemented them in the following tools:
- Providing meaningful feedbak for construction of deterministic finite automata (AtomataTutor)
- Auto grading introductory programming problems (AutoProf)
- Auto grading virtual laboratories in cyber-physical systems (CPSGrader)
- Problem Generation for Discrete Mathematics and Algorithms
- Teaching induction with functional programming and a proof assistant (InductFun)
Massively empowered classroom (MEC) is a blended learning platform by Microsoft Research that is aimed at providing high quality education to undergraduate students in India. The PI helped in the creation of this platform during his sabbatical and was the prime course coordinator for the primary course on this platform. The platform brings the usual MOOC elements of short video lectures, timed courses, quizzes, forums, etc. to students, but has the distinguishing feature of catering to the syllabus the student is enrolled in (by specializing to each individual university syllabus that is catered to). Also, the platform is open to individualization by local teachers in colleges, whereby teachers can upload their own videos, design their own quizzes (taking help from quiz banks created by other teachers), and can see the progress and performance of their students. The project also has a heavy grassroots effort in colleges in India, holding regular workshops for teachers, students, and administrators to introduce them to adopt the platform. There are also efforts to incentivize students (and colleges) to take the course using certificates at various levels, and a liaison with the industry to provide students who excel in these courses with job opportunities. The MEC framework is growing, catering to 5 universities (each having hundreds of colleges under it), and catered to about 18000 students in Spring 2014 through a single course on design and analysis of algorithms.
- The ROSETTE solver-aided host language has been released to open source after making it accessible to undergraduates and testing it in classroom on 13 synthesizers. The course materials for this course are publicly available.
- AutoProf provided to the teaching staff of Introduction to Programming course (6.00) at MIT.
- AutogProf was presented to the edX faculty teaching introduction to programming. An A/B test study on edX for evaluating its usefulness in this online course is planned.
- AutomataTutor has been made available for any academic institution (and any private individuals) to use at AutomataTutor.com.
- PI Alur organized a session titled Design of Cyber-Physical Systems: From Pacemakers to Driverless Cars and Beyond in Penn Engneering’s WICS Highschool Day for Girls. The goal of the event is to inspire highschools gilrs to pursue college education in computer science and engineering, and it attracted about 100 girls from Philadelphia highschools.
- PI Solar-Lezama has engaged two high-school students working on the problems of automatically generating Python programming problems using constraint-based synthesis as part of MIT PRIMES program.
- During Summer 2013, Penn undergraduate student Adam Freilich worked with PI Alur on the topic of regular functions. This work has led to a publication in LICS 2014 [AFR14].
- Linear Temporal Logic Mission Planner (LTLMoP) has been extended to work with Lego mindstorm. High school students experimented with the toolbox in the lab (summer 2012).
- PI Kress-Gazit ran the project component in the CURIE academy (summer 2012) – a week long summer camp about engineering for high school girls organized by Cornell University.
- Expanding Your Horizons (EYH) – Day of workshops for middle school girls – Workshop using the iRobot Create program using only the bump sensor – offered for the second time.
ExCAPE PIs are collaborating with industrial researchers, and have started discussions with other government organizations to find new avenues for applying the synthesis technology. Representative efforts are listed in the annual reports (1st year, 2nd year), and depicted here.
ExCAPE PIs are disseminating ExCAPE's view and the underlying synthesis approaches through courses, workshops, tutorials and invited talks. Details can be found in the annual reports (1st year, 2nd year).