Write a Blog >>
VenueJW Marriott New Orleans
Room nameSt Jerome
Floor3
Room InformationNo extra information available
Program

You're viewing the program in a time zone which is different from your device's time zone - change time zone

Conference Day
Sun 19 Jan

Displayed time zone: Saskatchewan, Central America change

09:00 - 10:00
Invited 1VMCAI at St Jerome
Chair(s): Dirk BeyerLMU Munich
09:00
60m
Talk
The Siren Song of Temporal Synthesis
VMCAI
Moshe VardiRice University
10:30 - 12:30
Papers 1VMCAI at St Jerome
Chair(s): Natasha SharyginaUSI Lugano, Switzerland
10:30
30m
Talk
Witnessing Secure Compilation
VMCAI
Kedar NamjoshiBell Labs, Nokia, Lucas M. TabajaraRice University
11:00
30m
Talk
BackFlow: Backward Context-sensitive Flow Reconstruction of Taint Analysis Results
VMCAI
Pietro FerraraUniversità Ca' Foscari, Venezia, Italy, Luca OlivieriJuliaSoft SRL, Fausto SpotoU. Verona
11:30
30m
Coffee break
Mini Break
VMCAI

12:00
30m
Talk
Fixing Code That Explodes Under Symbolic Evaluation
VMCAI
Sorawee PorncharoenwaseUniversity of Washington, James BornholtUniversity of Texas at Austin, Emina TorlakUniversity of Washington
14:00 - 15:05
Invited 2VMCAI at St Jerome
Chair(s): Damien ZuffereyMPI-SWS
14:00
65m
Talk
Safety and Robustness for Deep Learning with Provable Guarantees
VMCAI
Marta KwiatkowskaUniversity of Oxford
15:35 - 17:45
Papers 2VMCAI at St Jerome
Chair(s): Kedar NamjoshiBell Labs, Nokia
15:35
32m
Talk
The Correctness of a Code Generator for a Functional Language
VMCAI
Nathanaël CourantINRIA, Antoine SereEcole Polytechnique, Natarajan ShankarSRI International, USA
16:07
32m
Talk
Leveraging Compiler Intermediate Representation for Multi- and Cross-Language Verification
VMCAI
Jack GarzellaUniversity of Utah, Marek S. BaranowskiUniversity of Utah, Shaobo HeUniversity of Utah, Zvonimir RakamaricUniversity of Utah
16:40
32m
Coffee break
Mini Break
VMCAI

17:12
32m
Talk
Putting the Squeeze on Array Programs: Loop Verification via Inductive Rank Reduction
VMCAI
Oren Ish-ShalomTel Aviv University, Israel, Shachar ItzhakyTechnion, Israel, Noam RinetzkyTel Aviv University, Sharon ShohamTel Aviv university

Conference Day
Mon 20 Jan

Displayed time zone: Saskatchewan, Central America change

09:00 - 10:00
Invited 3VMCAI at St Jerome
Chair(s): Damien ZuffereyMPI-SWS
09:00
60m
Talk
Model Checking for Safe Autonomy
VMCAI
Rajeev AlurUniversity of Pennsylvania
10:30 - 12:30
Papers 3VMCAI at St Jerome
Chair(s): Dirk BeyerLMU Munich
10:30
30m
Research paper
A Systematic Approach to Abstract Interpretation of Program Transformations
VMCAI
Sven KeidelJGU Mainz, Sebastian ErdwegJGU Mainz
Pre-print
11:00
30m
Talk
Sharing Ghost Variables in a Collection of Abstract Domains
VMCAI
Marc ChevalierENS, CNRS, PSL University, INRIA, Jerome FeretINRIA Paris
11:30
30m
Coffee break
Mini Break
VMCAI

12:00
30m
Talk
Harnessing Static Analysis to Help Learn Pseudo-Inverses of String Manipulating Procedures for Automatic Test Generation
VMCAI
Oren Ish-ShalomTel Aviv University, Israel, Shachar ItzhakyTechnion, Israel, Roman ManevichMellanox Technologies, Noam RinetzkyTel Aviv University
14:00 - 15:05
Papers 4VMCAI at St Jerome
Chair(s): Ruzica PiskacYale University, USA
14:00
32m
Talk
Synthesizing Environment Invariants for Modular Hardware Verification
VMCAI
Hongce ZhangPrinceton University, Weikun YangPrinceton University, Grigory FedyukovichFlorida State University, Aarti GuptaPrinceton University, Sharad MalikPrinceton University
14:32
32m
Talk
Systematic Classification of Attackers via Bounded Model Checking
VMCAI
Eric Rothstein-MorrisSingapore University of Technology and Design, Jun SunSingapore Management University, Singapore, Sudipta ChattopadhyaySingapore University of Technology and Design
15:35 - 17:45
Papers 5VMCAI at St Jerome
Chair(s): Nikolaj BjørnerMicrosoft Research
15:35
32m
Talk
Cheap CTL Compassion in NuSMV
VMCAI
Daniel HausmannFriedrich-Alexander-Universität Erlangen-Nürnberg, Tadeusz LitakFAU Erlangen-Nuremberg, INF 8, Christoph RauchFAU Erlangen-Nürnberg, Lehrstuhl 8, Matthias ZinnerFAU Erlangen-Nürnberg
16:07
32m
Talk
A Cooperative Parallelization Approach for Property-Directed k-Induction
VMCAI
Martin BlichaUniversità della Svizzera italiana, Antti HyvärinenUniversità della Svizzera Italiana, Matteo MarescottiUniversità della Svizzera Italiana, Natasha SharyginaUSI Lugano, Switzerland
16:40
32m
Coffee break
Mini Break
VMCAI

