Program - VMCAI 2017

Filter

Sun 15 Jan

09:00 - 10:00: VMCAI - Invited talk 1 at Amphitheater 44
Chair(s): David MonniauxCNRS, VERIMAG

09:00 - 10:00
Talk

Detecting Strict Aliasing Violations in the Wild

Pascal CuoqTrust-in-Soft

File Attached

10:30 - 12:00: VMCAI - Program Analysis at Amphitheater 44
Chair(s): Boris YakobowskiCEA - LIST

10:30 - 11:00
Talk

Partitioned Memory Models for Program Analysis.

Wei WangGoogle, Inc., Clark BarrettStanford University, Thomas WiesNew York University

File Attached

11:00 - 11:30
Talk

Property Directed Reachability for Proving Absence of Concurrent Modification Errors

Asya FrumkinTel Aviv University, Yotam FeldmanTel Aviv University, Ondřej LhotákUniversity of Waterloo, Canada, Oded PadonTel Aviv University, Mooly SagivTel Aviv University, Sharon ShohamTel Aviv university

File Attached

11:30 - 12:00
Talk

Stabilizing Floating-Point Programs using Provenance Analysis

Yijia GuNortheastern University, Thomas WahlNortheastern University

14:00 - 15:30: VMCAI - Concurrency 1 at Amphitheater 44
Chair(s): Camille CotiLIPN, Université Paris 13

14:00 - 14:30
Talk

Accuracy of Message Counting Abstraction in Fault-Tolerant Distributed Algorithms

Igor KonnovTU Wien, Josef WidderTU Wien, Francesco Spegni, Luca Spalazzi

14:30 - 15:00
Talk

Independence Abstractions and Models of Concurrency

Vijay D'SilvaGoogle Inc., Daniel KroeningUniversity of Oxford, Marcelo SousaUniversity of Oxford

15:00 - 15:30
Talk

Static Analysis of Communicating Process using Symbolic Transducers

Vincent BotbolCEA LIST + LIP6 Université Pierre & Marie Curie, Tristan Le GallCEA LIST, Emmanuel ChaillouxLIP6 - UPMC

Media Attached File Attached

16:00 - 17:30: VMCAI - Decision procedures at Amphitheater 44
Chair(s): Andreas PodelskiUniversity of Freiburg, Germany

16:00 - 16:30
Talk

Synthesising Strategy Improvement and Recursive Algorithms for Solving 2.5 Player Parity Games

Ernst Moritz HahnState Key Laboratory of Computer Science, Institute of Software, Chinese Academy of Sciences, Sven ScheweUniversity of Liverpool, Andrea TurriniState Key Laboratory of Computer Science, Institute of Software, Chinese Academy of Sciences, Lijun ZhangInstitute of Software, Chinese Academy of Sciences

File Attached

16:30 - 17:00
Talk

Reasoning in the Bernays-Schönfinkel-Ramsey Fragment of Separation Logic

Andrew ReynoldsEPFL, Radu IosifVERIMAG, CNRS, Université Grenoble-Alpes, Cristina SerbanVERIMAG, CNRS, Université Grenoble-Alpes

File Attached

17:00 - 17:30
Talk

Matching multiplications in Bit-Vector formulas

Supratik ChakrabortyIIT Bombay, Ashutosh Gupta, Rahul JainTata Institute of Fundamental Research

File Attached

Mon 16 Jan

09:00 - 10:00: VMCAI - Invited talk 2 at Amphitheater 44
Chair(s): Ahmed BouajjaniIRIF, Université Paris Diderot

09:00 - 10:00
Talk

Verified Concurrent Code: Tricks of the Trade

Ernie CohenAmazon Web Services

10:30 - 12:00: VMCAI - Numerical domains at Amphitheater 44
Chair(s): Laure GonnordUniversity of Lyon & LIP, France

10:30 - 11:00
Talk

Sound Bit-Precise Numerical Domains

Tushar SharmaUniversity of Wisconsin - Madison, USA, Thomas RepsUniversity of Wisconsin - Madison and Grammatech Inc.

File Attached

11:00 - 11:30
Talk

Efficient Elimination of Redundancies in Polyhedra using Raytracing

Alexandre Maréchal, Michael Perin

Media Attached File Attached

11:30 - 12:00
Talk

Finding Relevant Templates via the Principal Component Analysis

Yassamine SeladjiUniversity of Tlemcen

File Attached

14:00 - 15:30: VMCAI - Model-checking and bug finding at Amphitheater 44
Chair(s): Andreas PodelskiUniversity of Freiburg, Germany

14:00 - 14:30
Talk

Effective Bug Finding in C Programs with Shape and Effect Abstraction

Iago AbalIT University of Copenhagen, Claus BrabrandIT University of Copenhagen, Denmark, Andrzej WąsowskiIT University of Copenhagen, Denmark

