VMCAI
Sun 17 - Tue 19 January 2016
St. Petersburg, Florida, United States
co-located with
POPL 2016
Toggle navigation
Attending
Venue: Hilton St. Petersburg Bayfront
VMCAI 2016 Proceedings
Registration
Invited Speakers
Student Travel Funding
Program
VMCAI Program
Your Program
Online Access to Conference Proceedings
Sun 17 Jan
Mon 18 Jan
Tue 19 Jan
Track/Call
Organization
VMCAI Committees
Program Chairs
Program Committee
Organizing Committee
Steering Committee
Contributors
People Index
Search
Series
Series
VMCAI 2025
VMCAI 2024
VMCAI 2023
VMCAI 2022
VMCAI 2021
VMCAI 2020
VMCAI 2019
VMCAI 2018
VMCAI 2017
VMCAI
Sign in
Sign up
POPL 2016
(
series
) /
VMCAI
(
series
) /
Hilton St. Petersburg Bayfront
/
Room information: Room St Petersburg I
Venue
Hilton St. Petersburg Bayfront
Room name
Room St Petersburg I
Floor
0
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-05:00) Guadalajara, Mexico City, Monterrey
.
Use conference time zone: (GMT-05:00) Guadalajara, Mexico City, Monterrey
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:30) Caracas
(GMT-03:00) Santiago
(GMT-04:00) La Paz
(GMT-03:00) Faukland Islands
(GMT-03: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-02: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+06: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+10:00) Magadan
(GMT+11: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 17 Jan
Displayed time zone:
Guadalajara, Mexico City, Monterrey
change
08:50 - 09:00
Welcome
VMCAI
at
Room St Petersburg I
Chair(s):
K. Rustan M. Leino
Microsoft Research
09:00 - 10:00
Invited Talk I
VMCAI
at
Room St Petersburg I
Chair(s):
Sharon Shoham
09:00
60m
Talk
Automating Abstract Interpretation
VMCAI
Thomas Reps
University of Wisconsin - Madison and Grammatech Inc.
10:30 - 12:00
Abstract Interpretation
VMCAI
at
Room St Petersburg I
Chair(s):
Peter Müller
ETH Zurich
10:30
30m
Talk
An Abstract Domain of Uninterpreted Functions
VMCAI
Graeme Gange
,
Jorge A. Navas
,
Peter Schachte
,
Harald Sondergaard
,
Peter Stuckey
11:00
30m
Talk
Predicate Abstraction for Linked Data Structures
VMCAI
Alexander Bakst
,
Ranjit Jhala
University of California, San Diego
11:30
30m
Talk
Property Directed Abstract Interpretation
VMCAI
Noam Rinetzky
,
Sharon Shoham
14:00 - 15:30
Abstraction I
VMCAI
at
Room St Petersburg I
Chair(s):
Eva Darulova
MPI-SWS, Germany
14:00
30m
Talk
Program Analysis with Local Policy Iteration
VMCAI
Egor Karpenkov
,
David Monniaux
CNRS, VERIMAG
,
Philipp Wendler
14:30
30m
Talk
Lazy Constrained Monotonic Abstraction
VMCAI
Zeinab Ganjei
,
Ahmed Rezine
,
Petru Eles
,
Zebo Peng
15:00
30m
Talk
Polyhedral Approximation of Multivariate Polynomials using Handelman’s Theorem
VMCAI
Alexandre Maréchal
,
Alexis Fouilhé
,
Tim King
,
David Monniaux
CNRS, VERIMAG
,
Michael Perin
16:00 - 17:00
Abstraction II
VMCAI
at
Room St Petersburg I
Chair(s):
David Pichardie
16:00
30m
Talk
D3 : Data-Driven Disjunctive Abstraction
VMCAI
Hila Peleg
,
Sharon Shoham
,
Eran Yahav
Technion
16:30
30m
Talk
Exact Heap Summaries for Symbolic Execution
VMCAI
Benjamin Hillery
,
Eric Mercer
,
Neha Rungta
,
Suzette Person
Mon 18 Jan
Displayed time zone:
Guadalajara, Mexico City, Monterrey
change
09:00 - 10:00
Invited Talk II
VMCAI
at
Room St Petersburg I
Chair(s):
K. Rustan M. Leino
Microsoft Research
09:00
60m
Talk
Ironclad - Full Verification of Complex Systems
VMCAI
Bryan Parno
Microsoft Research
10:30 - 12:00
Hybrid and Timed Systems
VMCAI
at
Room St Petersburg I
Chair(s):
David Monniaux
CNRS, VERIMAG
10:30
30m
Talk
Abstract Interpretation with Infinitesimals
VMCAI
Kengo Kido
,
Swarat Chaudhuri
Rice University
,
Ichiro Hasuo
University of Tokyo
11:00
30m
Talk
Lipschitz Robustness of Timed I/O Systems
VMCAI
Thomas A. Henzinger
IST Austria
,
Jan Otop
University of Wrocław
,
Roopsha Samanta
IST Austria
11:30
30m
Talk
A method for invariant generation for polynomial continuous systems
VMCAI
Andrew Sogokon
,
Khalil Ghorbal
Carnegie Mellon University
,
Paul Jackson
,
André Platzer
14:00 - 15:30
Dynamic and Static Verification
VMCAI
at
Room St Petersburg I
Chair(s):
Aarti Gupta
Princeton University
14:00
30m
Talk
Hybrid Analysis for Partial Order Reduction of Programs with Arrays
VMCAI
Pavel Parizek
Charles University in Prague
14:30
30m
Talk
Cloud-Based Verification of Concurrent Software
VMCAI
Gerald Holzmann
15:00
30m
Talk
Abstraction-driven Concolic Testing
VMCAI
Przemyslaw Daca
,
Ashutosh Gupta
,
Thomas A. Henzinger
IST Austria
16:00 - 17:00
Probabilistic Systems
VMCAI
at
Room St Petersburg I
Chair(s):
Paul Jackson
16:00
30m
Talk
Reward-Bounded Reachability Probability for Uncertain Weighted MDPs
VMCAI
Vahid Hashemi
,
Holger Hermanns
,
Lei Song
16:30
30m
Talk
Parameter Synthesis for Parametric Interval Markov Chains
VMCAI
Benoit Delahaye
,
Didier Lime
,
Laure Petrucci
Tue 19 Jan
Displayed time zone:
Guadalajara, Mexico City, Monterrey
change
09:00 - 10:00
Invited Talk III
VMCAI
at
Room St Petersburg I
Chair(s):
Bor-Yuh Evan Chang
University of Colorado Boulder
09:00
60m
Talk
Viper - A Verification Infrastructure for Permission-based Reasoning
VMCAI
Peter Müller
ETH Zurich
10:30 - 12:00
Concurrent Programs
VMCAI
at
Room St Petersburg I
Chair(s):
Noam Rinetzky
10:30
30m
Talk
Pointer Race Freedom
VMCAI
Frédéric Haziza
,
Lukáš Holík
,
Roland Meyer
,
Sebastian Wolff
Fraunhofer ITWM and TU Kaiserslautern
11:00
30m
Talk
A program logic for C11 memory fences
VMCAI
Marko Doko
MPI-SWS, Germany
,
Viktor Vafeiadis
MPI-SWS, Germany
11:30
30m
Talk
From Low Level Pointers to High Level Containers
VMCAI
Kamil Dudka
,
Lukáš Holík
,
Petr Peringer
,
Tomáš Vojnar
Brno University of Technology
14:00 - 15:30
Parameterized and Component-Based Systems
VMCAI
at
Room St Petersburg I
Chair(s):
Arie Gurfinkel
Carnegie Mellon University
14:00
30m
Talk
Regular Symmetry Patterns
VMCAI
Anthony Widjaja Lin
Yale-NUS College, Singapore
,
Truong Khanh Nguyen
,
Philipp Ruemmer
Uppsala University
,
Jun Sun
14:30
30m
Talk
Tight Cutoffs for Guarded Protocols with Fairness
VMCAI
Simon Außerlechner
,
Swen Jacobs
,
Ayrat Khalimov
15:00
30m
Talk
A General Modular Synthesis Problem for Pushdown Systems
VMCAI
Ilaria De Crescenzo
,
Salvatore La Torre
16:00 - 17:00
Solver Improvements
VMCAI
at
Room St Petersburg I
Chair(s):
Roopsha Samanta
IST Austria
16:00
30m
Talk
Model Checking with Multi-Threaded IC3 Portfolios
VMCAI
Sagar Chaki
,
Derrick Karimi
16:30
30m
Talk
Automatic Generation of Propagation Complete SAT Encodings
VMCAI
Martin Brain
,
Liana Hadarean
,
Daniel Kroening
University of Oxford
,
Ruben Martins
18:00 - 21:00
CPP Reception, sponsored by the DeepSpec project
CPP
at
Room St Petersburg I
18:00
3h
Social Event
CPP Reception, sponsored by the DeepSpec project
CPP
Sat 23 Jan
Displayed time zone:
Guadalajara, Mexico City, Monterrey
change
09:00 - 10:00
Session One
Off the Beaten Track
at
Room St Petersburg I
Chair(s):
Lindsey Kuper
Intel Labs
09:00
15m
Day opening
Opening remarks and program chair's report
Off the Beaten Track
Lindsey Kuper
Intel Labs
09:15
45m
Talk
Keynote Talk: Operationalizing Creative Theories
Off the Beaten Track
K:
Chris Martens
Carnegie Mellon University
10:30 - 12:10
Session Two
Off the Beaten Track
at
Room St Petersburg I
Chair(s):
Suresh Jagannathan
DARPA
10:30
25m
Talk
Chanakya: Computer-Aided Strategic Reasoning
Off the Beaten Track
Suguman Bansal
Rice University, USA
,
A:
Swarat Chaudhuri
Rice University
Pre-print
10:55
25m
Talk
Programming Interactivity Requires Both Semantics and Semiotics
Off the Beaten Track
Joseph Osborn
,
Michael Mateas
Pre-print
11:20
25m
Talk
Correct-by-Construction Interactive Software: From Declarative Specifications to Efficient Implementations
Off the Beaten Track
Kyle Headley
,
A:
Matthew Hammer
University of Colorado, Boulder
Pre-print
11:45
25m
Talk
Challenges Facing a High-Level Language for Machine Knitting
Off the Beaten Track
Lea Albaugh
,
James McCann
Pre-print
14:00 - 15:35
Session Three
Off the Beaten Track
at
Room St Petersburg I
Chair(s):
Limin Jia
Carnegie Mellon University
14:00
45m
Talk
Keynote Talk: Generalising Abstraction
Off the Beaten Track
K:
Robert Atkey
University of Strathclyde
14:45
25m
Talk
The Semantics of Syntax: Applying Denotational Semantics to Hygienic Macro Systems
Off the Beaten Track
A:
Neel Krishnaswami
Pre-print
15:10
25m
Talk
Affine Functional Programs as Higher-order Boolean Circuits
Off the Beaten Track
Damiano Mazza
Pre-print
16:00 - 17:30
Session Four
Off the Beaten Track
at
Room St Petersburg I
Chair(s):
Nada Amin
EPFL
16:00
25m
Talk
Declarative, Secure, Convergent Edge Computation
Off the Beaten Track
A:
Christopher Meiklejohn
Pre-print
16:25
25m
Talk
Starting from a Clean Slate: Creating a Top-down Parseable Runtime
Off the Beaten Track
A:
Randolph Langley
Pre-print
16:50
25m
Talk
New Tools and Practices for Online Collaboration in Teaching, Learning, and Research of Programming Languages
Off the Beaten Track
A:
William E. Byrd
University of Utah
Pre-print
17:15
15m
Day closing
Closing remarks
Off the Beaten Track
Sun 17 Jan
Displayed time zone:
Guadalajara, Mexico City, Monterrey
change
Room
8:00
30
9:00
30
10:00
30
11:00
30
12:00
30
13:00
30
14:00
30
15:00
30
16:00
30
Room St Petersburg I
VMCAI
Welcome
VMCAI
Invited Talk I
VMCAI
Abstract Interpretation
VMCAI
Abstraction I
VMCAI
Abstraction II
Mon 18 Jan
Displayed time zone:
Guadalajara, Mexico City, Monterrey
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
Room St Petersburg I
VMCAI
Invited Talk II
VMCAI
Hybrid and Timed Systems
VMCAI
Dynamic and Static Verification
VMCAI
Probabilistic Systems
Tue 19 Jan
Displayed time zone:
Guadalajara, Mexico City, Monterrey
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
18:00
30
19:00
30
20:00
30
Room St Petersburg I
PADL
VMCAI
Invited Talk III
09:00 - 10:00
VMCAI
Concurrent Programs
VMCAI
Parameterized and Component-Based Systems
VMCAI
Solver Improvements
CPP
CPP Reception, sponsored by the DeepSpec project
Sat 23 Jan
Displayed time zone:
Guadalajara, Mexico City, Monterrey
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
Room St Petersburg I
Off the Beaten Track
Session One
Off the Beaten Track
Session Two
Off the Beaten Track
Session Three
Off the Beaten Track
Session Four
Sun 17 Jan
Displayed time zone:
Guadalajara, Mexico City, Monterrey
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
Room St Petersburg I
VMCAI
Automating Abstract Interpretation
09:00 - 10:00
VMCAI
An Abstract Domain of Uninterpreted Functions
10:30 - 11:00
VMCAI
Predicate Abstraction for Linked Data Structures
11:00 - 11:30
VMCAI
Property Directed Abstract Interpretation
11:30 - 12:00
VMCAI
Program Analysis with Local Policy Iteration
14:00 - 14:30
VMCAI
Lazy Constrained Monotonic Abstraction
14:30 - 15:00
VMCAI
Polyhedral Approximation of Multivariate Polynomials using Handelman’s ...
15:00 - 15:30
VMCAI
D3 : Data-Driven Disjunctive Abstraction
16:00 - 16:30
VMCAI
Exact Heap Summaries for Symbolic Execution
16:30 - 17:00
Mon 18 Jan
Displayed time zone:
Guadalajara, Mexico City, Monterrey
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
Room St Petersburg I
VMCAI
Ironclad - Full Verification of Complex Systems
09:00 - 10:00
VMCAI
Abstract Interpretation with Infinitesimals
10:30 - 11:00
VMCAI
Lipschitz Robustness of Timed I/O Systems
11:00 - 11:30
VMCAI
A method for invariant generation for polynomial continuous systems
11:30 - 12:00
VMCAI
Hybrid Analysis for Partial Order Reduction of Programs with Arrays
14:00 - 14:30
VMCAI
Cloud-Based Verification of Concurrent Software
14:30 - 15:00
VMCAI
Abstraction-driven Concolic Testing
15:00 - 15:30
VMCAI
Reward-Bounded Reachability Probability for Uncertain Weighted MDPs
16:00 - 16:30
VMCAI
Parameter Synthesis for Parametric Interval Markov Chains
16:30 - 17:00
Tue 19 Jan
Displayed time zone:
Guadalajara, Mexico City, Monterrey
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
18:00
15
30
45
19:00
15
30
45
20:00
15
30
45
Room St Petersburg I
VMCAI
Viper - A Verification Infrastructure for Permission-based Reasoning
09:00 - 10:00
VMCAI
Pointer Race Freedom
10:30 - 11:00
VMCAI
A program logic for C11 memory fences
11:00 - 11:30
VMCAI
From Low Level Pointers to High Level Containers
11:30 - 12:00
VMCAI
Regular Symmetry Patterns
14:00 - 14:30
VMCAI
Tight Cutoffs for Guarded Protocols with Fairness
14:30 - 15:00
VMCAI
A General Modular Synthesis Problem for Pushdown Systems
15:00 - 15:30
VMCAI
Model Checking with Multi-Threaded IC3 Portfolios
16:00 - 16:30
VMCAI
Automatic Generation of Propagation Complete SAT Encodings
16:30 - 17:00
CPP
CPP Reception, sponsored by the DeepSpec project
18:00 - 21:00
Sat 23 Jan
Displayed time zone:
Guadalajara, Mexico City, Monterrey
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
Room St Petersburg I
Off the Beaten Track
Opening remarks and program chair's report
09:00 - 09:15
Off the Beaten Track
Keynote Talk: Operationalizing Creative Theories
09:15 - 10:00
Off the Beaten Track
Chanakya: Computer-Aided Strategic Reasoning
10:30 - 10:55
Off the Beaten Track
Programming Interactivity Requires Both Semantics and Semiotics
10:55 - 11:20
Off the Beaten Track
Correct-by-Construction Interactive Software: From Declarative Specific ...
11:20 - 11:45
Off the Beaten Track
Challenges Facing a High-Level Language for Machine Knitting
11:45 - 12:10
Off the Beaten Track
Keynote Talk: Generalising Abstraction
14:00 - 14:45
Off the Beaten Track
The Semantics of Syntax: Applying Denotational Semantics to Hygienic Ma ...
14:45 - 15:10
Off the Beaten Track
Affine Functional Programs as Higher-order Boolean Circuits
15:10 - 15:35
Off the Beaten Track
Declarative, Secure, Convergent Edge Computation
16:00 - 16:25
Off the Beaten Track
Starting from a Clean Slate: Creating a Top-down Parseable Runtime
16:25 - 16:50
Off the Beaten Track
New Tools and Practices for Online Collaboration in Teaching, Learning, ...
16:50 - 17:15
Off the Beaten Track
Closing remarks
17:15 - 17:30
x
Sat 21 Dec 18:02