CS294-25: Current Berkeley Research in Programming Systems

From CS294-Fa07

(Redirected from Main Page)
Jump to: navigation, search

Instructors: Ras Bodik, Koushik Sen, Sanjit Seshia, Dawn Song, and Kathy Yelick.
Time: Tu 9:30–11, Th 3:30–5
Place: 310 Soda

Contents

[edit] Course Description

Several trends can be distinguished in recent programming systems research: renaissance in program verification and testing fueled by novel decision procedures and hybrid analyses; new software tools driven by scalable analyses and software mining; autotuning and sketching synthesizers as answers to the complexity of multicore compilation; renewed interest in language design for parallel hardware; and a greater hunger to apply research results in real-world applications. Berkeley is at the forefront of these trends. In this course, we will discuss our recent projects, brainstorm to formulate a vision and come up with new ideas, and maybe also start some new projects.

[edit] Tentative list of topics

  • program synthesis with sketching, program analysis and tools for dynamically typed languages (Ras Bodik);
  • automated test generation and model checking using program analysis and constraint solving techniques (Koushik Sen);
  • satisfiability modulo theories (SMT) solvers, model checking, malware analysis and detection (Sanjit Seshia);
  • dynamic and static binary analysis for computer security applications including vulnerability analysis and malicious code defense (Dawn Song);
  • compiler optimizations, automatically tuning sparse matrix kernels (Kathy Yelick);
  • shape analysis (Mooly Sagiv, guest speaker);
  • synthesis of concurrent garbage collectors (Martin Vechev and Eran Yahav, guest speakers) .

[edit] Course format and grading

Students will pursue an independent research project, which can be carried out in groups of two students. The first part of the semester will consists of lectures given by the instructors and occasional visiting speakers; to prepare for lively class discussions, students will read papers and write mini-reviews before the lecture. Some topics may be accompanied with a short homework. In the middle part of the semester, students will present a paper related to their project. The semester will conclude with project presentations and demos. Course grading will be passed on classroom participation, the project, paper reviews, homeworks, and the paper presentation.

First year graduate students are encouraged to take this course if they are interested in pursuing research in the general area of programming systems. Students in other areas who may benefit from or contribute to programming technology (eg, security, systems, CAD, hardware verification) are welcome to take the course. The prerequisite is a senior-level compiler course.

[edit] Schedule

Date Lecturer Topic Reading Slides Homework Assigned Homework Due
Tue Aug 28 Bodik, Sen, Seshia, Song, Yelick Introduction to course; overview of topics overview Ras Kathy Dawn
Thu Aug 30 Seshia Satisfiability modulo theories two simple papers Lecture1
Tue Sep 4 Seshia Satisfiability modulo theories
Thu Sep 6 Seshia Malware analysis and detection paper
Tue Sep 11 Bodik Synthesis by Sketching paper slides Homework 1: PDF, wiki
Thu Sep 13 Bodik Synthesis by Sketching PowerPoint Slides
Tue Sep 18 Sagiv Shape Analysis see Ras for hardcopy reviews
Thu Sep 20 Yahav and Vechev Synthesis of Concurrent Algorithms paper
Tue Sep 25 Sen Concolic Testing paper1 paper2 slides Homework 2: CUTE
Thu Sep 27 Sen Concolic Testing (cont.)
Tue Oct 2 Song Binary Analysis for Malicious Code Analysis and Defense paper1 paper2
Thu Oct 4 Sen Dynamic Race Detection paper slides Homework3: CUTE (part 2)
Tue Oct 9 Yelick Automatic Tuning SparseMat Stencils
Thu Oct 11 Yelick Code Gen for Autotuning
Tue Oct 16 Mayur Naik Static Race Detection paper
Thu Oct 18 Yelick Analysis of Parallel Programs

Concurrency Analysis Hierarchical Pointer Analysis

Tue Oct 23 Song Binary Analysis for Vulnerability Signature Generation paper
Thu Oct 25 Song Binary Analysis for Other Security Applications paper
Tue Oct 30 Bodik Pointer Analysis paper
Thu Nov 1 students Project Proposal Presentations I sign up
Tue Nov 6 students Project Proposal Presentations II sign up
Thu Nov 8 students sign up
Tue Nov 13 Gautam Altekar, Raluca Sauciuc Catchcov: Symbolic execution and Run-time type inference, ESP: Path-Sensitive Program Verification in Polynomial Time paper paper
Thu Nov 15 Leo Meyerovich; Jacob Burnim Data Structure State Dynamic Analysis; Type-Dependence Analysis for Symbolic Execution paper paper
Tue Nov 20 Shaunak Chatterjee, Sudeep Juvekar 1) Mining Jungloids: Helping to Navigate the API Jungle, PLDI'05
2) PARSEWeb: A Programmer Assistant for Reusing Open Source Code on the Web 		Prospector parseWeb
" Chang-Seo Park, Christos Stergiou Making asynchronous parallelism safe for the world paper
Thu Nov 22 Thanksgiving break
Tue Nov 27 Lexin Shan, Sayak Ray Data Structure Testing, Dynamic Partial Order Reduction Korat, DPOR
Thu Nov 29 Shoaib Kamil, Mark Murphy Delta Debugging, SPIRAL's Search Algorithm DD Stochastic Search Mark's Slides
Tue Dec 4 Pallavi Joshi, Yamini Kannan Typestate verification, Automatic Incrementalization of Data Structure Invariant Checks typestate Ditto
Thu Dec 6 Chris Jones; Mike Case The SPIN model checker; Hybrid Abstraction SPIN Hybrid Abstraction
Fri Dec 14 During OSQ Lunch (12:00 - 1:30 PM) Poster presentations

[edit] Student Pages

Are you looking for a project partner? Write your project idea and qualifications here.

Submit your project proposals here.

[edit] Administrivia

Retrieved from "http://play.cs.berkeley.edu/wiki/cs294/fa07/index.php/CS294-25:_Current_Berkeley_Research_in_Programming_Systems"
Personal tools