Schedule

During the Summer School, every day has four slots, one of which is marked as “free for homework”. During the Coq Intensive, there will be more and smaller homework sessions.

The schedule is tentative; you can expect it to no longer change by July 29th.

Locations

• Heilmeier Hall, Room 100, Towne Building, 220 S 33rd Street
• The Study Hotel, 20 S 33rd Steet
• Berger Auditorium, Skirkanich Hall, 210 S 33rd Steet

The engineering complex (buildings Moore, Levine, Skirkanich, Towne) is connected by interior hallways, so it is effectively one large building. But it can be a confusing labyrinthine, so arrive early.

Many entrances require a Penn ID to open. The Levine Hall entrance on Chancellor Walk (see the map) is usually open to the general public.

Additionally, rooms 211, 213, and 215 in the Towne Building have been reserved for students to spread out to work on homework assignments.

Barns Foundation trip

We are visiting the Barnes Foundation.

Our group has two entrance times: 10:00am and 11:00am. We need to arrange so that (roughly) 30-35 people arrive for each

Departure

• 9:30AM - first group departs from Towers Hall
• 10:30AM - second group departs from Towers Hall

Penn Students will lead these groups. The walk from Towers Hall to the Barnes is about 1.5 miles, and will take about half an hour. If you are staying elsewhere, please join one of the groups departing from Towers Hall (it's on the way)

Touring the museum

Our tickets include the audio tour guide. Visiting the collection takes 1.5-2 hours.

Lunch 12:30 - 2:00

The plan is to eat in the park at 2124 Wood St, which is just across the Benjamin Franklin Parkway from the Barnes. We will have a variety of hoagies and wraps, chips, snacks, and bottled water. Other food and drinks can be purchased at the Whole Foods located just behind the Barnes.

Map & Route

See this map for suggested routes.

Afterwards

You're free to continue the afternoon on your own. Some suggestions of things to do near the Barnes:

Museums

• The Rodin Museum
• The Philadelphia Museum of Art
• The Franklin Institute

Walks

• A stroll along the Schuylkill River toward Boathouse Row
• A walk to Reading Terminal Market via City Hall

Biking

• Philadelphia has a pay-per-use bike share service with kiosks located throughout the city. It costs $4 for half an hour, which is long enough to get you pretty much anywhere in Center City.

Rain Plans

The Barnes is inside, but we still plan to walk, so consider bringing an umbrella if it looks like rain.

For lunch we don't have great backup options (it's hard to find indoor seating for such a large group). We may try to distribute the lunch from within Whole Foods if that seems possible; otherwise, we just get wet.

Bartram’s Gardens trip

On Wednesday, we’ll be visiting Bartram’s garden. The park is free and open to the public, with many shaded paths and trails along the Schuylkill River.

Departure

At 6:00-6:30pm board buses at 3330 Walnut Street, near Levine Hall entrance Bartram's Garden is a short drive from Penn; we'll probably arrive before 7:00pm.

Dinner

BEFORE boarding the buses, pick up a boxed meal near the "CyberCafe" entrance to the engineering school. (We will have local participants directing you.)

Once you arrive at the gardens, there are picnic tables near the parking lot, benches available on the garden paths, and large open grassy areas where you can sit to eat.

Visiting the gardens

You're free to explore the gardens and surround area at your leisure.

Return:

The buses will return to Penn at 9:00PM. (Please be on time!)

Student talks

The student talk sessions were helpfully organized by Talia L. Ringer.

First session

Talia Ringer	Proof Patching
John Wiegley	Using computational reflection to speed up proofs
Yishuai Li	Testing HTTP server with QuickChick
Robert Rand	Formally Verifying your Quantum Programs
Heiko Becker	A Verified Certificate Checker for Floating-Point Error Bounds
Marco Vassena	MAC, A Mechanically Verified Information-Flow Control Library
Daniel Selsam	Deep Specifications for Machine Learning Systems
Roberto Blanco	An approach to correctness through proof: Foundational Proof Certificates
Ken Roe	Scaling Coq based separation logic to more complex problems (Video)
Daniel Schoepe	Reconciling Database Access Control and Information-Flow Control
Thiago Mael de Castro	Commuting Strategies for Product-Line Reliability Analysis
Jim McCarthy	Scoping a system modelling environment
Benoît Viguier	Toward the correctness of TweetNaCl Ed25519 with VST
Paul Torrini	Translating to C an OS proto-kernel written in Coq
Marianna Rapoport	Extending Dependent Object Types
Nick Rioux	Taming Nontermination: Recovering Free Theorems with Linearity

Second session

Perry Metzger	"Shotgun Parsing" and Security
Ryan Doenges	Verifying distributed systems with Verdi
Thomas Sibut-Pinote	Formally Verified Approximation of Definite Integrals
Adam Petz	Trust- What it is and how to get it
Yatin Manerkar	Automated Verification of Memory Consistency Model Implementations
Piotr Polesiuk	Lightweight approach for variable binding in Coq
Jannis Limperg	Propaganda for the Dark Side
Saswat Padhi	LoopInvGen
Christine Rizkallah	Reducing the Cost of Efficient Secure Verified Software

---