Blogs (1) >>
POPL 2019
Sun 13 - Sat 19 January 2019 Cascais, Portugal
POPL 2019 (series) / Hotel Cascais Miragem /

Room information: Sala III

VenueHotel Cascais Miragem
Room nameSala III
Floor0
Room InformationNo extra information available
Program

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

Sun 13 Jan

Displayed time zone: Belfast change

09:00 - 10:30
Invited Talk 1VMCAI at Sala III
Chair(s): Constantin Enea Université Paris Diderot
09:00
90m
Talk
Under and Over Approximated Reachability Analysis for the Verifcation of Control Systems
VMCAI
Sylvie Putot École Polytechnique
11:00 - 12:30
Abstract Interpretation (1)VMCAI at Sala III
Chair(s): Patrick M. Cousot
11:00
30m
Talk
Static Analysis of Binary Code with Memory Indirections Using Polyhedra
VMCAI
Clément Ballabriga , Julien Forget , Laure Gonnord University of Lyon & LIP, France, Giuseppe Lipari , Jordy Ruiz
File Attached
11:30
30m
Talk
Disjunctive Relational Abstract Interpretation for Interprocedural Program Analysis
VMCAI
Rémy Boutonnet , Nicolas Halbwachs
File Attached
12:00
30m
Talk
Application of Abstract Interpretation to the Automotive Electronic Control System
VMCAI
Tomoya Yamaguchi , Martin Brain , Chris Ryder , Yosikazu Imai , Yoshiumi Kawamura
14:00 - 15:30
Program SynthesisVMCAI at Sala III
Chair(s): Nuno P. Lopes Microsoft Research
14:00
30m
Talk
Minimal Synthesis of String To String Functions From Examples
VMCAI
Jad Hamza LIAFA, Université Paris Diderot, Viktor Kunčak EPFL, Switzerland
14:30
30m
Talk
Lazy but Effective Functional Synthesis
VMCAI
Grigory Fedyukovich Princeton University, Arie Gurfinkel University of Waterloo, Aarti Gupta Princeton University
15:00
30m
Talk
Automatic Program Repair using Formal Verification and Expression Templates
VMCAI
Thanh-Toan Nguyen , Quang-Trung Ta National University of Singapore, Wei-Ngan Chin National University of Singapore
16:00 - 17:30
Abstract Interpretation (2)VMCAI at Sala III
Chair(s): Mihaela Sighireanu IRIF, University Paris Diderot and CNRS, France
16:00
30m
Talk
Demand Control-Flow Analysis
VMCAI
Kimball Germane University of Utah, Jay McCarthy University of Massachusetts Lowell, Michael D. Adams University of Utah, Matthew Might University of Alabama at Birmingham | Harvard Medical School
16:30
30m
Talk
Effect-driven Flow Analysis
VMCAI
Jens Nicolay Vrije Universiteit Brussel, Belgium, Quentin Stiévenart Vrije Universiteit Brussel, Belgium, Wolfgang De Meuter Vrije Universiteit Brussel, Coen De Roover Vrije Universiteit Brussel
17:00
30m
Talk
Relatively Complete Pushdown Analysis of Escape Continuations
VMCAI
Kimball Germane University of Utah, Matthew Might University of Alabama at Birmingham | Harvard Medical School

Mon 14 Jan

Displayed time zone: Belfast change

