SOAP 2019
Sat 22 Jun 2019
Phoenix, Arizona, United States
co-located with
PLDI 2019
Toggle navigation
Attending
Venue: Phoenix Convention Center
Program
Complete Program
Your Program
Sat 22 Jun
Track/Call
Organization
SOAP 2019 Committees
Track Committees
Organizing Committee
Program Committee
Contributors
People Index
Search
Series
Series
SOAP 2024
SOAP 2023
SOAP 2022
SOAP 2021
SOAP 2020
SOAP 2019
SOAP 2018
SOAP 2017
SOAP 2016
SOAP 2015
Sign in
Sign up
PLDI 2019
(
series
) /
SOAP 2019 (
series
) /
Phoenix Convention Center
/
Room information: 106B
Venue
Phoenix Convention Center
Room name
106B
Floor
0
Room number
106B
Room Information
No extra information available
Program
Detailed Table
Session Timeline
Detailed Timeline
Program Display Configuration
Time Zone
The program is currently displayed in
(GMT-07:00) Tijuana, Baja California
.
Use conference time zone: (GMT-07:00) Tijuana, Baja California
Select other time zone
(GMT-12:00) AoE (Anywhere On Earth)
(GMT-11:00) Midway Island, Samoa
(GMT-09:00) Hawaii-Aleutian
(GMT-10:00) Hawaii
(GMT-09:30) Marquesas Islands
(GMT-09:00) Gambier Islands
(GMT-08:00) Alaska
(GMT-07:00) Tijuana, Baja California
(GMT-08:00) Pitcairn Islands
(GMT-07:00) Pacific Time (US & Canada)
(GMT-06:00) Mountain Time (US & Canada)
(GMT-06:00) Chihuahua, La Paz, Mazatlan
(GMT-07:00) Arizona
(GMT-06:00) Saskatchewan, Central America
(GMT-05:00) Guadalajara, Mexico City, Monterrey
(GMT-06:00) Easter Island
(GMT-05:00) Central Time (US & Canada)
(GMT-04:00) Eastern Time (US & Canada)
(GMT-04:00) Cuba
(GMT-05:00) Bogota, Lima, Quito, Rio Branco
(GMT-04:00) Caracas
(GMT-04:00) Santiago
(GMT-04:00) La Paz
(GMT-03:00) Faukland Islands
(GMT-04:00) Manaus, Amazonas, Brazil
(GMT-03:00) Atlantic Time (Goose Bay)
(GMT-03:00) Atlantic Time (Canada)
(GMT-02:30) Newfoundland
(GMT-03:00) UTC-3
(GMT-03:00) Montevideo
(GMT-02:00) Miquelon, St. Pierre
(GMT-02:00) Greenland
(GMT-03:00) Buenos Aires
(GMT-03:00) Brasilia, Distrito Federal, Brazil
(GMT-02:00) Mid-Atlantic
(GMT-01:00) Cape Verde Is.
(GMT) Azores
(UTC) Coordinated Universal Time
(GMT+01:00) Belfast
(GMT+01:00) Dublin
(GMT+01:00) Lisbon
(GMT+01:00) London
(GMT) Monrovia, Reykjavik
(GMT+02:00) Amsterdam, Berlin, Bern, Rome, Stockholm, Vienna
(GMT+02:00) Belgrade, Bratislava, Budapest, Ljubljana, Prague
(GMT+02:00) Brussels, Copenhagen, Madrid, Paris
(GMT+01:00) West Central Africa
(GMT+02:00) Windhoek
(GMT+03:00) Athens
(GMT+03:00) Beirut
(GMT+02:00) Cairo
(GMT+03:00) Gaza
(GMT+02:00) Harare, Pretoria
(GMT+03:00) Jerusalem
(GMT+03:00) Minsk
(GMT+03:00) Syria
(GMT+03:00) Moscow, St. Petersburg, Volgograd
(GMT+03:00) Nairobi
(GMT+04:30) Tehran
(GMT+04:00) Abu Dhabi, Muscat
(GMT+04:00) Yerevan
(GMT+04:30) Kabul
(GMT+05:00) Ekaterinburg
(GMT+05:00) Tashkent
(GMT+05:30) Chennai, Kolkata, Mumbai, New Delhi
(GMT+05:45) Kathmandu
(GMT+06:00) Astana, Dhaka
(GMT+07:00) Novosibirsk
(GMT+06:30) Yangon (Rangoon)
(GMT+07:00) Bangkok, Hanoi, Jakarta
(GMT+07:00) Krasnoyarsk
(GMT+08:00) Beijing, Chongqing, Hong Kong, Urumqi
(GMT+08:00) Irkutsk, Ulaan Bataar
(GMT+08:00) Perth
(GMT+08:45) Eucla
(GMT+09:00) Osaka, Sapporo, Tokyo
(GMT+09:00) Seoul
(GMT+09:00) Yakutsk
(GMT+09:30) Adelaide
(GMT+09:30) Darwin
(GMT+10:00) Brisbane
(GMT+10:00) Hobart
(GMT+10:00) Vladivostok
(GMT+10:30) Lord Howe Island
(GMT+11:00) Solomon Is., New Caledonia
(GMT+11:00) Magadan
(GMT+11:00) Norfolk Island
(GMT+12:00) Anadyr, Kamchatka
(GMT+12:00) Auckland, Wellington
(GMT+12:00) Fiji, Kamchatka, Marshall Is.
(GMT+12:45) Chatham Islands
(GMT+13:00) Nuku'alofa
(GMT+14:00) Kiritimati
The GMT offsets shown reflect the offsets
at the moment of the conference
.
Time Band
By setting a time band, the program will dim events that are outside this time window. This is useful for (virtual) conferences with a continuous program (with repeated sessions).
The time band will also limit the events that are included in the personal iCalendar subscription service.
Display full program
Specify a time band
-
Save
×
You're viewing the program in a time zone which is different from your device's time zone
change time zone
Sat 22 Jun
Displayed time zone:
Tijuana, Baja California
change
09:00 - 10:30
Deep Specifications
DeepSpec
at
106B
Chair(s):
Lennart Beringer
Princeton University
09:00
45m
Talk
Overview of the DeepSpec Expedition and its Capstone Application
DeepSpec
Benjamin C. Pierce
University of Pennsylvania
09:45
45m
Talk
Project Updates from Participating Sites
DeepSpec
Andrew W. Appel
Princeton
,
Adam Chlipala
Massachusetts Institute of Technology, USA
,
Zhong Shao
Yale University
10:30 - 11:00
Coffee Break
DeepSpec
at
106B
11:00 - 12:30
Compiler Verification
DeepSpec
at
106B
Chair(s):
Zhong Shao
Yale University
11:00
30m
Talk
Closure Conversion is Safe for Space
DeepSpec
Zoe Paraskevopoulou
Princeton University
,
Andrew W. Appel
Princeton
11:30
30m
Talk
Fast, Verified Partial Evaluation
DeepSpec
Adam Chlipala
Massachusetts Institute of Technology, USA
12:00
30m
Talk
Stack-Aware CompCert
DeepSpec
Yuting Wang
Yale University
14:00 - 15:30
Modular Reasoning
DeepSpec
at
106B
Chair(s):
Benjamin C. Pierce
University of Pennsylvania
14:00
30m
Talk
Abstraction, Subsumption, and Linking in VST
DeepSpec
Lennart Beringer
Princeton University
,
Andrew W. Appel
Princeton
14:30
30m
Talk
Compositional Verification of Preemptive OS Kernels with Temporal and Spatial Isolation
DeepSpec
Mengqi Liu
Yale University
15:00
30m
Talk
Modular Correctness Proofs at the Hardware-Software Interface
DeepSpec
Joonwon Choi
Massachusetts Institute of Technology, USA
16:00 - 17:30
Interaction Trees and Algebraic Effects I
DeepSpec
at
106B
Chair(s):
Andrew W. Appel
Princeton
16:00
20m
Talk
Interaction Trees: Representing Recursive and Impure Programs in Coq
DeepSpec
Steve Zdancewic
University of Pennsylvania
16:20
25m
Talk
Connecting Separation Logic with First-Order Reasoning on Memory
DeepSpec
William Mansky
University of Illinois at Chicago
,
Wolf Honore
16:45
45m
Talk
Typed Programming with Algebraic Effects (in terms of ambient values, functions, and control)
DeepSpec
Daan Leijen
Microsoft Research, USA
Sun 23 Jun
Displayed time zone:
Tijuana, Baja California
change
09:00 - 10:30
Interaction Trees and Algebraic Effects II
DeepSpec
at
106B
Chair(s):
Steve Zdancewic
University of Pennsylvania
09:00
45m
Talk
Implementation and Verification of Modular Effectful Systems in Coq using FreeSpec
DeepSpec
Yann Régis-Gianas
IRIF, University Paris Diderot and CNRS, France / INRIA PI.R2
09:45
45m
Talk
Names, Places, and Things: Generic Traversals over Generic Syntax with Binding
DeepSpec
James McKinna
University of Edinburgh
10:30 - 11:00
Coffee Break
DeepSpec
at
106B
11:00 - 12:30
HW/SW Interface Specifications
DeepSpec
at
106B
Chair(s):
Adam Chlipala
Massachusetts Institute of Technology, USA
11:00
45m
Talk
Development of the RISC-V ISA Formal Specification
DeepSpec
Rishiyur Nikhil
11:45
45m
Talk
Automated Formal Memory Consistency Verification of Hardware
DeepSpec
Yatin Manerkar
Princeton University
14:00 - 15:15
Verifying All the Things
DeepSpec
at
106B
Chair(s):
Zhong Shao
Yale University
14:00
45m
Talk
Project Oak: Control Data in Distributed Systems, Verify All The Things
DeepSpec
Ben Laurie
Google Research
14:45
30m
Talk
Refinement-Based Game Semantics for CompCert
DeepSpec
Jérémie Koenig
Yale University
15:15 - 15:45
Coffee Break
DeepSpec
at
106B
15:45 - 16:45
Coinduction and Testing
DeepSpec
at
106B
Chair(s):
Lennart Beringer
Princeton University
15:45
30m
Talk
Coinductive Reasoning about Interaction Trees
DeepSpec
Chung-Kil Hur
Seoul National University
16:15
30m
Talk
Coverage Guided, Property Based Testing
DeepSpec
Leonidas Lampropoulos
University of Pennsylvania
Sat 22 Jun
Displayed time zone:
Tijuana, Baja California
change
Room
9:00
30
10:00
30
11:00
30
12:00
30
13:00
30
14:00
30
15:00
30
16:00
30
17:00
30
106B
DeepSpec
Deep Specifications
DeepSpec
Coffee Break
DeepSpec
Compiler Verification
DeepSpec
Modular Reasoning
DeepSpec
DeepSpec
Interaction Trees and Algebraic Effects I
Sun 23 Jun
Displayed time zone:
Tijuana, Baja California
change
Room
9:00
30
10:00
30
11:00
30
12:00
30
13:00
30
14:00
30
15:00
30
16:00
30
106B
DeepSpec
Interaction Trees and Algebraic Effects II
DeepSpec
Coffee Break
DeepSpec
HW/SW Interface Specifications
DeepSpec
DeepSpec
Verifying All the Things
DeepSpec
Coffee Break
DeepSpec
Coinduction and Testing
Sat 22 Jun
Displayed time zone:
Tijuana, Baja California
change
Room
9:00
15
30
45
10:00
15
30
45
11:00
15
30
45
12:00
15
30
45
13:00
15
30
45
14:00
15
30
45
15:00
15
30
45
16:00
15
30
45
17:00
15
30
45
106B
DeepSpec
Overview of the DeepSpec Expedition and its Capstone Application
09:00 - 09:45
DeepSpec
Project Updates from Participating Sites
09:45 - 10:30
DeepSpec
Closure Conversion is Safe for Space
11:00 - 11:30
DeepSpec
Fast, Verified Partial Evaluation
11:30 - 12:00
DeepSpec
Stack-Aware CompCert
12:00 - 12:30
DeepSpec
Abstraction, Subsumption, and Linking in VST
14:00 - 14:30
DeepSpec
Compositional Verification of Preemptive OS Kernels with Temporal and S ...
14:30 - 15:00
DeepSpec
Modular Correctness Proofs at the Hardware-Software Interface
15:00 - 15:30
DeepSpec
Interaction Trees: Representing Recursive and Impure Programs in Coq
16:00 - 16:20
DeepSpec
Connecting Separation Logic with First-Order Reasoning on Memory
16:20 - 16:45
DeepSpec
Typed Programming with Algebraic Effects (in terms of ambient values, f ...
16:45 - 17:30
Sun 23 Jun
Displayed time zone:
Tijuana, Baja California
change
Room
9:00
15
30
45
10:00
15
30
45
11:00
15
30
45
12:00
15
30
45
13:00
15
30
45
14:00
15
30
45
15:00
15
30
45
16:00
15
30
45
106B
DeepSpec
Implementation and Verification of Modular Effectful Systems in Coq usi ...
09:00 - 09:45
DeepSpec
Names, Places, and Things: Generic Traversals over Generic Syntax with ...
09:45 - 10:30
DeepSpec
Development of the RISC-V ISA Formal Specification
11:00 - 11:45
DeepSpec
Automated Formal Memory Consistency Verification of Hardware
11:45 - 12:30
DeepSpec
Project Oak: Control Data in Distributed Systems, Verify All The Things
14:00 - 14:45
DeepSpec
Refinement-Based Game Semantics for CompCert
14:45 - 15:15
DeepSpec
Coinductive Reasoning about Interaction Trees
15:45 - 16:15
DeepSpec
Coverage Guided, Property Based Testing
16:15 - 16:45
x
Fri 19 Apr 22:24