Write a Blog >>
POPL 2021
Sun 17 - Fri 22 January 2021 Online
POPL 2021 (series) / Online (How to POPL in 2021) /

Room information: VMCAI

VenueOnline (How to POPL in 2021)
Room nameVMCAI
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

Sun 17 Jan

Displayed time zone: Amsterdam, Berlin, Bern, Rome, Stockholm, Vienna change

16:00 - 17:00
Invited talkVMCAI at VMCAI
Chair(s): Yakir Vizel Technion—Israel Institute of Technology
16:00
60m
Keynote
Model Checking Hyperproperties
VMCAI
I: Bernd Finkbeiner CISPA Helmholtz Center for Information Security
Media Attached
17:00 - 17:30
HyperpropertiesVMCAI at VMCAI
Chair(s): Grigory Fedyukovich Florida State University
17:00
15m
Talk
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
15m
Talk
Decomposing Data Structure Commutativity Proofs with mn-Differencing
VMCAI
Eric Koskinen Stevens Institute of Technology, Kshitij Bansal Google
Media Attached
18:00 - 18:30
Infinite-State Systems and CompilationVMCAI at VMCAI
Chair(s): Orna Grumberg Technion – Israel Institute of Technology
18:00
15m
Talk
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
15m
Talk
A Self-Certifying Compilation Framework for WebAssembly
VMCAI
Kedar Namjoshi Nokia Bell Labs, Anton Xue University of Pennsylvania
Media Attached
18:30 - 19:30
Concurrent and Distributed SystemsVMCAI at VMCAI
Chair(s): Dana Drachsler Cohen Technion
18:30
15m
Talk
Concurrent Correctness in Vector Space
VMCAI
Christina Peterson University of Central Florida, Victor Cook University of Central Florida, Damian Dechev University of Central Florida
Media Attached
18:45
15m
Talk
Verification of Concurrent Programs Using Petri Net Unfoldings
VMCAI
Daniel Dietsch University of Freiburg, Matthias Heizmann University of Freiburg, Germany, Dominik Klumpp University of Freiburg, Mehdi Naouar University of Freiburg, Andreas Podelski University of Freiburg, Germany, Claus Schätzle University of Freiburg
Media Attached
19:00
15m
Talk
Eliminating Message Counters in Synchronous Threshold Automata
VMCAI
Ilina Stoilkovska Vienna University of Technology , Igor Konnov Informal Systems Inc, Josef Widder Informal Systems, Florian Zuleger Vienna University of Technology
Media Attached
19:15
15m
Talk
A Reduction Theorem for Randomized Distributed Algorithms under Weak Adversaries
VMCAI
Nathalie Bertrand INRIA Rennes, Marijana Lazic Technical University of Munich, Josef Widder Informal Systems
Media Attached

Mon 18 Jan

Displayed time zone: Amsterdam, Berlin, Bern, Rome, Stockholm, Vienna change

16:00 - 17:00
Invited talkVMCAI at VMCAI
Chair(s): Yakir Vizel Technion—Israel Institute of Technology
16:00
60m
Keynote
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
Abstract InterpretationVMCAI at VMCAI
Chair(s): Xavier Rival INRIA/CNRS/ENS Paris
17:00
15m
Talk
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
15m
Talk
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
Model CheckingVMCAI at VMCAI
Chair(s): James R. Wilcox University of Washington
18:00
15m
Talk
Unbounded Procedure Summaries from Bounded Environments
VMCAI
Lauren Pick Princeton University, Grigory Fedyukovich Florida State University, Aarti Gupta Princeton University
Media Attached
18:15
15m
Talk
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
Synthesis and RepairVMCAI at VMCAI
Chair(s): Aws Albarghouthi University of Wisconsin-Madison, USA
18:30
15m
Talk
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
15m
Talk
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
15m
Talk
GPURepair: Automated Repair of GPU Kernels
VMCAI
Saurabh Joshi IIT Hyderabad, Gautam Muduganti IIT Hyderabad
Media Attached

Tue 19 Jan

Displayed time zone: Amsterdam, Berlin, Bern, Rome, Stockholm, Vienna change

16:00 - 17:00
Invited talkVMCAI at VMCAI
16:00
60m
Keynote
Generative Program Analysis and Beyond: The Power of Domain-Specific Languages
VMCAI
I: Bernhard Steffen TU Dortmund, Alnis Murtovi TU Dortmund, David Schmidt Kansas State University
Media Attached
17:00 - 17:30
ApplicationsVMCAI at VMCAI
Chair(s): Rayna Dimitrova CISPA Helmholtz Center for Information Security
17:00
15m
Talk
A Synchronous Effects Logic for Temporal Verification of Pure Esterel
VMCAI
Yahui Song National University of Singapore, Wei-Ngan Chin National University of Singapore
Media Attached
17:15
15m
Talk
A Design of GPU-Based Quantitative Model Checking
VMCAI
YoungMin Kwon SUNY Korea, Eunhee Kim 2e Consulting Corp.
Media Attached
18:00 - 18:30
Case StudiesVMCAI at VMCAI
Chair(s): Roderick Bloem Institute of Software Technology, Graz University of Technology
18:00
15m
Talk
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
15m
Talk
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
Decision ProceduresVMCAI at VMCAI
Chair(s): Alexander J. Summers University of British Columbia
18:30
15m
Talk
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
15m
Talk
Incremental Search for Conflict and Unit Instances of Quantified Formulas with E-Matching
VMCAI
Jochen Hoenicke University of Freiburg, Tanja Schindler University of Freiburg
Media Attached
19:00
15m
Talk
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
15m
Talk
Compositional Satisfiability Solving in Separation Logic
VMCAI
Quang Loc Le University College London, UK
Media Attached

