OSQ

Past Meetings

Meetings Fall '07:

●Fri, Aug 31		First meeting of the semester Presentation on Trend Prof by Simon Goldsmith.
●Fri, Sep 7		Presentation by Chris Jones
●Fri, Sep 14		Presentation by Leo Meyerovich
●Fri, Sep 21		Presentation by Manu Sridharan
●Fri, Sep 28		Presentation by Armando Solar-Lezama
●Fri, Oct 5		Presentation by Jimmy Su
●Fri, Oct 12		Presentation by Evan Chang
●Fri, Oct 19		Presentation by Zach Anderson
●Fri, Oct 26		PLDI Day
●Fri, Nov 2		Presentation by Raluca Sauciuc
●Fri, Nov 9		Presentation by Pallavi Joshi
●Fri, Nov 16		Presentation by Christos Stergiou
●Fri, Nov 30		Presentation by Gilad Arnold
●Fri, Dec 7		Presentation by Apollo Ellis
●Fri, Dec 14		Poster session for CS294. in the 6th floor hallway.

Meetings Spring '07:

●Fri, Jan 19		First meeting of the semester.
●Fri, Jan 26		Presentation on program analysis for dynamic languages by Bill McCloskey
●Fri, Feb 2 Moved to 373 Soda		Presentation by Manu Sridharan Thin Slicing
●Fri, Feb 9		Group discussion
●Fri, Feb 16		Group discussion
●Fri, Feb 23		Presentation by Jeremy Condit Deputy: Dependent Types for Safe Systems Software
●Fri, March 2		Discussion lead by Matthew Tschantz Techniques for code reuse in object oriented systems (inheritance, composition, traits, and mixins)
●Fri, March 9		Presentation by Adam Chlipala A statically-typed language for unified UNIX system configuration
●Mon, March 12		Special OSQ lunch with prospective students with short talks by: Kathy Yelick Ras Bodik George Necula Koushik Sen Sanjit Seshia Jeremy Condit James Demmel Armando & Gilad Adam Chlipala Dave & Liviu Amir Kamil Manu Sridharan
●Fri, March 16		Presentation by Dan Wilkerson Progress Report on using Oink to Perform a Garbage Collection Safety Analysis of The FireFoxjava_script Engine, SpiderMonkey
●Fri, March 23		Presentation by Evan Chang
●Fri, March 30		No meeting (Spring Break)
●Fri, April 6		Presentation by Xavier Rival
●Fri, April 13		Presentation by Armando Solar-Lezama
●Fri, April 20		Presentation by Matt Harren
●Fri, April 27		Presentation by Gilad Arnold
●Fri, May 4		Presentation by AJ Shankar

Meetings Fall '06:

●Thurs, Aug 31 First meeting of the semester.

