POPL 2019 (series) / VMCAI 2019 (series) /
VMCAI 2019 Program
This is the VMCAI 2019 program - see the full program for POPL 2019 and all affiliated events.
Filter Program
Dates
Rooms
Tracks
Badges
Your Program
Sun 13 JanDisplayed time zone: Belfast change
Sun 13 Jan
Displayed time zone: Belfast change
09:00 - 10:30 | |||
09:00 90mTalk | Under and Over Approximated Reachability Analysis for the Verifcation of Control Systems VMCAI Sylvie Putot École Polytechnique |
11:00 - 12:30 | |||
11:00 30mTalk | 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 30mTalk | Disjunctive Relational Abstract Interpretation for Interprocedural Program Analysis VMCAI File Attached | ||
12:00 30mTalk | Application of Abstract Interpretation to the Automotive Electronic Control System VMCAI |
14:00 - 15:30 | |||
14:00 30mTalk | Minimal Synthesis of String To String Functions From Examples VMCAI | ||
14:30 30mTalk | Lazy but Effective Functional Synthesis VMCAI Grigory Fedyukovich Princeton University, Arie Gurfinkel University of Waterloo, Aarti Gupta Princeton University | ||
15:00 30mTalk | 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 30mTalk | 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 30mTalk | 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 30mTalk | 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 JanDisplayed time zone: Belfast change
Mon 14 Jan
Displayed time zone: Belfast change
09:00 - 10:30 | |||
09:00 90mTalk | Designing Self-Certifying Software Systems VMCAI Kedar Namjoshi Bell Labs, Nokia |
11:00 - 12:30 | |||
11:00 30mTalk | Solving and Interpolating Constant Arrays Based on Weak Equivalences VMCAI | ||
11:30 30mTalk | A Decidable Logic for Tree Data-Structures with Measurements VMCAI File Attached | ||
12:00 30mTalk | A Practical Algorithm for Structure Embedding VMCAI File Attached |
14:00 - 15:30 | |||
14:00 30mTalk | Syntactic Partial Order Compression for Probabilistic Reachability VMCAI | ||
14:30 30mTalk | Termination of Nondeterministic Probabilistic Programs VMCAI | ||
15:00 30mTalk | Combining Refinement of Parametric Models with Goal-Oriented Reduction of Dynamics VMCAI |
16:00 - 17:30 | |||
16:00 30mTalk | 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 30mTalk | A Parallel Relation-Based Algorithm for Symbolic Bisimulation Minimization VMCAI File Attached | ||
17:00 30mTalk | Flat Model Checking for Counting LTL using Quantifier-free Presburger Arithmetic VMCAI |
Tue 15 JanDisplayed time zone: Belfast change
Tue 15 Jan
Displayed time zone: Belfast change
09:00 - 10:30 | |||
09:00 90mTalk | Semantics for Compiler IRs: Undefined Behavior is not Evil! VMCAI Nuno P. Lopes Microsoft Research Media Attached |
11:00 - 12:30 | |||
11:00 30mTalk | Mechanically Proving Determinacy of Hierarchical Block Diagram Translations VMCAI Link to publication DOI Pre-print File Attached | ||
11:30 30mTalk | euforia: Complete Software Model Checking with Uninterpreted Functions VMCAI | ||
12:00 30mTalk | Program Synthesis with Equivalence Reduction VMCAI |
14:00 - 15:30 | |||
14:00 30mTalk | 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 30mTalk | 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 30mTalk | 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 | |||
16:00 30mTalk | On the Semantics of Snapshot Isolation VMCAI | ||
16:30 30mTalk | Fast BGP Simulation of Large Datacenters VMCAI Pre-print | ||
17:00 30mTalk | Parametric Timed Broadcast Protocols VMCAI Étienne André LIPN, CNRS UMR 7030, Université Paris 13, Benoit Delahaye , Paulin Fournier , Didier Lime File Attached |