Sun 17 Jan

Displayed time zone: Amsterdam, Berlin, Bern, Rome, Stockholm, Vienna change

Room16:003017:003018:003019:0030
VMCAI

VMCAI

Invited talk

VMCAI

Hyperproperties

VMCAI

Infinite-State Systems and Compilation

VMCAI

Concurrent and Distributed Systems

Mon 18 Jan

Displayed time zone: Amsterdam, Berlin, Bern, Rome, Stockholm, Vienna change

Room16:003017:003018:003019:0030
VMCAI

VMCAI

Invited talk

VMCAI

Abstract Interpretation

VMCAI

Model Checking

VMCAI

Synthesis and Repair

Tue 19 Jan

Displayed time zone: Amsterdam, Berlin, Bern, Rome, Stockholm, Vienna change

Room16:003017:003018:003019:0030
VMCAI

VMCAI

Invited talk

VMCAI

Applications

VMCAI

Case Studies

VMCAI

Decision Procedures

Sun 17 Jan

Displayed time zone: Amsterdam, Berlin, Bern, Rome, Stockholm, Vienna change

Room16:0015304517:0015304518:0015304519:00153045
VMCAI
VMCAI
Model Checking Hyperproperties
16:00 - 17:00
VMCAI
Compositional Model Checking for Multi-Properties
17:00 - 17:15
VMCAI
Decomposing Data Structure Commutativity Proofs with mn-Differencing
17:15 - 17:30
VMCAI
Proving the existence of fair paths in infinite state systems
18:00 - 18:15
VMCAI
A Self-Certifying Compilation Framework for WebAssembly
18:15 - 18:30
VMCAI
Concurrent Correctness in Vector Space
18:30 - 18:45
VMCAI
Verification of Concurrent Programs Using Petri Net Unfoldings
18:45 - 19:00
VMCAI
Eliminating Message Counters in Synchronous Threshold Automata
19:00 - 19:15
VMCAI
A Reduction Theorem for Randomized Distributed Algorithms under Weak Ad ...
19:15 - 19:30

Mon 18 Jan

Displayed time zone: Amsterdam, Berlin, Bern, Rome, Stockholm, Vienna change

Room16:0015304517:0015304518:0015304519:00153045
VMCAI
VMCAI
Algebra-based Synthesis of Loops and their Invariants
16:00 - 17:00
VMCAI
Runtime Abstract Interpretation for Numerical Accuracy and Robustness
17:00 - 17:15
VMCAI
Twinning automata and regular expressions for string static analysis
17:15 - 17:30
VMCAI
Unbounded Procedure Summaries from Bounded Environments
18:00 - 18:15
VMCAI
Syntax-Guided Synthesis for Lemma Generation in Hardware Model Checking
18:15 - 18:30
VMCAI
Approximate Bit Dependency Analysis to Identify Program Synthesis Probl ...
18:30 - 18:45
VMCAI
Automated Repair of Heap-Manipulating Programs using Deductive Synthesis
18:45 - 19:00
VMCAI
GPURepair: Automated Repair of GPU Kernels
19:00 - 19:15

Tue 19 Jan

Displayed time zone: Amsterdam, Berlin, Bern, Rome, Stockholm, Vienna change

Room16:0015304517:0015304518:0015304519:00153045
VMCAI
VMCAI
Generative Program Analysis and Beyond: The Power of Domain-Specific La ...
16:00 - 17:00
VMCAI
A Synchronous Effects Logic for Temporal Verification of Pure Esterel
17:00 - 17:15
VMCAI
A Design of GPU-Based Quantitative Model Checking
17:15 - 17:30
VMCAI
Formal Semantics and Verification of Network Based Biocomputation Circuits
18:00 - 18:15
VMCAI
Netter: Probabilistic, Stateful Network Models
18:15 - 18:30
VMCAI
Deciding the Bernays-Schoenfinkel Fragment over Bounded Difference Cons ...
18:30 - 18:45
VMCAI
Incremental Search for Conflict and Unit Instances of Quantified Formul ...
18:45 - 19:00
VMCAI
On Pre- and Inprocessing for Weighted MaxSAT
19:00 - 19:15
VMCAI
Compositional Satisfiability Solving in Separation Logic
19:15 - 19:30