14:30 - 15:00
Talk

Reduction of Workflow Nets for Generalised Soundness Verification

Hadrien BrideFemto-ST / Université de Franche-Comté, Olga KouchnarenkoFemto-ST / Université de Franche-Comté, Fabien PeureuxFemto-ST / Université de Franche-Comté + Smartesting S&S

Media Attached

15:00 - 15:30
Talk

Dynamic Reductions for Model Checking Concurrent Software.

Henning GüntherTechnische Universität Wien, Alfons LaarmanVienna University of Technology, Ana SokolovaUniversity of Salzburg, Georg WeissenbacherTechnische Universität Wien

File Attached

16:00 - 17:30: VMCAI - Symbolic analysis and invariant synthesis at Amphitheater 44
Chair(s): Constantin EneaLIAFA, Université Paris Diderot

16:00 - 16:30
Talk

Block-wise abstract interpretation by combining abstract domains with SMT

Jiahong Jiang, Liqian Chen, Xueguang Wu, Ji Wang

16:30 - 17:00
Talk

IC3 - Flipping the E in ICE

Yakir Vizel, Arie GurfinkelUniversity of Waterloo, Sharon ShohamTel Aviv university, Sharad MalikPrinceton University

17:00 - 17:30
Talk

Counterexample Validation and Interpolation-Based Refinement for Forest Automata

Lukas Holik, Martin HruskaBrno University of Technology , Ondrej LengalBrno University of Technology , Adam RogalewiczBrno University of Technology , Tomas VojnarBrno University of Technology

19:30 - 22:00: VMCAI - Banquet at Procope

Tue 17 Jan

09:00 - 10:00: VMCAI - Invited talk 3 at Amphitheater 44
Chair(s): Andreas PodelskiUniversity of Freiburg, Germany

09:00 - 10:00
Talk

Verification of Cancer Programs

Jasmin FisherMicrosoft Research

10:30 - 12:00: VMCAI - Model Checking and Synthesis at Amphitheater 44
Chair(s): Ahmed BouajjaniIRIF, Université Paris Diderot

10:30 - 11:00
Talk

Reachability for dynamic parametric processes

Anca MuschollUniversité de Bordeaux / LaBRI, Helmut SeidlTechnische Universität München, Igor WalukiewiczCNRS, LaBRI

11:00 - 11:30
Talk

Synthesizing Non-Vacuous Systems

Roderick BloemInstitute of Software Technology, Graz University of Technology , Hana Chockler, Masoud EbrahimiInstitute of Applied Information Processing and Communications, Graz University of Technology, Ofer StrichmanTechnion

File Attached

11:30 - 12:00
Talk

Solving Nonlinear Integer Arithmetic with MCSat

Dejan JovanovićSRI International

14:00 - 15:30: VMCAI - Abstract Interpretation at Amphitheater 44
Chair(s): Roberto GiacobazziUniversity of Verona, Italy

14:00 - 14:30
Talk

Complete Abstractions and Subclassical Modal Logics

Vijay D'SilvaGoogle, Marcelo SousaUniversity of Oxford

14:30 - 15:00
Talk

Structuring Abstract Interpreters through State and Value Abstractions

David BühlerCEA LIST, Boris YakobowskiCEA - LIST, Sandrine BlazyUniversity of Rennes 1, France

Media Attached

15:00 - 15:30
Talk

Conjunctive Abstract Interpretation using Paramodulation

Mooly SagivTel Aviv University, Or OzeriTel Aviv university, Oded PadonTel Aviv University, Noam RinetzkyTel Aviv University

Media Attached

16:00 - 17:30: VMCAI - Concurrency 2 at Amphitheater 44
Chair(s): David MonniauxCNRS, VERIMAG

16:00 - 16:30
Talk

Using Abstract Interpretation to Correct Synchronization Faults

Pietro FerraraIBM Research, Omer TrippIBM Thomas J. Watson Research Center, Peng LiuPurdue University, Eric KoskinenYale University

16:30 - 17:00
Talk

Detecting All High-Level Dataraces in an RTOS Kernel.

Suvam MukherjeeIndian Institute of Science, Arunkumar SIndian Institute of Science, Deepak D'Souza

17:00 - 17:30
Talk

Precise Thread-Modular Abstract Interpretation of Concurrent Programs using Relational Interference Abstractions

Raphaël MonatEcole Normale Supérieure de Lyon, Antoine MinéUPMC, France

Sun 15 Jan 2017


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
Amphitheater 44	VMCAI Invited talk 1 09:00 - 10:00																		VMCAI Program Analysis 10:30 - 12:00																																										VMCAI Concurrency 1 14:00 - 15:30																								VMCAI Decision procedures 16:00 - 17:30

