Write a Blog >>
VMCAI 2017
Sun 15 - Tue 17 January 2017
co-located with POPL 2017
You're viewing the program in a time zone which is different from your device's time zone change time zone

Sun 15 Jan

Displayed time zone: Amsterdam, Berlin, Bern, Rome, Stockholm, Vienna change

09:00 - 10:00
Invited talk 1VMCAI at Amphitheater 44
Chair(s): David Monniaux CNRS, VERIMAG
09:00
60m
Talk
Detecting Strict Aliasing Violations in the Wild
VMCAI
Pascal Cuoq Trust-in-Soft
File Attached
10:30 - 12:00
Program AnalysisVMCAI at Amphitheater 44
Chair(s): Boris Yakobowski CEA - LIST
10:30
30m
Talk
Partitioned Memory Models for Program Analysis.
VMCAI
Wei Wang Google, Inc., Clark Barrett Stanford University, Thomas Wies New York University
File Attached
11:00
30m
Talk
Property Directed Reachability for Proving Absence of Concurrent Modification Errors
VMCAI
Asya Frumkin Tel Aviv University, Yotam M. Y. Feldman Tel Aviv University, Ondřej Lhoták University of Waterloo, Canada, Oded Padon Tel Aviv University, Mooly Sagiv Tel Aviv University, Sharon Shoham Tel Aviv university
File Attached
11:30
30m
Talk
Stabilizing Floating-Point Programs using Provenance Analysis
VMCAI
Yijia Gu Northeastern University, Thomas Wahl Northeastern University
14:00 - 15:30
Concurrency 1VMCAI at Amphitheater 44
Chair(s): Camille Coti LIPN, Université Paris 13
14:00
30m
Talk
Accuracy of Message Counting Abstraction in Fault-Tolerant Distributed Algorithms
VMCAI
14:30
30m
Talk
Independence Abstractions and Models of Concurrency
VMCAI
Vijay D'Silva Google Inc., Daniel Kroening University of Oxford, Marcelo Sousa University of Oxford
15:00
30m
Talk
Static Analysis of Communicating Process using Symbolic Transducers
VMCAI
Vincent Botbol CEA LIST + LIP6 Université Pierre & Marie Curie, Tristan Le Gall CEA LIST, Emmanuel Chailloux LIP6 - UPMC
Media Attached File Attached
16:00 - 17:30
Decision proceduresVMCAI at Amphitheater 44
Chair(s): Andreas Podelski University of Freiburg, Germany
16:00
30m
Talk
Synthesising Strategy Improvement and Recursive Algorithms for Solving 2.5 Player Parity Games
VMCAI
Ernst Moritz Hahn State Key Laboratory of Computer Science, Institute of Software, Chinese Academy of Sciences, Sven Schewe University of Liverpool, Andrea Turrini State Key Laboratory of Computer Science, Institute of Software, Chinese Academy of Sciences, Lijun Zhang Institute of Software, Chinese Academy of Sciences
File Attached
16:30
30m
Talk
Reasoning in the Bernays-Schönfinkel-Ramsey Fragment of Separation Logic
VMCAI
Andrew Reynolds EPFL, Radu Iosif VERIMAG, CNRS, Université Grenoble-Alpes, Cristina Serban VERIMAG, CNRS, Université Grenoble-Alpes
File Attached
17:00
30m
Talk
Matching multiplications in Bit-Vector formulas
VMCAI
Supratik Chakraborty IIT Bombay, Ashutosh Gupta , Rahul Jain Tata Institute of Fundamental Research
File Attached

Mon 16 Jan

Displayed time zone: Amsterdam, Berlin, Bern, Rome, Stockholm, Vienna change