17:12
32m
Talk
Generalized Property-Directed Reachability for Hybrid Systems
VMCAI
Kohei SuenagaGraduate School of Informatics, Kyoto University, Takuya IshizawaKyoto University
Link to publication Pre-print

Conference Day
Tue 21 Jan

Displayed time zone: Saskatchewan, Central America change

09:00 - 10:00
Papers 6VMCAI at St Jerome
Chair(s): Andreas PodelskiUniversity of Freiburg, Germany
09:00
30m
Talk
How to Win First-Order Safety Games
VMCAI
Helmut SeidlTechnische Universität München, Christian MüllerTechnical University of Munich, Bernd FinkbeinerSaarland University
09:30
30m
Talk
Improving Parity Game Solvers with Justifications
VMCAI
Ruben LapauwKatholieke Universiteit Leuven, Maurice BruynoogheKatholieke Universiteit Leuven, Marc DeneckerKatholieke Universiteit Leuven
10:30 - 12:30
Papers 7VMCAI at St Jerome
Chair(s): Thomas WiesNew York University
10:30
30m
Talk
Language Inclusion for Finite Prime Event Structures
VMCAI
Andreas FellnerAIT - Austrian Institute of Technology, Thorsten TarrachAustrian Institute of Technology, Georg WeissenbacherTechnische Universität Wien
11:00
30m
Talk
Promptness and Bounded Fairness in Concurrent and Parameterized Systems
VMCAI
Swen JacobsCISPA Helmholtz Center for Information Security, Mouhammad SakrSaarland University, Martin ZimmermannUniversity of Liverpool
11:30
30m
Coffee break
Mini Break
VMCAI

12:00
30m
Talk
Solving LIA* Using Approximations
VMCAI
Maxwell LevatichYale, Nikolaj BjørnerMicrosoft Research, Ruzica PiskacYale University, USA, Sharon ShohamTel Aviv university
14:00 - 15:05
Papers 8VMCAI at St Jerome
Chair(s): Ori LahavTel Aviv University
14:00
32m
Talk
Formalizing and Checking Multilevel Consistency
VMCAI
Ahmed BouajjaniIRIF, Université Paris Diderot, Constantin EneaIRIF, University Paris Diderot & CNRS, Madhavan MukundChennai Mathematical Institute, Gautham Shenoy RChennai Mathematical Institute, S.P. SureshChennai Mathematical Institute
14:32
32m
Talk
Practical Abstractions for Automated Verification of Shared-Memory Concurrency
VMCAI
Wytse OortwijnETH Zürich, Dilian GurovKTH Royal Institute of Technology, Marieke HuismanUniversity of Twente
15:35 - 17:45
Panel SessionVMCAI at St Jerome
Chair(s): Dirk BeyerLMU Munich
15:35
2h10m
Other
Panel "The Future of Software Verification" at VMCAI
VMCAI
Lenore ZuckUIC, Michael WhalenAmazon Web Services and the University of Minnesota, Natarajan ShankarSRI International, USA, Andreas PodelskiUniversity of Freiburg, Germany, Dirk BeyerLMU Munich

Conference Day
Thu 23 Jan

Displayed time zone: Saskatchewan, Central America change

14:00 - 15:30
SRC Finalists PresentationsStudent Research Competition at St Jerome
14:00
90m
Talk
SRC Finalists Presentations
Student Research Competition

Conference Day
Sun 19 Jan

Displayed time zone: Saskatchewan, Central America change

Room9:003010:003011:003012:003013:003014:003015:003016:003017:0030
St Jerome

Conference Day
Mon 20 Jan

Displayed time zone: Saskatchewan, Central America change

Room9:003010:003011:003012:003013:003014:003015:003016:003017:0030
St Jerome

Conference Day
Tue 21 Jan

Displayed time zone: Saskatchewan, Central America change

Room9:003010:003011:003012:003013:003014:003015:003016:003017:0030
St Jerome

Conference Day
Thu 23 Jan

Displayed time zone: Saskatchewan, Central America change

Conference Day
Thu 23 Jan

Displayed time zone: Saskatchewan, Central America change