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

Sun 16 Jan

Displayed time zone: Eastern Time (US & Canada) change

09:00 - 10:00
Invited TalkVMCAI at Salon I
Chair(s): Thomas Wies New York University
09:00
60m
Keynote
Sequential Information FlowRemote
VMCAI
Thomas A. Henzinger IST Austria, Austria
10:20 - 11:50
Static Analysis and Abstract InterpretationVMCAI at Salon I
Chair(s): Thomas Wies New York University
10:20
30m
Paper
Relational String Abstract DomainsRemote
VMCAI
Vincenzo Arceri University of Parma - Department of Mathematical, Physical, and Computer Sciences, Martina Olliaro Ca' Foscari University of Venice - Department of Environmental Sciences, Informatics and Statistics, Agostino Cortesi Università Ca' Foscari Venezia, Pietro Ferrara Università Ca' Foscari, Venezia, Italy
10:50
30m
Paper
Lightweight Shape Analysis based on Physical TypesInPerson
VMCAI
Olivier Nicole CEA LIST, France, Matthieu Lemerre CEA LIST, France, Xavier Rival INRIA/CNRS/ENS Paris
11:20
30m
Paper
A Flow-Insensitive-Complete Program RepresentationRemote
VMCAI
Solène Mirliaz ENS Rennes / IRISA / Inria, David Pichardie Facebook Paris
13:30 - 14:30
Privacy and SecurityVMCAI at Salon I
Chair(s): Vincenzo Arceri University of Parma - Department of Mathematical, Physical, and Computer Sciences
13:30
30m
Paper
Verifying Pufferfish Privacy in Hidden Markov ModelsRemote
VMCAI
Depeng Liu Institute of Software, Chinese Academy of Sciences, Bow-Yaw Wang Academia Sinica, Lijun Zhang Institute of Software, Chinese Academy of Sciences
14:00
30m
Paper
Verifying Solidity Smart Contracts Via Communication Abstraction in SmartACERemote
VMCAI
Scott Wesley University of Waterloo, Canada, Maria Christakis MPI-SWS, Jorge A. Navas Certora, inc., Richard Trefler University of Waterloo, Canada, Valentin Wüstholz ConsenSys, Arie Gurfinkel University of Waterloo
15:05 - 16:35
Satisfiability Modulo TheoriesVMCAI at Salon I
Chair(s): Natarajan Shankar SRI International, USA
15:05
30m
Paper
Generalized Arrays for Stainless FramesRemote
VMCAI
Georg Stefan Schmid EPFL, Switzerland, Viktor Kunčak EPFL, Switzerland
15:35
30m
Paper
NP Satisfiability for Arrays as PowersInPerson
VMCAI
Rodrigo Raya EPFL, Viktor Kunčak EPFL, Switzerland
16:05
30m
Paper
Bit-Precise Reasoning via Int-BlastingRemote
VMCAI
Yoni Zohar Bar Ilan University, Ahmed Irfan Stanford University, Makai Mann Stanford University, Aina Niemetz Stanford University, Andres Nötzli Stanford University, USA, Mathias Preiner Stanford University, Andrew Reynolds University of Iowa, Clark Barrett Stanford University, Cesare Tinelli University of Iowa

Mon 17 Jan

Displayed time zone: Eastern Time (US & Canada) change