09:00 - 10:30
Invited Talk 2VMCAI at Sala III
Chair(s): Lenore Zuck
09:00
90m
Talk
Designing Self-Certifying Software Systems
VMCAI
Kedar Namjoshi Bell Labs, Nokia
11:00 - 12:30
Decision ProceduresVMCAI at Sala III
Chair(s): Kedar Namjoshi Bell Labs, Nokia
11:00
30m
Talk
Solving and Interpolating Constant Arrays Based on Weak Equivalences
VMCAI
Jochen Hoenicke Universität Freiburg, Tanja Schindler University of Freiburg
11:30
30m
Talk
A Decidable Logic for Tree Data-Structures with Measurements
VMCAI
Xiaokang Qiu Purdue University, Yanjun Wang Purdue University
File Attached
12:00
30m
Talk
A Practical Algorithm for Structure Embedding
VMCAI
Charlie Murphy Princeton University, Zachary Kincaid Princeton University
File Attached
14:00 - 15:30
Probabilistic SystemsVMCAI at Sala III
Chair(s): Justin Hsu University of Wisconsin-Madison, USA
14:00
30m
Talk
Syntactic Partial Order Compression for Probabilistic Reachability
VMCAI
Gereon Fox , Daniel Stan , Holger Hermanns Saarland University
14:30
30m
Talk
Termination of Nondeterministic Probabilistic Programs
VMCAI
Hongfei Fu IST Austria, Krishnendu Chatterjee IST Austria
15:00
30m
Talk
Combining Refinement of Parametric Models with Goal-Oriented Reduction of Dynamics
VMCAI
Stefan Haar , Juraj Kolčák LSV, CNRS & ENS Cachan, University Paris Saclay, Loïc Paulevé
16:00 - 17:30
Model CheckingVMCAI at Sala III
Chair(s): Xiaokang Qiu Purdue University
16:00
30m
Talk
Verification of an Industrial Asynchronous Leader Election Algorithm Using Abstractions and Parametric Model Checking
VMCAI
Étienne André LIPN, CNRS UMR 7030, Université Paris 13, Laurent Fribourg , Romain Soulat , Jean-Marc Mota
16:30
30m
Talk
A Parallel Relation-Based Algorithm for Symbolic Bisimulation Minimization
VMCAI
Alfons Laarman Leiden University, Richard Huybers
File Attached
17:00
30m
Talk
Flat Model Checking for Counting LTL using Quantifier-free Presburger Arithmetic
VMCAI
Normann Decker , Anton Pirogov

Tue 15 Jan

Displayed time zone: Belfast change

09:00 - 10:30
Invited Talk 3VMCAI at Sala III
Chair(s): Ruzica Piskac Yale University, USA
09:00
90m
Talk
Semantics for Compiler IRs: Undefined Behavior is not Evil!
VMCAI
Nuno P. Lopes Microsoft Research
Media Attached
11:00 - 12:30
Software Verification and SynthesisVMCAI at Sala III
Chair(s): Ori Lahav Tel Aviv University
11:00
30m
Talk
Mechanically Proving Determinacy of Hierarchical Block Diagram Translations
VMCAI
Viorel Preoteasa , Iulia Dragomir , Stavros Tripakis Aalto University and UC Berkeley
Link to publication DOI Pre-print File Attached
11:30
30m
Talk
euforia: Complete Software Model Checking with Uninterpreted Functions
VMCAI
Denis Bueno , Karem A. Sakallah
12:00
30m
Talk
Program Synthesis with Equivalence Reduction
VMCAI
Calvin Smith University of Wisconsin - Madison, Aws Albarghouthi University of Wisconsin-Madison
14:00 - 15:30
Software VerificationVMCAI at Sala III
Chair(s): Grigory Fedyukovich Princeton University
14:00
30m
Talk
Type-directed Bounding of Collections in Reactive Programs
VMCAI
Tianhan Lu University of Colorado Boulder, Pavol Cerny University of Colorado Boulder, Bor-Yuh Evan Chang University of Colorado Boulder, Ashutosh Trivedi
14:30
30m
Talk
Exploiting Pointer Analysis in Memory Models for Deductive Verification
VMCAI
Quentin Bouillaguet , François Bobot CEA, Mihaela Sighireanu IRIF, University Paris Diderot and CNRS, France, Boris Yakobowski CEA - LIST
File Attached
15:00
30m
Talk
Small Faults Grow Up - Verification of Error Masking Robustness in Arithmetically Encoded Programs
VMCAI
Anja Karl Institute of Applied Information Processing and Communications, Graz University of Technology, Robert Schilling , Roderick Bloem Institute of Software Technology, Graz University of Technology , Stefan Mangard
16:00 - 17:30
Networks and ConcurrencyVMCAI at Sala III
Chair(s): Cezara Drăgoi INRIA, ENS, CNRS
16:00
30m
Talk
On the Semantics of Snapshot Isolation
VMCAI
Azalea Raad MPI-SWS, Germany, Ori Lahav Tel Aviv University, Viktor Vafeiadis MPI-SWS, Germany
16:30
30m
Talk
Fast BGP Simulation of Large Datacenters
VMCAI
Nuno P. Lopes Microsoft Research, Andrey Rybalchenko Microsoft Research
Pre-print
17:00
30m
Talk
Parametric Timed Broadcast Protocols
VMCAI
Étienne André LIPN, CNRS UMR 7030, Université Paris 13, Benoit Delahaye , Paulin Fournier , Didier Lime
File Attached

Thu 17 Jan

Displayed time zone: Belfast change

10:30 - 12:30
Finalist Poster PresentationsStudent Research Competition at Sala III

Sun 13 Jan

Displayed time zone: Belfast change

Room9:003010:003011:003012:003013:003014:003015:003016:003017:0030
Sala III

