POPL 2017 (series) / VMCAI 2017 (series) /
VMCAI 2017 Program
This is the VMCAI 2017 program - see the full program for POPL 2017 and all affiliated events.
Filter Program
Dates
Rooms
Tracks
Badges
Your Program
Sun 15 JanDisplayed time zone: Amsterdam, Berlin, Bern, Rome, Stockholm, Vienna change
Sun 15 Jan
Displayed time zone: Amsterdam, Berlin, Bern, Rome, Stockholm, Vienna change
09:00 - 10:00 | |||
09:00 60mTalk | Detecting Strict Aliasing Violations in the Wild VMCAI Pascal Cuoq Trust-in-Soft File Attached | ||
10:30 - 12:00 | |||
10:30 30mTalk | Partitioned Memory Models for Program Analysis. VMCAI File Attached | ||
11:00 30mTalk | 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 30mTalk | Stabilizing Floating-Point Programs using Provenance Analysis VMCAI | ||
14:00 - 15:30 | |||
14:00 30mTalk | Accuracy of Message Counting Abstraction in Fault-Tolerant Distributed Algorithms VMCAI | ||
14:30 30mTalk | Independence Abstractions and Models of Concurrency VMCAI | ||
15:00 30mTalk | 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 30mTalk | 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 30mTalk | 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 30mTalk | Matching multiplications in Bit-Vector formulas VMCAI File Attached | ||
Mon 16 JanDisplayed time zone: Amsterdam, Berlin, Bern, Rome, Stockholm, Vienna change
Mon 16 Jan
Displayed time zone: Amsterdam, Berlin, Bern, Rome, Stockholm, Vienna change
09:00 - 10:00 | |||
09:00 60mTalk | Verified Concurrent Code: Tricks of the Trade VMCAI | ||
10:30 - 12:00 | |||
10:30 30mTalk | 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 30mTalk | Efficient Elimination of Redundancies in Polyhedra using Raytracing VMCAI Media Attached File Attached | ||
11:30 30mTalk | 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 30mTalk | 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 30mTalk | 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 30mTalk | 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 30mTalk | Block-wise abstract interpretation by combining abstract domains with SMT VMCAI | ||
16:30 30mTalk | 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 30mTalk | 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 | ||
Tue 17 JanDisplayed time zone: Amsterdam, Berlin, Bern, Rome, Stockholm, Vienna change
Tue 17 Jan
Displayed time zone: Amsterdam, Berlin, Bern, Rome, Stockholm, Vienna change
09:00 - 10:00 | |||
09:00 60mTalk | 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 30mTalk | 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 30mTalk | 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 30mTalk | 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 30mTalk | Complete Abstractions and Subclassical Modal Logics VMCAI | ||
14:30 30mTalk | Structuring Abstract Interpreters through State and Value Abstractions VMCAI Media Attached | ||
15:00 30mTalk | 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 | |||
16:00 30mTalk | 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 30mTalk | 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 30mTalk | Precise Thread-Modular Abstract Interpretation of Concurrent Programs using Relational Interference Abstractions VMCAI | ||