Mon 16 Jan 2017


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	21:00	30	22:00	30
Amphitheater 44	VMCAI Invited talk 2 09:00 - 10:00			VMCAI Numerical domains 10:30 - 12:00							VMCAI Model-checking and bug finding 14:00 - 15:30					VMCAI Symbolic analysis and invariant synthesis 16:00 - 17:30
Procope												VMCAI Banquet 19:30 - 22:00

Tue 17 Jan 2017


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
Amphitheater 44	VMCAI Invited talk 3 09:00 - 10:00																		VMCAI Model Checking and Synthesis 10:30 - 12:00																																										VMCAI Abstract Interpretation 14:00 - 15:30																								VMCAI Concurrency 2 16:00 - 17:30

Sun 15 Jan 2017


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
Amphitheater 44	VMCAI 2017 Detecting Strict Aliasing Violations in the Wild 09:00 - 10:00																		VMCAI 2017 Partitioned Memory Models for Program Analysis. 10:30 - 11:00						VMCAI 2017 Property Directed Reachability for Proving Absence of Concurrent Modifi ... 11:00 - 11:30						VMCAI 2017 Stabilizing Floating-Point Programs using Provenance Analysis 11:30 - 12:00																														VMCAI 2017 Accuracy of Message Counting Abstraction in Fault-Tolerant Distributed ... 14:00 - 14:30						VMCAI 2017 Independence Abstractions and Models of Concurrency 14:30 - 15:00						VMCAI 2017 Static Analysis of Communicating Process using Symbolic Transducers 15:00 - 15:30												VMCAI 2017 Synthesising Strategy Improvement and Recursive Algorithms for Solving ... 16:00 - 16:30						VMCAI 2017 Reasoning in the Bernays-Schönfinkel-Ramsey Fragment of Separation Logic 16:30 - 17:00						VMCAI 2017 Matching multiplications in Bit-Vector formulas 17:00 - 17:30

Mon 16 Jan 2017


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
Amphitheater 44	VMCAI 2017 Verified Concurrent Code: Tricks of the Trade 09:00 - 10:00																		VMCAI 2017 Sound Bit-Precise Numerical Domains 10:30 - 11:00						VMCAI 2017 Efficient Elimination of Redundancies in Polyhedra using Raytracing 11:00 - 11:30						VMCAI 2017 Finding Relevant Templates via the Principal Component Analysis 11:30 - 12:00																														VMCAI 2017 Effective Bug Finding in C Programs with Shape and Effect Abstraction 14:00 - 14:30						VMCAI 2017 Reduction of Workflow Nets for Generalised Soundness Verification 14:30 - 15:00						VMCAI 2017 Dynamic Reductions for Model Checking Concurrent Software. 15:00 - 15:30												VMCAI 2017 Block-wise abstract interpretation by combining abstract domains with SMT 16:00 - 16:30						VMCAI 2017 IC3 - Flipping the E in ICE 16:30 - 17:00						VMCAI 2017 Counterexample Validation and Interpolation-Based Refinement for Forest ... 17:00 - 17:30

Tue 17 Jan 2017


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
Amphitheater 44	VMCAI 2017 Verification of Cancer Programs 09:00 - 10:00																		VMCAI 2017 Reachability for dynamic parametric processes 10:30 - 11:00						VMCAI 2017 Synthesizing Non-Vacuous Systems 11:00 - 11:30						VMCAI 2017 Solving Nonlinear Integer Arithmetic with MCSat 11:30 - 12:00																														VMCAI 2017 Complete Abstractions and Subclassical Modal Logics 14:00 - 14:30						VMCAI 2017 Structuring Abstract Interpreters through State and Value Abstractions 14:30 - 15:00						VMCAI 2017 Conjunctive Abstract Interpretation using Paramodulation 15:00 - 15:30												VMCAI 2017 Using Abstract Interpretation to Correct Synchronization Faults 16:00 - 16:30						VMCAI 2017 Detecting All High-Level Dataraces in an RTOS Kernel. 16:30 - 17:00						VMCAI 2017 Precise Thread-Modular Abstract Interpretation of Concurrent Programs u ... 17:00 - 17:30

iCalendar subscription service for your personal schedule

You first need to have starred events () in order to use the iCalendar subscription service.

Currently Viewed Program

Downloads the currently viewed program (with filters applied) in iCal format

VMCAI 2017 Program

Sun 15 Jan

Mon 16 Jan

Tue 17 Jan

Sun 15 Jan 2017

VMCAI

VMCAI

VMCAI

VMCAI

Mon 16 Jan 2017

VMCAI

VMCAI

VMCAI

VMCAI

VMCAI

Tue 17 Jan 2017

VMCAI

VMCAI

VMCAI

VMCAI

Sun 15 Jan 2017

Mon 16 Jan 2017

Tue 17 Jan 2017

Tracks