Write a Blog >>
CoqPL 2020
Sat 25 Jan 2020
New Orleans, Louisiana, United States
co-located with
POPL 2020
Toggle navigation
Attending
Venue: JW Marriott New Orleans
Restaurant: Palace Cafe
Program
Complete Program
Your Program
Sat 25 Jan
Track/Call
Organization
CoqPL 2020 Committees
Track Committees
Invited speakers
Organizing Committee
Program Committee
Contributors
People Index
Search
Series
Series
CoqPL 2024
CoqPL 2023
CoqPL 2022
CoqPL 2021
CoqPL 2020
CoqPL 2019
CoqPL 2018
CoqPL 2017
CoqPL 2016
Sign in
Sign up
POPL 2020
(
series
) /
CoqPL 2020 (
series
) /
JW Marriott New Orleans
/
Room information: St Jerome
Venue
JW Marriott New Orleans
Room name
St Jerome
Floor
3
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-06:00) Saskatchewan, Central America
.
Use conference time zone: (GMT-06:00) Saskatchewan, Central America
Select other time zone
(GMT-12:00) AoE (Anywhere On Earth)
(GMT-11:00) Midway Island, Samoa
(GMT-10:00) Hawaii-Aleutian
(GMT-10:00) Hawaii
(GMT-09:30) Marquesas Islands
(GMT-09:00) Gambier Islands
(GMT-09:00) Alaska
(GMT-08:00) Tijuana, Baja California
(GMT-08:00) Pitcairn Islands
(GMT-08:00) Pacific Time (US & Canada)
(GMT-07:00) Mountain Time (US & Canada)
(GMT-07:00) Chihuahua, La Paz, Mazatlan
(GMT-07:00) Arizona
(GMT-06:00) Saskatchewan, Central America
(GMT-05:00) Guadalajara, Mexico City, Monterrey
(GMT-05:00) Easter Island
(GMT-06:00) Central Time (US & Canada)
(GMT-05:00) Eastern Time (US & Canada)
(GMT-05:00) Cuba
(GMT-05:00) Bogota, Lima, Quito, Rio Branco
(GMT-04:00) Caracas
(GMT-03:00) Santiago
(GMT-04:00) La Paz
(GMT-03:00) Faukland Islands
(GMT-04:00) Manaus, Amazonas, Brazil
(GMT-04:00) Atlantic Time (Goose Bay)
(GMT-04:00) Atlantic Time (Canada)
(GMT-03:30) Newfoundland
(GMT-03:00) UTC-3
(GMT-03:00) Montevideo
(GMT-03:00) Miquelon, St. Pierre
(GMT-03: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-01:00) Azores
(UTC) Coordinated Universal Time
(GMT) Belfast
(GMT) Dublin
(GMT) Lisbon
(GMT) London
(GMT) Monrovia, Reykjavik
(GMT+01:00) Amsterdam, Berlin, Bern, Rome, Stockholm, Vienna
(GMT+01:00) Belgrade, Bratislava, Budapest, Ljubljana, Prague
(GMT+01:00) Brussels, Copenhagen, Madrid, Paris
(GMT+01:00) West Central Africa
(GMT+02:00) Windhoek
(GMT+02:00) Athens
(GMT+02:00) Beirut
(GMT+02:00) Cairo
(GMT+02:00) Gaza
(GMT+02:00) Harare, Pretoria
(GMT+02:00) Jerusalem
(GMT+03:00) Minsk
(GMT+02:00) Syria
(GMT+03:00) Moscow, St. Petersburg, Volgograd
(GMT+03:00) Nairobi
(GMT+03: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+10:30) Adelaide
(GMT+09:30) Darwin
(GMT+10:00) Brisbane
(GMT+11:00) Hobart
(GMT+10:00) Vladivostok
(GMT+11:00) Lord Howe Island
(GMT+11:00) Solomon Is., New Caledonia
(GMT+11:00) Magadan
(GMT+12:00) Norfolk Island
(GMT+12:00) Anadyr, Kamchatka
(GMT+13:00) Auckland, Wellington
(GMT+12:00) Fiji, Kamchatka, Marshall Is.
(GMT+13: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
Sun 19 Jan
Displayed time zone:
Saskatchewan, Central America
change
09:00 - 10:00
Invited 1
VMCAI
at
St Jerome
Chair(s):
Dirk Beyer
LMU Munich
09:00
60m
Talk
The Siren Song of Temporal Synthesis
VMCAI
Moshe Vardi
Rice University
10:30 - 12:30
Papers 1
VMCAI
at
St Jerome
Chair(s):
Natasha Sharygina
USI Lugano, Switzerland
10:30
30m
Talk
Witnessing Secure Compilation
VMCAI
Kedar Namjoshi
Bell Labs, Nokia
,
Lucas M. Tabajara
Rice University
11:00
30m
Talk
BackFlow: Backward Context-sensitive Flow Reconstruction of Taint Analysis Results
VMCAI
Pietro Ferrara
Università Ca' Foscari, Venezia, Italy
,
Luca Olivieri
JuliaSoft SRL
,
Fausto Spoto
U. Verona
11:30
30m
Coffee break
Mini Break
VMCAI
12:00
30m
Talk
Fixing Code That Explodes Under Symbolic Evaluation
VMCAI
Sorawee Porncharoenwase
University of Washington
,
James Bornholt
University of Texas at Austin
,
Emina Torlak
University of Washington
14:00 - 15:05
Invited 2
VMCAI
at
St Jerome
Chair(s):
Damien Zufferey
MPI-SWS
14:00
65m
Talk
Safety and Robustness for Deep Learning with Provable Guarantees
VMCAI
Marta Kwiatkowska
University of Oxford
15:35 - 17:45
Papers 2
VMCAI
at
St Jerome
Chair(s):
Kedar Namjoshi
Bell Labs, Nokia
15:35
32m
Talk
The Correctness of a Code Generator for a Functional Language
VMCAI
Nathanaël Courant
INRIA
,
Antoine Sere
Ecole Polytechnique
,
Natarajan Shankar
SRI International, USA
16:07
32m
Talk
Leveraging Compiler Intermediate Representation for Multi- and Cross-Language Verification
VMCAI
Jack Garzella
University of Utah
,
Marek S. Baranowski
University of Utah
,
Shaobo He
University of Utah
,
Zvonimir Rakamaric
University of Utah
16:40
32m
Coffee break
Mini Break
VMCAI
17:12
32m
Talk
Putting the Squeeze on Array Programs: Loop Verification via Inductive Rank Reduction
VMCAI
Oren Ish-Shalom
Tel Aviv University, Israel
,
Shachar Itzhaky
Technion, Israel
,
Noam Rinetzky
Tel Aviv University
,
Sharon Shoham
Tel Aviv university
Mon 20 Jan
Displayed time zone:
Saskatchewan, Central America
change
09:00 - 10:00
Invited 3
VMCAI
at
St Jerome
Chair(s):
Damien Zufferey
MPI-SWS
09:00
60m
Talk
Model Checking for Safe Autonomy
VMCAI
Rajeev Alur
University of Pennsylvania
10:30 - 12:30
Papers 3
VMCAI
at
St Jerome
Chair(s):
Dirk Beyer
LMU Munich
10:30
30m
Research paper
A Systematic Approach to Abstract Interpretation of Program Transformations
VMCAI
Sven Keidel
JGU Mainz
,
Sebastian Erdweg
JGU Mainz
Pre-print
11:00
30m
Talk
Sharing Ghost Variables in a Collection of Abstract Domains
VMCAI
Marc Chevalier
ENS, CNRS, PSL University, INRIA
,
Jerome Feret
INRIA Paris
11:30
30m
Coffee break
Mini Break
VMCAI
12:00
30m
Talk
Harnessing Static Analysis to Help Learn Pseudo-Inverses of String Manipulating Procedures for Automatic Test Generation
VMCAI
Oren Ish-Shalom
Tel Aviv University, Israel
,
Shachar Itzhaky
Technion, Israel
,
Roman Manevich
Mellanox Technologies
,
Noam Rinetzky
Tel Aviv University
14:00 - 15:05
Papers 4
VMCAI
at
St Jerome
Chair(s):
Ruzica Piskac
Yale University, USA
14:00
32m
Talk
Synthesizing Environment Invariants for Modular Hardware Verification
VMCAI
Hongce Zhang
Princeton University
,
Weikun Yang
Princeton University
,
Grigory Fedyukovich
Florida State University
,
Aarti Gupta
Princeton University
,
Sharad Malik
Princeton University
14:32
32m
Talk
Systematic Classification of Attackers via Bounded Model Checking
VMCAI
Eric Rothstein-Morris
Singapore University of Technology and Design
,
Jun Sun
Singapore Management University, Singapore
,
Sudipta Chattopadhyay
Singapore University of Technology and Design
15:35 - 17:45
Papers 5
VMCAI
at
St Jerome
Chair(s):
Nikolaj Bjørner
Microsoft Research
15:35
32m
Talk
Cheap CTL Compassion in NuSMV
VMCAI
Daniel Hausmann
Friedrich-Alexander-Universität Erlangen-Nürnberg
,
Tadeusz Litak
FAU Erlangen-Nuremberg, INF 8
,
Christoph Rauch
FAU Erlangen-Nürnberg, Lehrstuhl 8
,
Matthias Zinner
FAU Erlangen-Nürnberg
16:07
32m
Talk
A Cooperative Parallelization Approach for Property-Directed k-Induction
VMCAI
Martin Blicha
Università della Svizzera italiana
,
Antti Hyvärinen
Università della Svizzera Italiana
,
Matteo Marescotti
Università della Svizzera Italiana
,
Natasha Sharygina
USI Lugano, Switzerland
16:40
32m
Coffee break
Mini Break
VMCAI
17:12
32m
Talk
Generalized Property-Directed Reachability for Hybrid Systems
VMCAI
Kohei Suenaga
Graduate School of Informatics, Kyoto University
,
Takuya Ishizawa
Kyoto University
Link to publication
Pre-print
Tue 21 Jan
Displayed time zone:
Saskatchewan, Central America
change
09:00 - 10:00
Papers 6
VMCAI
at
St Jerome
Chair(s):
Andreas Podelski
University of Freiburg, Germany
09:00
30m
Talk
How to Win First-Order Safety Games
VMCAI
Helmut Seidl
Technische Universität München
,
Christian Müller
Technical University of Munich
,
Bernd Finkbeiner
Saarland University
09:30
30m
Talk
Improving Parity Game Solvers with Justifications
VMCAI
Ruben Lapauw
Katholieke Universiteit Leuven
,
Maurice Bruynooghe
Katholieke Universiteit Leuven
,
Marc Denecker
Katholieke Universiteit Leuven
10:30 - 12:30
Papers 7
VMCAI
at
St Jerome
Chair(s):
Thomas Wies
New York University
10:30
30m
Talk
Language Inclusion for Finite Prime Event Structures
VMCAI
Andreas Fellner
AIT - Austrian Institute of Technology
,
Thorsten Tarrach
Austrian Institute of Technology
,
Georg Weissenbacher
Technische Universität Wien
11:00
30m
Talk
Promptness and Bounded Fairness in Concurrent and Parameterized Systems
VMCAI
Swen Jacobs
CISPA Helmholtz Center for Information Security
,
Mouhammad Sakr
Saarland University
,
Martin Zimmermann
University of Liverpool
11:30
30m
Coffee break
Mini Break
VMCAI
12:00
30m
Talk
Solving LIA* Using Approximations
VMCAI
Maxwell Levatich
Yale
,
Nikolaj Bjørner
Microsoft Research
,
Ruzica Piskac
Yale University, USA
,
Sharon Shoham
Tel Aviv university
14:00 - 15:05
Papers 8
VMCAI
at
St Jerome
Chair(s):
Ori Lahav
Tel Aviv University
14:00
32m
Talk
Formalizing and Checking Multilevel Consistency
VMCAI
Ahmed Bouajjani
IRIF, Université Paris Diderot
,
Constantin Enea
IRIF, University Paris Diderot & CNRS
,
Madhavan Mukund
Chennai Mathematical Institute
,
Gautham Shenoy R
Chennai Mathematical Institute
,
S.P. Suresh
Chennai Mathematical Institute
14:32
32m
Talk
Practical Abstractions for Automated Verification of Shared-Memory Concurrency
VMCAI
Wytse Oortwijn
ETH Zürich
,
Dilian Gurov
KTH Royal Institute of Technology
,
Marieke Huisman
University of Twente
15:35 - 17:45
Panel Session
VMCAI
at
St Jerome
Chair(s):
Dirk Beyer
LMU Munich
15:35
2h10m
Other
Panel "The Future of Software Verification" at VMCAI
VMCAI
Lenore Zuck
UIC
,
Michael Whalen
Amazon Web Services and the University of Minnesota
,
Natarajan Shankar
SRI International, USA
,
Andreas Podelski
University of Freiburg, Germany
,
Dirk Beyer
LMU Munich
Thu 23 Jan
Displayed time zone:
Saskatchewan, Central America
change
14:00 - 15:30
SRC Finalists Presentations
POPL Student Research Competition
at
St Jerome
14:00
90m
Talk
SRC Finalists Presentations
POPL Student Research Competition
Sun 19 Jan
Displayed time zone:
Saskatchewan, Central America
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
St Jerome
VMCAI
Invited 1
VMCAI
Papers 1
VMCAI
Invited 2
VMCAI
Papers 2
Mon 20 Jan
Displayed time zone:
Saskatchewan, Central America
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
St Jerome
VMCAI
Invited 3
VMCAI
Papers 3
VMCAI
Papers 4
VMCAI
Papers 5
Tue 21 Jan
Displayed time zone:
Saskatchewan, Central America
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
St Jerome
VMCAI
Papers 6
VMCAI
Papers 7
VMCAI
Papers 8
VMCAI
Panel Session
Thu 23 Jan
Displayed time zone:
Saskatchewan, Central America
change
Room
14:00
30
15:00
30
St Jerome
POPL Student Research Competition
SRC Finalists Presentations
Sun 19 Jan
Displayed time zone:
Saskatchewan, Central America
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
St Jerome
VMCAI
The Siren Song of Temporal Synthesis
09:00 - 10:00
VMCAI
Witnessing Secure Compilation
10:30 - 11:00
VMCAI
BackFlow: Backward Context-sensitive Flow Reconstruction of Taint Analy ...
11:00 - 11:30
VMCAI
Mini Break
11:30 - 12:00
VMCAI
Fixing Code That Explodes Under Symbolic Evaluation
12:00 - 12:30
VMCAI
Safety and Robustness for Deep Learning with Provable Guarantees
14:00 - 15:05
VMCAI
The Correctness of a Code Generator for a Functional Language
15:35 - 16:07
VMCAI
Leveraging Compiler Intermediate Representation for Multi- and Cross-La ...
16:07 - 16:40
VMCAI
Mini Break
16:40 - 17:12
VMCAI
Putting the Squeeze on Array Programs: Loop Verification via Inductive ...
17:12 - 17:45
Mon 20 Jan
Displayed time zone:
Saskatchewan, Central America
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
St Jerome
VMCAI
Model Checking for Safe Autonomy
09:00 - 10:00
VMCAI
A Systematic Approach to Abstract Interpretation of Program Transformations
10:30 - 11:00
VMCAI
Sharing Ghost Variables in a Collection of Abstract Domains
11:00 - 11:30
VMCAI
Mini Break
11:30 - 12:00
VMCAI
Harnessing Static Analysis to Help Learn Pseudo-Inverses of String Mani ...
12:00 - 12:30
VMCAI
Synthesizing Environment Invariants for Modular Hardware Verification
14:00 - 14:32
VMCAI
Systematic Classification of Attackers via Bounded Model Checking
14:32 - 15:05
VMCAI
Cheap CTL Compassion in NuSMV
15:35 - 16:07
VMCAI
A Cooperative Parallelization Approach for Property-Directed k-Induction
16:07 - 16:40
VMCAI
Mini Break
16:40 - 17:12
VMCAI
Generalized Property-Directed Reachability for Hybrid Systems
17:12 - 17:45
Tue 21 Jan
Displayed time zone:
Saskatchewan, Central America
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
St Jerome
VMCAI
How to Win First-Order Safety Games
09:00 - 09:30
VMCAI
Improving Parity Game Solvers with Justifications
09:30 - 10:00
VMCAI
Language Inclusion for Finite Prime Event Structures
10:30 - 11:00
VMCAI
Promptness and Bounded Fairness in Concurrent and Parameterized Systems
11:00 - 11:30
VMCAI
Mini Break
11:30 - 12:00
VMCAI
Solving LIA* Using Approximations
12:00 - 12:30
VMCAI
Formalizing and Checking Multilevel Consistency
14:00 - 14:32
VMCAI
Practical Abstractions for Automated Verification of Shared-Memory Conc ...
14:32 - 15:05
VMCAI
Panel "The Future of Software Verification" at VMCAI
15:35 - 17:45
Thu 23 Jan
Displayed time zone:
Saskatchewan, Central America
change
Room
14:00
15
30
45
15:00
15
30
45
St Jerome
POPL Student Research Competition
SRC Finalists Presentations
14:00 - 15:30
x
Tue 16 Apr 08:58