POPL 2021 (series) / VMCAI 2021 (series) /
VMCAI 2021 Program
This is the VMCAI 2021 program - see the full program for POPL 2021 and all affiliated events.
Filter Program
Dates
Rooms
Tracks
Badges
Your Program
Sun 17 JanDisplayed time zone: Amsterdam, Berlin, Bern, Rome, Stockholm, Vienna change
Sun 17 Jan
Displayed time zone: Amsterdam, Berlin, Bern, Rome, Stockholm, Vienna change
16:00 - 17:00 | |||
16:00 60mKeynote | Model Checking Hyperproperties VMCAI Media Attached |
17:00 - 17:30 | |||
17:00 15mTalk | Compositional Model Checking for Multi-Properties VMCAI Ohad Goudsmid Department of Computer Science, The Technion, Orna Grumberg Technion – Israel Institute of Technology, Sarai Sheinvald Department of Software Engineering, ORT Braude College of Engineering Media Attached | ||
17:15 15mTalk | Decomposing Data Structure Commutativity Proofs with mn-Differencing VMCAI Media Attached |
18:00 - 18:30 | Infinite-State Systems and CompilationVMCAI at VMCAI Chair(s): Orna Grumberg Technion – Israel Institute of Technology | ||
18:00 15mTalk | Proving the existence of fair paths in infinite state systems VMCAI Enrico Magnago Fondazione Bruno Kessler, Alberto Griggio Fondazione Bruno Kessler, Alessandro Cimatti Fondazione Bruno Kessler Media Attached | ||
18:15 15mTalk | A Self-Certifying Compilation Framework for WebAssembly VMCAI Media Attached |
Mon 18 JanDisplayed time zone: Amsterdam, Berlin, Bern, Rome, Stockholm, Vienna change
Mon 18 Jan
Displayed time zone: Amsterdam, Berlin, Bern, Rome, Stockholm, Vienna change
16:00 - 17:00 | |||
16:00 60mKeynote | Algebra-based Synthesis of Loops and their Invariants VMCAI I: Laura Kovacs Vienna University of Technology (TU Wien), Andreas Humenberger Vienna University of Technology Media Attached |
17:00 - 17:30 | |||
17:00 15mTalk | Runtime Abstract Interpretation for Numerical Accuracy and Robustness VMCAI Franck Védrine CEA LIST, Maxime Jacquemin CEA LIST, France, Nikolai Kosmatov Thales Research and Technology, Julien Signoles CEA LIST Media Attached | ||
17:15 15mTalk | Twinning automata and regular expressions for string static analysis VMCAI Luca Negrini Ca’ Foscari University of Venice, Julia S.r.l., Vincenzo Arceri Ca’ Foscari University of Venice, Pietro Ferrara Università Ca' Foscari, Venezia, Italy, Agostino Cortesi Università Ca' Foscari Venezia Media Attached |
18:00 - 18:30 | |||
18:00 15mTalk | Unbounded Procedure Summaries from Bounded Environments VMCAI Lauren Pick Princeton University, Grigory Fedyukovich Florida State University, Aarti Gupta Princeton University Media Attached | ||
18:15 15mTalk | Syntax-Guided Synthesis for Lemma Generation in Hardware Model Checking VMCAI Hongce Zhang Princeton University, Aarti Gupta Princeton University, Sharad Malik Princeton University Media Attached |
18:30 - 19:15 | |||
18:30 15mTalk | Approximate Bit Dependency Analysis to Identify Program Synthesis Problems as Infeasible VMCAI Marius Kamp Friedrich-Alexander University Erlangen-Nürnberg, Michael Philippsen Friedrich-Alexander University Erlangen-Nürnberg (FAU) Media Attached | ||
18:45 15mTalk | Automated Repair of Heap-Manipulating Programs using Deductive Synthesis VMCAI Thanh-Toan Nguyen National University of Singapore, Quang-Trung Ta National University of Singapore, Ilya Sergey Yale-NUS College and National University of Singapore, Wei-Ngan Chin National University of Singapore Media Attached | ||
19:00 15mTalk | GPURepair: Automated Repair of GPU Kernels VMCAI Media Attached |
Tue 19 JanDisplayed time zone: Amsterdam, Berlin, Bern, Rome, Stockholm, Vienna change
Tue 19 Jan
Displayed time zone: Amsterdam, Berlin, Bern, Rome, Stockholm, Vienna change
16:00 - 17:00 | |||
16:00 60mKeynote | Generative Program Analysis and Beyond: The Power of Domain-Specific Languages VMCAI Media Attached |
17:00 - 17:30 | ApplicationsVMCAI at VMCAI Chair(s): Rayna Dimitrova CISPA Helmholtz Center for Information Security | ||
17:00 15mTalk | A Synchronous Effects Logic for Temporal Verification of Pure Esterel VMCAI Media Attached | ||
17:15 15mTalk | A Design of GPU-Based Quantitative Model Checking VMCAI Media Attached |
18:00 - 18:30 | Case StudiesVMCAI at VMCAI Chair(s): Roderick Bloem Institute of Software Technology, Graz University of Technology | ||
18:00 15mTalk | Formal Semantics and Verification of Network Based Biocomputation Circuits VMCAI Michelle Aluf-Medina Bar Ilan University, Till Korten TU Dresden, Avraham Raviv Bar Ilan University, Dan Nicolau Jr. Molecular Sense, Hillel Kugler Bar Ilan University Media Attached | ||
18:15 15mTalk | Netter: Probabilistic, Stateful Network Models VMCAI Han Zhang Carnegie Mellon University, Chi Zhang CMU, Arthur Azevedo de Amorim Carnegie Mellon University, USA, Yuvraj Agarwal Carnegie Mellon University, Matt Fredrikson Carnegie Mellon University, Limin Jia Carnegie Mellon University Media Attached |
18:30 - 19:30 | |||
18:30 15mTalk | Deciding the Bernays-Schoenfinkel Fragment over Bounded Difference Constraints by Simple Clause Learning over Theories VMCAI Martin Bromberger MPI-INF, Alberto Fiori Max Planck Institute for Informatics, Christoph Weidenbach MPI-INF Media Attached | ||
18:45 15mTalk | Incremental Search for Conflict and Unit Instances of Quantified Formulas with E-Matching VMCAI Media Attached | ||
19:00 15mTalk | On Pre- and Inprocessing for Weighted MaxSAT VMCAI Tobias Paxian University of Freiburg, Pascal Raiola University of Freiburg, Bernd Becker Albert-Ludwigs-University Freiburg Media Attached | ||
19:15 15mTalk | Compositional Satisfiability Solving in Separation Logic VMCAI Quang Loc Le University College London, UK Media Attached |