POPL 2022 (series) / VMCAI 2022 (series) /
VMCAI 2022 Program
This is the VMCAI 2022 program - see the full program for POPL 2022 and all affiliated events.
Filter Program
Dates
Rooms
Tracks
Badges
Your Program
Sun 16 JanDisplayed time zone: Eastern Time (US & Canada) change
Sun 16 Jan
Displayed time zone: Eastern Time (US & Canada) change
09:00 - 10:00 | |||
09:00 60mKeynote | 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 30mPaper | 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 30mPaper | 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 30mPaper | A Flow-Insensitive-Complete Program RepresentationRemote VMCAI |
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 30mPaper | 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 30mPaper | 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 | |||
15:05 30mPaper | Generalized Arrays for Stainless FramesRemote VMCAI | ||
15:35 30mPaper | NP Satisfiability for Arrays as PowersInPerson VMCAI | ||
16:05 30mPaper | 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 JanDisplayed time zone: Eastern Time (US & Canada) change
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 60mKeynote | Back to the Future: A Fresh Look at Linear Temporal LogicRemote VMCAI |
10:20 - 11:50 | |||
10:20 30mPaper | 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 30mPaper | 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 30mPaper | Scaling Up Livelock Verification for Network-on-Chip Routing AlgorithmsInPerson VMCAI |
13:30 - 14:30 | |||
13:30 30mPaper | 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 30mPaper | Bisimulations for Neural Network ReductionInPerson VMCAI Pavithra Prabhakar Kansas State University |
15:05 - 16:35 | |||
15:05 30mPaper | 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 30mPaper | Loop Verification with Invariants and ContractsRemote VMCAI Gidon Ernst Ludwig Maximilian University of Munich Pre-print | ||
16:05 30mPaper | 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 JanDisplayed time zone: Eastern Time (US & Canada) change
Tue 18 Jan
Displayed time zone: Eastern Time (US & Canada) change
09:00 - 10:00 | |||
09:00 30mPaper | 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 30mPaper | Satisfiability and Synthesis Modulo OraclesRemote VMCAI Elizabeth Polgreen University of Edinburgh, Andrew Reynolds University of Iowa, Sanjit Seshia UC Berkeley |
10:20 - 11:50 | |||
10:20 30mPaper | 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 30mPaper | 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 30mPaper | 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 60mKeynote | Simplifying Concurrent Programming via Synchronization SynthesisRemote VMCAI Işıl Dillig University of Texas at Austin |
15:05 - 16:05 | |||
15:05 30mPaper | Fast Three-Valued Abstract Bit-Vector ArithmeticInPerson VMCAI | ||
15:35 30mPaper | 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 |