VMCAI

Invited Talk 1

VMCAI

Abstract Interpretation (1)

VMCAI

Program Synthesis

VMCAI

Abstract Interpretation (2)

Mon 14 Jan

Displayed time zone: Belfast change

Room9:003010:003011:003012:003013:003014:003015:003016:003017:0030
Sala III

VMCAI

Invited Talk 2

VMCAI

Decision Procedures

VMCAI

Probabilistic Systems

VMCAI

Model Checking

Tue 15 Jan

Displayed time zone: Belfast change

Room9:003010:003011:003012:003013:003014:003015:003016:003017:0030
Sala III

VMCAI

Invited Talk 3

VMCAI

Software Verification and Synthesis

VMCAI

Software Verification

VMCAI

Networks and Concurrency

Thu 17 Jan

Displayed time zone: Belfast change

Room10:003011:003012:0030
Sala III

Student Research Competition

Finalist Poster Presentations

Sun 13 Jan

Displayed time zone: Belfast change

Room9:0015304510:0015304511:0015304512:0015304513:0015304514:0015304515:0015304516:0015304517:00153045
Sala III
VMCAI
Under and Over Approximated Reachability Analysis for the Verifcation o ...
09:00 - 10:30
VMCAI
Static Analysis of Binary Code with Memory Indirections Using Polyhedra
11:00 - 11:30
VMCAI
Disjunctive Relational Abstract Interpretation for Interprocedural Prog ...
11:30 - 12:00
VMCAI
Application of Abstract Interpretation to the Automotive Electronic Con ...
12:00 - 12:30
VMCAI
Minimal Synthesis of String To String Functions From Examples
14:00 - 14:30
VMCAI
Lazy but Effective Functional Synthesis
14:30 - 15:00
VMCAI
Automatic Program Repair using Formal Verification and Expression Templates
15:00 - 15:30
VMCAI
Demand Control-Flow Analysis
16:00 - 16:30
VMCAI
Effect-driven Flow Analysis
16:30 - 17:00
VMCAI
Relatively Complete Pushdown Analysis of Escape Continuations
17:00 - 17:30

Mon 14 Jan

Displayed time zone: Belfast change

Room9:0015304510:0015304511:0015304512:0015304513:0015304514:0015304515:0015304516:0015304517:00153045
Sala III
VMCAI
Designing Self-Certifying Software Systems
09:00 - 10:30
VMCAI
Solving and Interpolating Constant Arrays Based on Weak Equivalences
11:00 - 11:30
VMCAI
A Decidable Logic for Tree Data-Structures with Measurements
11:30 - 12:00
VMCAI
A Practical Algorithm for Structure Embedding
12:00 - 12:30
VMCAI
Syntactic Partial Order Compression for Probabilistic Reachability
14:00 - 14:30
VMCAI
Termination of Nondeterministic Probabilistic Programs
14:30 - 15:00
VMCAI
Combining Refinement of Parametric Models with Goal-Oriented Reduction ...
15:00 - 15:30
VMCAI
Verification of an Industrial Asynchronous Leader Election Algorithm Us ...
16:00 - 16:30
VMCAI
A Parallel Relation-Based Algorithm for Symbolic Bisimulation Minimization
16:30 - 17:00
VMCAI
Flat Model Checking for Counting LTL using Quantifier-free Presburger A ...
17:00 - 17:30

Tue 15 Jan

Displayed time zone: Belfast change

Room9:0015304510:0015304511:0015304512:0015304513:0015304514:0015304515:0015304516:0015304517:00153045
Sala III
VMCAI
Semantics for Compiler IRs: Undefined Behavior is not Evil!
09:00 - 10:30
VMCAI
Mechanically Proving Determinacy of Hierarchical Block Diagram Translations
11:00 - 11:30
VMCAI
euforia: Complete Software Model Checking with Uninterpreted Functions
11:30 - 12:00
VMCAI
Program Synthesis with Equivalence Reduction
12:00 - 12:30
VMCAI
Type-directed Bounding of Collections in Reactive Programs
14:00 - 14:30
VMCAI
Exploiting Pointer Analysis in Memory Models for Deductive Verification
14:30 - 15:00
VMCAI
Small Faults Grow Up - Verification of Error Masking Robustness in Arit ...
15:00 - 15:30
VMCAI
On the Semantics of Snapshot Isolation
16:00 - 16:30
VMCAI
Fast BGP Simulation of Large Datacenters
16:30 - 17:00
VMCAI
Parametric Timed Broadcast Protocols
17:00 - 17:30