09:00 - 10:00
Invited talk 2VMCAI at Amphitheater 44
Chair(s): Ahmed Bouajjani IRIF, Université Paris Diderot
09:00
60m
Talk
Verified Concurrent Code: Tricks of the Trade
VMCAI
A: Ernie Cohen Amazon Web Services
10:30 - 12:00
Numerical domainsVMCAI at Amphitheater 44
Chair(s): Laure Gonnord University of Lyon & LIP, France
10:30
30m
Talk
Sound Bit-Precise Numerical Domains
VMCAI
Tushar Sharma University of Wisconsin - Madison, USA, Thomas Reps University of Wisconsin - Madison and Grammatech Inc.
File Attached
11:00
30m
Talk
Efficient Elimination of Redundancies in Polyhedra using Raytracing
VMCAI
Media Attached File Attached
11:30
30m
Talk
Finding Relevant Templates via the Principal Component Analysis
VMCAI
Yassamine Seladji University of Tlemcen
File Attached
14:00 - 15:30
Model-checking and bug findingVMCAI at Amphitheater 44
Chair(s): Andreas Podelski University of Freiburg, Germany
14:00
30m
Talk
Effective Bug Finding in C Programs with Shape and Effect Abstraction
VMCAI
Iago Abal IT University of Copenhagen, Claus Brabrand IT University of Copenhagen, Denmark, Andrzej Wąsowski IT University of Copenhagen, Denmark
14:30
30m
Talk
Reduction of Workflow Nets for Generalised Soundness Verification
VMCAI
Hadrien Bride Femto-ST / Université de Franche-Comté, Olga Kouchnarenko Femto-ST / Université de Franche-Comté, Fabien Peureux Femto-ST / Université de Franche-Comté + Smartesting S&S
Media Attached
15:00
30m
Talk
Dynamic Reductions for Model Checking Concurrent Software.
VMCAI
Henning Günther Technische Universität Wien, Alfons Laarman Vienna University of Technology, Ana Sokolova University of Salzburg, Georg Weissenbacher Technische Universität Wien
File Attached
16:00 - 17:30
Symbolic analysis and invariant synthesisVMCAI at Amphitheater 44
Chair(s): Constantin Enea LIAFA, Université Paris Diderot
16:00
30m
Talk
Block-wise abstract interpretation by combining abstract domains with SMT
VMCAI
16:30
30m
Talk
IC3 - Flipping the E in ICE
VMCAI
Yakir Vizel , Arie Gurfinkel University of Waterloo, Sharon Shoham Tel Aviv university, Sharad Malik Princeton University
17:00
30m
Talk
Counterexample Validation and Interpolation-Based Refinement for Forest Automata
VMCAI
Lukáš Holík , Martin Hruska Brno University of Technology , Ondřej Lengál Brno University of Technology , Adam Rogalewicz Brno University of Technology , Tomáš Vojnar Brno University of Technology
19:30 - 22:00
BanquetVMCAI at Procope

Tue 17 Jan

Displayed time zone: Amsterdam, Berlin, Bern, Rome, Stockholm, Vienna change

09:00 - 10:00
Invited talk 3VMCAI at Amphitheater 44
Chair(s): Andreas Podelski University of Freiburg, Germany
09:00
60m
Talk
Verification of Cancer Programs
VMCAI
Jasmin Fisher Microsoft Research
10:30 - 12:00
Model Checking and SynthesisVMCAI at Amphitheater 44
Chair(s): Ahmed Bouajjani IRIF, Université Paris Diderot
10:30
30m
Talk
Reachability for dynamic parametric processes
VMCAI
Anca Muscholl Université de Bordeaux / LaBRI, Helmut Seidl Technische Universität München, Igor Walukiewicz CNRS, LaBRI
11:00
30m
Talk
Synthesizing Non-Vacuous Systems
VMCAI
Roderick Bloem Institute of Software Technology, Graz University of Technology , Hana Chockler , ma e , Ofer Strichman Technion
File Attached
11:30
30m
Talk
Solving Nonlinear Integer Arithmetic with MCSat
VMCAI
Dejan Jovanović SRI International
14:00 - 15:30
Abstract InterpretationVMCAI at Amphitheater 44
Chair(s): Roberto Giacobazzi University of Verona, Italy
14:00
30m
Talk
Complete Abstractions and Subclassical Modal Logics
VMCAI
Vijay D'Silva Google, Marcelo Sousa University of Oxford
14:30
30m
Talk
Structuring Abstract Interpreters through State and Value Abstractions
VMCAI
David Bühler CEA LIST, Boris Yakobowski CEA - LIST, Sandrine Blazy University of Rennes 1, France
Media Attached
15:00
30m
Talk
Conjunctive Abstract Interpretation using Paramodulation
VMCAI
Mooly Sagiv Tel Aviv University, A: Or Ozeri Tel Aviv university, Oded Padon Tel Aviv University, Noam Rinetzky Tel Aviv University
Media Attached
16:00 - 17:30
Concurrency 2VMCAI at Amphitheater 44
Chair(s): David Monniaux CNRS, VERIMAG
16:00
30m
Talk
Using Abstract Interpretation to Correct Synchronization Faults
VMCAI
Pietro Ferrara IBM Research, Omer Tripp IBM Thomas J. Watson Research Center, Peng Liu Purdue University, Eric Koskinen Yale University
16:30
30m
Talk
Detecting All High-Level Dataraces in an RTOS Kernel.
VMCAI
Suvam Mukherjee Indian Institute of Science, Arunkumar S Indian Institute of Science, Deepak D'Souza
17:00
30m
Talk
Precise Thread-Modular Abstract Interpretation of Concurrent Programs using Relational Interference Abstractions
VMCAI
Raphaël Monat Ecole Normale Supérieure de Lyon, Antoine Miné UPMC, France