09:00 - 10:00
Invited TalkVMCAI at Salon I
Chair(s): Bernd Finkbeiner CISPA Helmholtz Center for Information Security
09:00
60m
Keynote
Back to the Future: A Fresh Look at Linear Temporal LogicRemote
VMCAI
10:20 - 11:50
Model CheckingVMCAI at Salon I
Chair(s): Arie Gurfinkel University of Waterloo
10:20
30m
Paper
Automata-Driven Partial Order Reduction and Guided Search for LTL Model CheckingRemote
VMCAI
Peter Gjøl Jensen Aalborg University, Denmark, Jiri Srba Aalborg University, Nikolaj Jensen Ulrik Aalborg University, Simon Mejlby Virenfeldt Aalborg University
10:50
30m
Paper
Stateful Dynamic Partial Order Reduction for Model Checking Event-Driven Applications that Do Not TerminateRemote
VMCAI
Rahmadi Trimananda University of California at Irvine, USA, Weiyu Luo University of California, Irvine, Brian Demsky University of California at Irvine, Harry Xu University of California, Los Angeles (UCLA)
Link to publication DOI Pre-print Media Attached File Attached
11:20
30m
Paper
Scaling Up Livelock Verification for Network-on-Chip Routing AlgorithmsInPerson
VMCAI
Landon Taylor Utah State University, Zhen Zhang Utah State University
13:30 - 14:30
Formal Methods in Machine LearningVMCAI at Salon I
Chair(s): Rupak Majumdar MPI-SWS
13:30
30m
Paper
Fanoos: Multi-Resolution, Multi-Strength, Interactive Explanations for Learned SystemsRemote
VMCAI
David Bayani Carnegie Mellon University's School of Computer Science, Stefan Mitsch Carnegie Mellon University, USA
14:00
30m
Paper
Bisimulations for Neural Network ReductionInPerson
VMCAI
Pavithra Prabhakar Kansas State University
15:05 - 16:35
Program VerificationVMCAI at Salon I
Chair(s): Elizabeth Polgreen University of Edinburgh
15:05
30m
Paper
High Assurance Software for Financial Regulation and Business PlatformsRemote
VMCAI
Stephen Goldbaum Morgan Stanley, Attila Mihaly Morgan Stanley, Tosha Ellison Fintech Open Source Foundation, Earl Barr UCL, Mark Marron Microsoft Research
15:35
30m
Paper
Loop Verification with Invariants and ContractsRemote
VMCAI
Gidon Ernst Ludwig Maximilian University of Munich
Pre-print
16:05
30m
Paper
Making PROGRESS in Property Directed ReachabilityRemote
VMCAI
Tobias Seufert University of Freiburg, Christoph Scholl University of Freiburg, Arun Chandrasekharan OneSpin Solutions, Munich, Sven Reimer OneSpin Solutions, Munich, Tobias Welp OneSpin Solutions, Munich

Tue 18 Jan

Displayed time zone: Eastern Time (US & Canada) change

09:00 - 10:00
SynthesisVMCAI at Salon I
Chair(s): Viktor Kunčak EPFL, Switzerland
09:00
30m
Paper
Gradient-Descent for Randomized Controllers under Partial ObservabilityInPerson
VMCAI
Jip Spel RWTH Aachen University, Linus Heck RWTH Aachen University, Sebastian Junges University of California, Berkeley, Joshua Moerman Open University of the Netherlands, Joost-Pieter Katoen RWTH Aachen University
09:30
30m
Paper
Satisfiability and Synthesis Modulo OraclesRemote
VMCAI
Elizabeth Polgreen University of Edinburgh, Andrew Reynolds University of Iowa, Sanjit Seshia UC Berkeley
10:20 - 11:50
Probabilistic SystemsVMCAI at Salon I
Chair(s): Pavithra Prabhakar Kansas State University
10:20
30m
Paper
Out of Control: Reducing Probabilistic Models by Control-State EliminationInPerson
VMCAI
Tobias Winkler RWTH Aachen University, Johannes Lehmann RWTH Aachen University, Joost-Pieter Katoen RWTH Aachen University
10:50
30m
Paper
STAMINA 2.0: Improving Scalability of Infinite-StateStochastic Model CheckingRemote
VMCAI
Riley Roberts Utah State University, Thakur Neupane The MathWorks, Inc., Lukas Buecherl University of Colorado, Boulder, Chris Myers University of Colorado, Boulder, Zhen Zhang Utah State University
11:20
30m
Paper
EPMC Gets Knowledge in Multi-Agent SystemsRemote
VMCAI
Chen Fu Institute of Software at Chinese Academy of Sciences; University of Chinese Academy of Sciences, Ernst Moritz Hahn University of Twente, Yong Li Institute of Software, Chinese Academy of Sciences, Sven Schewe University of Liverpool, Meng Sun Peking University, Andrea Turrini State Key Laboratory of Computer Science, Institute of Software, Chinese Academy of Sciences, Lijun Zhang Institute of Software, Chinese Academy of Sciences
13:30 - 14:30
Invited TalkVMCAI at Salon I
Chair(s): Bernd Finkbeiner CISPA Helmholtz Center for Information Security
13:30
60m
Keynote
Simplifying Concurrent Programming via Synchronization SynthesisRemote
VMCAI
Isil Dillig University of Texas at Austin
15:05 - 16:05
Static Analysis and Hybrid SystemsVMCAI at Salon I
Chair(s): Yoni Zohar Bar Ilan University
15:05
30m
Paper
Fast Three-Valued Abstract Bit-Vector ArithmeticInPerson
VMCAI
Jan Onderka Czech Technical University in Prague, Stefan Ratschan The Czech Academy of Sciences
15:35
30m
Paper
Mixed Semantics Guided Layered Bounded Reachability Analysis of Compositional Linear Hybrid AutomataRemote
VMCAI
Yuming Wu Nanjing University, Lei Bu Nanjing University, Jiawan Wang Nanjing University, Xinyue Ren Nanjing University, Wen Xiong Nanjing University, Xuandong Li Nanjing University