●Thurs, Sept 7 Adam Chlipala Modular Development of Certified Program Verifiers with a Proof Assistant. (ICFP '06)

●Thurs, Sept 14 Arindam Chakrabarti Software Partitioning for Effective Automated Unit Testing. (EMSOFT '06)

●Thurs, Sept 21 Zachary Anderson A concolic testing tool for C.

●Thurs, Sept 28 Matthew Tschantz Javari: Java with reference immutability.

●Thurs, Oct 5 Armando Solar-Lezama Sketching for Structured Grid Computations.

●Thurs, Oct 12 Daniel Kröning, ETH Zurich Model Checking C++ Programs that use the STL. [abstract]

●Thurs, Oct 19 AJ Shankar Transparent Incrementalization of Data Structure Invariants.

●Thurs, Oct 26 Emery Berger, UMass Exploiting Multiple Cores Now: Scalability and Reliability for Off-the-shelf Software. [abstract]

●Thurs, Nov 2 Feng Zhou SafeDrive - Safe and Recoverable Extensions Using Language-Based Techniques (OSDI '06).

●Thurs, Nov 9 Bill McCloskey Real-Time Garbage Collection for Java.

●Thurs, Nov 16 Liviu Tancau JavaSketch

●Thurs, Nov 23 No meeting (Thanksgiving).

●Thurs, Nov 30 Daniel Wilkerson,
Taras Glek,
Igor Bukanov,
Tim Riley, and
Brendan Eich (Mozilla) The Oink Open-Analysis Framework in Action at Mozilla

●Thurs, Dec 7 Marta Kwiatkowska,
University of Birmingham PRISM - Probabilistic Symbolic Model Checking. [abstract]

●Thurs, Dec 14 Jim Whitehead, UCSC Predicting Bugs by Analyzing Software History. [abstract]

Meetings Spring '06:

● Wed, Jan 18 Bill McCloskey Scripting languages and dynamic typing.

● Wed, Jan 25 Manu Sridharan Refinement-Based Context-Sensitive Points-To Analysis for Java.

● Wed, Feb 1 Yuanyuan Zhou, UIUC ARTS: Available, Robust and Trusted Software.

● Wed, Feb 8 Dan Wilkerson Elsa/Oink/Cqual++. (CodeCon '06)

● Wed, Feb 15 Greg Bronevetsky, Cornell. Application-level checkpointing for multi-threaded programs. [abstract]

● Wed, Feb 22 David Bacon, IBM Eventrons: A Safe Programming Construct for High-Frequency Hard Real-Time Applications.

● Wed, Mar 1

● Wed, Mar 8 Evan and Jeremy Model checking for heaps, and bounds checking for C.

● Thurs, Mar 16
   11:00 -12:30

   in 320 Soda

Tom Reps
WYSINWYX: What You See Is Not What You eXecute

● Wed, Mar 22

● Wed, Mar 29 (No meeting) Spring break

● Wed, Apr 5 Simon Goldsmith Trend Profiling: Empirical Computational Complexity

● Wed, Apr 12 David Monniaux The ASTRÉE Static Analyzer

● Wed, Apr 19 Adam Chlipala The Ultimate Web Programming Language.

● Wed, Apr 26

● Wed, May 3 Marat Boshernitsan Dissertation talk

● Wed - Fri,
     May 10 - 12
The Sixth Annual OSQ Retreat

Meetings Fall '05:

Wed, Aug 31. John Kodumal and Tachio Terauchi. SAS practice talks: A duet.
Wed, Sep 7. Adam Chlipala. Summer project at MSR.
Wed, Sep 14. Dave Mandelin. Comparing models (Summer project at IBM Watson.)
Wed, Sep 21. AJ Shankar. Runtime Specialization With Optimistic Heap Analysis (OOPSLA '05)
Wed, Sep 28. Rob O'Callahan, Novell. Engineering Firefox [abstract] [slides]
Wed, Oct 5. Manu Sridharan. Demand-Driven Points-to Analysis for Java (OOPSLA '05)
Wed, Oct 12. PLDI submission preview.
Wed, Oct 19. Armando Solar-Lezama.
Wed, Oct 26. Simon Goldsmith. Predicting the scalability of programs.
Wed, Nov 2. Adam Megacz. The Java Boolean Parser (JBP), a scannerless GLR parser.
Wed, Nov 9. Shuvendu Lahiri, Microsoft Research. Verifying Properties of Well-Founded Linked Lists (POPL '06) [abstract]
Wed, Nov 16.Adam Chlipala.
Wed, Nov 23. Python.
Wed, Nov 30. Bill McCloskey. Autolocker: Synchronization Inference for Atomic Sections. (POPL '06)
Wed, Dec 7. Adam Chlipala. A Framework for Certified Program Analysis and Its Applications to Mobile-Code Safety (VMCAI '06).
Wed, Dec 14. Gilad Arnold. Combining Shape Analyses by Intersecting Abstractions (VMCAI '06).

Meetings Spring '05:

Friday, Jan 28. Daniel Wilkerson: A Suite of Tools for Pragmatic Program Analysis of C and C++.
Friday, Feb 4 (CS 264 guest lecture). Job talk by Sumit Gulwani: Program Analysis using Random Interpretation.
Friday, Feb 4 (OSQ Lunch). Job talk by Wes Weimer: Language Support For Run-Time Error Handling Mistakes.
Friday, Feb 11. Scott McPeak: Data Structure Invariants.
Friday, Feb 18. Job talk by Andy Begel: Programming by voice.
Friday, Feb 25. AJ Shankar: On-line analysis for dynamic compilation.
Friday, Mar 4. Manu Sridharan: Points-to analysis in Java vs. C.
Friday, Mar 11. Jeremy Condit: Data Slicing (with flying boxes, of course).
Friday, Mar 18. Job talk by Marat Boshernitsan.
Friday, Apr 1. Adam Chlipala: A language for writing provably-correct program verifiers.
Friday, Apr 8. Armando Solar-Lezama: StreamBit: Optimization of Bit-Stream Programs through Sketching
Friday, Apr 15. Rupak Majumdar
Friday, Apr 22. David Mandelin
Friday, Apr 29. Arindam Chakrabarti: Web Services Interfaces.
Friday, May 6. Simon Goldsmith: Profiling for scalability.
Thursday - Friday, May 12-13. OSQ Retreat.

Meetings Fall '04:

Fri Dec 10. Adam Chlipala told us about the OpenVerifier.
Fri Nov 19. CS Job Search Fireside Chat: Ben Liblit, Rupak Majumdar, Ranjit Jhala.
Fri Nov 12. Evan Chang. Abstract interpretation with alien expressions and heap structures.
Fri Oct 29. Manu Sridharan spoke on post-mortem analysis of crash reports.
Fri Oct 15. Wes Weimer talked about specification mining techniques for bug-finding.
Fri Oct 08. Tom Ball: A Theory of Predicate-Complete Test Coverage and Generation [Abstract]
Fri Oct 01. There was chit-chat.
Fri Sep 24. Mooly Sagiv, Tel Aviv University: A Case Study in Automatic Assume-Guarantee Reasoning Proving Conformance to Collection Interface Requirement (Ongoing work).

Meetings Spring '04:

Sat May 22. Spring semester ends, last day of finals.
Thu May 13 - Fri May 13. OSQ Retreat.
Mon May 03. John Kodumal, PLDI Practice Talk.
Mon Apr 26. Sumit Gulwani -- global value numbering results and algorithm tutorials .
Mon Apr 12. Bill McCloskey: Macros -- analyzable language and translation tools for replacing the C preprocessor.
Mon Apr 05. Simon Goldsmit: Partiqle -- program trace query language, lightweight monitoring.
Mon Mar 29. Scott McPeak: Elkhound practice talk for CC04.
Mon Feb 23. Scott McPeak: Using Knuth-Bendix to complete axiom sets for data structure invariants.
Mon Feb 09. Armando Solar-Lezama: Sketching high-performance implementations of bitstream programs.
Mon Feb 02. Dirk Beyer: Simple and Efficient Relational Querying. You can also find out more about the CrocoPat project.
Mon Jan 26. First meeting. Scott McPeak spoke on handling padding and alignmnet in CCured.

Meetings Fall '03:

Monday, December 15, 4pm. Stephen Freund, Cormac Flanagan. "Atomizer: A Dynamic Atomicity Checker For Multithreaded Programs."
Tuesday, December 09. AJ Shankar spoke on Dynamic Specialization.
Tuesday, December 02. Ben Liblit spoke on Random Sampling.
Tuesday, Novemeber 25. Evan Chang spoke on applying PL techniques to Systems Biology.
Tuesday, Novemeber 18. George Necula spoke on the Open Verifier.
Tuesday, Novemeber 04. Rob Johnson: Scaling CQual to Millions of Lines of Code and Millions of Users.
Tuesday, October 28. Hao Chen: Experiences with Checking a Million Lines of Codes. You can find out more about the MOPS project here.
Tuesday, October 21. Evan Chang spoke on the internals of the Open Verifier. Adam Chlipala discussed the type system reasoning required to make a TAL extension for the Open Verifier, paying special attention to continuations.
Tuesday, October 14. Sumit Gulwani spoke on "Combining Abstract Interpreters".
Tuesday, October 7. Arindam gave a practice talk for Emsoft about "Resource Interfaces".
Tuesday, September 30. Scott McPeak spoke about helicopters.
Tuesday, September 23. Matt Harren spoke on the XJ project at IBM (related to providing language support for XML).
Monday, September 08. Jeremy Condit spoke on "Region-based model abstraction", work done at Microsoft Research.
Monday, September 15. Scott McPeak spoke on the importance of injective functions for dealing with strong updates in program verification.
Monday, September 15, 4pm in 540 Cory. Rupak Majumdar gave his Ph.D. talk on Quantitative Games in Verification.

Meetings Spring '03:

Tuesday, May 13th-15th. OSQ Retreat. The retreat will be two days long. A tentative schedule is available.
Monday, May 5. Jeremy Condit gave a practice PLDI talk on CCured.
Monday, April 14. John Kodumal.
Monday, April 7. Facult Candidate Talk by Chris Olston (entitled Approximate Replication).
Wednesday, April 9. Special Meeting. "Object Equality Profiling" by Darko Marinov, MIT.
Monday, February 10. Christoph Kirsch.
Monday, February 24. Marco Sanvido.
Monday, March 3. Krishnendu Chatterjee.
Monday, March 10. Scott McPeak on Elsa/Elkhound.
Monday, March 17. No meeting. Grad student visit day.
Monday, March 24. No meeting. Spring Recess.
Monday, March 31. No speaker.

Fall 2002 meetings:

Monday, December 9. Last meeting of the semester. There will be food. Westley Weimer gave a summary of the pros and cons of major OSQ projects.
Monday, December 2. Rupak Majumdar gave an informal presentation on ongoing work in race detection (read: parallel BLAST) with Ranjit Jhala and Shaz Qadeer. Daniel Weise was visiting.
Monday, Novemeber 25. Natarajan Shankar and associates from SRI gave a demo of the SALEnv model checking framework. Rob O'Callahan from IBM was present and encouraged students to look into IBM internships.
Monday, Novemeber 18. Sumit Gulwani gave a practice talk: Discovering Affine Equalities Using Random Interpretation.
Monday, Novemeber 11. No meeting: Veterans Day (University Holiday). Check out Hao Chen's paper entitled "MOPS: an Infrastructure for Examining Security Properties of Software". The full version is available.
Monday, November 4. Wes Weimer gave a presentation about the success of the OSQ project. A general discussion about the nature of its successor project ensued.
Monday, October 28. Manu Sridharan gave a demo of The Alloy Analyzer. David Schmidt from Kansas State University was visiting.
Monday, October 14. Sriram Rajamani spoke on the Behave! project at Microsoft Research.
Monday, October 7. Ben Liblit spoke on fair randomized program sampling.
Monday, September 30. Wes Weimer spoke on speeding up data-flow analysis using flow-insensitive pointer analysis (an SAS 2002 presentation).
Monday, September 23. Ranjit Jhala spoke about model-checking heap data structures.
Monday, September 16. Scott McPeak spoke about Elkhound, a system and algorithm for GLR parsing. His slides are available in PPT and in PS.
Monday, September 9. First meeting of the semester. General discussion.
Monday, September 2. No Meeting: Labor Day.

OSQ Project Retreats

The fifth annual OSQ retreat will be held in Santa Cruz on May 12-13, 2005. The bus will leave Soda Wednesday afternoon and return Friday afternoon. Details TBD. See you there!

Past retreats:

Page maintained by Armando Solar-Lezama..

●Thurs, Aug 31		First meeting of the semester.
●Thurs, Sept 7	Adam Chlipala	Modular Development of Certified Program Verifiers with a Proof Assistant. (ICFP '06)
●Thurs, Sept 14	Arindam Chakrabarti	Software Partitioning for Effective Automated Unit Testing. (EMSOFT '06)
●Thurs, Sept 21	Zachary Anderson	A concolic testing tool for C.
●Thurs, Sept 28	Matthew Tschantz	Javari: Java with reference immutability.
●Thurs, Oct 5	Armando Solar-Lezama	Sketching for Structured Grid Computations.
●Thurs, Oct 12	Daniel Kröning, ETH Zurich	Model Checking C++ Programs that use the STL. [abstract]
●Thurs, Oct 19	AJ Shankar	Transparent Incrementalization of Data Structure Invariants.
●Thurs, Oct 26	Emery Berger, UMass	Exploiting Multiple Cores Now: Scalability and Reliability for Off-the-shelf Software. [abstract]
●Thurs, Nov 2	Feng Zhou	SafeDrive - Safe and Recoverable Extensions Using Language-Based Techniques (OSDI '06).
●Thurs, Nov 9	Bill McCloskey	Real-Time Garbage Collection for Java.
●Thurs, Nov 16	Liviu Tancau	JavaSketch
●Thurs, Nov 23		No meeting (Thanksgiving).
●Thurs, Nov 30	Daniel Wilkerson, Taras Glek, Igor Bukanov, Tim Riley, and Brendan Eich (Mozilla)	The Oink Open-Analysis Framework in Action at Mozilla
●Thurs, Dec 7	Marta Kwiatkowska, University of Birmingham	PRISM - Probabilistic Symbolic Model Checking. [abstract]
●Thurs, Dec 14	Jim Whitehead, UCSC	Predicting Bugs by Analyzing Software History. [abstract]

● Wed, Jan 18	Bill McCloskey	Scripting languages and dynamic typing.
● Wed, Jan 25	Manu Sridharan	Refinement-Based Context-Sensitive Points-To Analysis for Java.
● Wed, Feb 1	Yuanyuan Zhou, UIUC	ARTS: Available, Robust and Trusted Software.
● Wed, Feb 8	Dan Wilkerson	Elsa/Oink/Cqual++. (CodeCon '06)
● Wed, Feb 15	Greg Bronevetsky, Cornell.	Application-level checkpointing for multi-threaded programs. [abstract]
● Wed, Feb 22	David Bacon, IBM	Eventrons: A Safe Programming Construct for High-Frequency Hard Real-Time Applications.
● Wed, Mar 1
● Wed, Mar 8	Evan and Jeremy	Model checking for heaps, and bounds checking for C.
● Thurs, Mar 16 11:00 -12:30 in 320 Soda	Tom Reps	WYSINWYX: What You See Is Not What You eXecute
● Wed, Mar 22
● Wed, Mar 29	(No meeting)	Spring break
● Wed, Apr 5	Simon Goldsmith	Trend Profiling: Empirical Computational Complexity
● Wed, Apr 12	David Monniaux	The ASTRÉE Static Analyzer
● Wed, Apr 19	Adam Chlipala	The Ultimate Web Programming Language.
● Wed, Apr 26
● Wed, May 3	Marat Boshernitsan	Dissertation talk
● Wed - Fri, May 10 - 12	The Sixth Annual OSQ Retreat