VenueHilton Philadelphia at Penn's Landing
Room nameColumbus Ballroom B
Floor0
Additional informationThere is no additional information of this room available.
Program

You're viewing the program in a time zone which is different from your device's time zone - change time zone

Mon 18 Jun
Times are displayed in time zone: Eastern Time (US & Canada) change

09:00 - 10:30: Deep SpecificationsDeepSpec at Columbus Ballroom B
09:00 - 10:00
Talk
The Science of Deep Specification
DeepSpec
Andrew AppelPrinceton
10:00 - 10:30
Talk
CakeML: from functions to machine code with proof all the way
DeepSpec
Magnus O. MyreenChalmers University of Technology, Sweden
11:00 - 12:15: LLVMDeepSpec at Columbus Ballroom B
11:00 - 11:30
Talk
Vellvm - Modular Semantics via Interaction Trees
DeepSpec
Steve ZdancewicUniversity of Pennsylvania
11:30 - 12:00
Talk
Crellvm
DeepSpec
Chung-Kil HurSeoul National University
14:00 - 15:40: From Testing to VerificationDeepSpec at Columbus Ballroom B
14:00 - 14:30
Talk
Verifiable C, a logic and system for proving C programs correct
DeepSpec
14:30 - 15:00
Talk
Progress Report on the DeepSpec Web Server
DeepSpec
Benjamin C. PierceUniversity of Pennsylvania
15:00 - 15:30
Talk
QuickChick: Random Testing in Coq
DeepSpec
Leonidas LampropoulosUniversity of Pennsylvania

Tue 19 Jun
Times are displayed in time zone: Eastern Time (US & Canada) change

11:00 - 12:15: Haskell Core and Debugging DebuggersDeepSpec at Columbus Ballroom B
11:00 - 11:30
Talk
Towards a formal semantics for GHC Core
DeepSpec
Stephanie WeirichUniversity of Pennsylvania, USA
11:30 - 12:00
Talk
Debugging Debug Information and Beyond
DeepSpec
14:00 - 15:40: Concurrency and Concurrent Operating SystemsDeepSpec at Columbus Ballroom B
14:00 - 14:30
Talk
Multicore and Multithreaded Linking for Concurrent CertiKOS
DeepSpec
Jieung KimYale University, USA
14:30 - 15:00
Talk
Verifying seL4 towards Concurrency
DeepSpec
Thomas SewellUNSW, Australia
15:00 - 15:30
Talk
Specifying and Verifying Concurrent Programs with Ghost State
DeepSpec
William ManskyPrinceton University
16:10 - 17:35: Lightning TalksDeepSpec at Columbus Ballroom B
16:10 - 16:15
Talk
5-minute Lightning Talks
DeepSpec
16:15 - 16:20
Talk
Simplicity for Smart Contracts
DeepSpec
16:20 - 16:25
Talk
Machine-Verified Machine Learning
DeepSpec
Gordon StewartOhio University
16:25 - 16:30
Talk
Verification of Union-Find in C
DeepSpec
16:30 - 16:35
Talk
Narcissus: Deriving Correct-By-Construction Decoders and Encoders from Binary Formats
DeepSpec
16:35 - 16:40
Talk
LLVM's IR and Call-By-Push-Value Lambda Calculus
DeepSpec
16:40 - 16:45
Talk
A Formal Equational Theory for Call-By-Push-Value
DeepSpec
Christine RizkallahUniversity of New South Wales
16:45 - 16:50
Talk
Serializability for Distributed Protocols
DeepSpec
Joonwon ChoiMassachusetts Institute of Technology, USA
16:50 - 16:55
Talk
A Quick Hack to ask any SMT Solver if my Coq Goal is True
DeepSpec
Sam GruetterMassachusetts Institute of Technology

Mon 18 Jun
Times are displayed in time zone: Eastern Time (US & Canada) change

Tue 19 Jun
Times are displayed in time zone: Eastern Time (US & Canada) change