6.885 Class Home

6.885 Introduction to Principles and Practice of Software Synthesis

Spring 2015

home page image

Instructors: Xiaokang Qiu, Armando Solar Lezama

Lecture: MW1-2.30 (34-304)

Information:

The goal of this course is to provide a comprehensive introduction to the field of Software synthesis, an emerging field that sits at the intersection of programming systems, formal methods and artificial intelligence. Overall, the course will cover classical work on automata-based synthesis of reactive systems, as well as recent advances in the use of SAT/SMT solvers to synthesize programs. It will also cover the use of heuristic search techniques to explore large spaces of candidate programs. The course will also discuss different approaches to address the specification problem, ranging from logic-based specification mechanisms to programming by demonstration. The course will be graded on the basis of three homework assignments and an open ended final project.

Announcements

Course evaluations due tomorrow morning

If you haven't done so already, don't forget to fill out the official course evaluation.

http://web.mit.edu/subjectevaluation

The deadline is tomorrow at 9am. These are very important, especially given that it is the first time we teach this course.

Thanks!
Armando.

Announced on 17 May 2015 12:53 p.m. by Armando Solar Lezama

Project Presentations

Dear All,

We will have project presentations next week. Please be prepared for 10-minute short presentation of your project and 5-minute Q&A. I have created a Google doc for you to sign up:

https://docs.google.com/spreadsheets/d/1VGoc5RlnGPGtgnbafJH9dz6KNwT9NE9BPUfAaW8BMKQ/edit?usp=sharing

There will be 5 slots in each lecture; please sign up as soon as possible. Thanks!

Announced on 07 May 2015 9:04 p.m. by Xiaokang Qiu

Hint for problem 2 (spoiler alert)

Here is a hint if you are having trouble with part 2:
The set of safe states right before the adversary's turn has the form:

return (copier[0] > ?? && copier[1]>??) || (copier[0] > ?? && copier[1]>??);

It's a little simpler if you look at the set of safe states before your turn.

Announced on 01 May 2015 2:23 p.m. by Armando Solar Lezama

Office hours at 1pm as usual

We'll have the usual office hours today at 1pm. See you then!

Armando.

Announced on 01 May 2015 12:01 p.m. by Armando Solar Lezama

Office hour in 32-G840

Happening now!

Announced on 24 April 2015 1:01 p.m. by Xiaokang Qiu

View archived announcements