The Science of Deep Specification


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.

Location 9:00-10:30 11:00-12:30 2:00-3:30 4:00-5:30 Evening
Thu, July 13 Heilmeier Hall Coq Intensive Coq Intensive Coq Intensive Coq Intensive
Fri, July 14 Heilmeier Hall Coq Intensive Coq Intensive Coq Intensive Coq Intensive
Sat, July 15 Heilmeier Hall Coq Intensive Coq Intensive Coq Intensive Coq Intensive
Sun, July 16Free day
Mon, July 17 Heilmeier Hall Pierce Leroy Homework Weirich
Tue, July 18 Heilmeier Hall Pierce Leroy Homework Zdancewic
Wed, July 19 Heilmeier Hall Leroy Zdancewic Homework Weirich
Thu, July 20 Heilmeier Hall Zdancewic Pierce Homework Leroy Student talks
Fri, July 21 The Study Hotel Zdancewic Weirich Pierce Homework/
CompCert Q&A
Sat, July 22 Barnes Foundation trip
Sun, July 23 Free day
Mon, July 24 Berger Auditorium Chlipala Shao Homework Appel
Tue, July 25 Berger Auditorium Kaashoek/Zeldovich Shao Homework AppelStudent talks
Wed, July 26 Berger Auditorium Kaashoek/Zeldovich Appel Homework Chlipala Picnic at Bartram's Garden
Thu, July 27 Berger Auditorium Kaashoek/Zeldovich Chlipala Homework Shao
Fri, July 28 Berger Auditorium Kaashoek/Zeldovich Shao Appel


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


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.


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




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.


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.


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.


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 RingerProof Patching
John WiegleyUsing computational reflection to speed up proofs
Yishuai LiTesting HTTP server with QuickChick
Robert RandFormally Verifying your Quantum Programs
Heiko BeckerA Verified Certificate Checker for Floating-Point Error Bounds
Marco VassenaMAC, A Mechanically Verified Information-Flow Control Library
Daniel SelsamDeep Specifications for Machine Learning Systems
Roberto BlancoAn approach to correctness through proof: Foundational Proof Certificates
Ken RoeScaling Coq based separation logic to more complex problems (Video)
Daniel SchoepeReconciling Database Access Control and Information-Flow Control
Thiago Mael de CastroCommuting Strategies for Product-Line Reliability Analysis
Jim McCarthyScoping a system modelling environment
Benoît ViguierToward the correctness of TweetNaCl Ed25519 with VST
Paul TorriniTranslating to C an OS proto-kernel written in Coq
Marianna RapoportExtending Dependent Object Types
Nick RiouxTaming Nontermination: Recovering Free Theorems with Linearity

Second session

Perry Metzger"Shotgun Parsing" and Security
Ryan DoengesVerifying distributed systems with Verdi
Thomas Sibut-PinoteFormally Verified Approximation of Definite Integrals
Adam PetzTrust- What it is and how to get it
Yatin ManerkarAutomated Verification of Memory Consistency Model Implementations
Piotr PolesiukLightweight approach for variable binding in Coq
Jannis LimpergPropaganda for the Dark Side
Saswat PadhiLoopInvGen
Christine RizkallahReducing the Cost of Efficient Secure Verified Software