Write a Blog >>
POPL 2021
Sun 17 - Fri 22 January 2021 Online
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

Conference Day
Sun 17 Jan

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

16:00 - 17:00
Invited talkVMCAI at VMCAI
Chair(s): Yakir VizelTechnion—Israel Institute of Technology
16:00
60m
Keynote
Model Checking Hyperproperties
VMCAI
I: Bernd FinkbeinerCISPA Helmholtz Center for Information Security
Media Attached
17:00 - 17:30
HyperpropertiesVMCAI at VMCAI
Chair(s): Grigory FedyukovichFlorida State University
17:00
15m
Talk
Compositional Model Checking for Multi-Properties
VMCAI
Ohad GoudsmidDepartment of Computer Science, The Technion, Orna GrumbergTechnion – Israel Institute of Technology, Sarai SheinvaldDepartment of Software Engineering, ORT Braude College of Engineering
Media Attached
17:15
15m
Talk
Decomposing Data Structure Commutativity Proofs with mn-Differencing
VMCAI
Eric KoskinenStevens Institute of Technology, Kshitij BansalGoogle
Media Attached
18:00 - 18:30
Infinite-State Systems and CompilationVMCAI at VMCAI
Chair(s): Orna GrumbergTechnion – Israel Institute of Technology
18:00
15m
Talk
Proving the existence of fair paths in infinite state systems
VMCAI
Enrico MagnagoFondazione Bruno Kessler, Alberto GriggioFondazione Bruno Kessler, Alessandro CimattiFondazione Bruno Kessler
Media Attached
18:15
15m
Talk
A Self-Certifying Compilation Framework for WebAssembly
VMCAI
Kedar NamjoshiNokia Bell Labs, Anton XueUniversity of Pennsylvania
Media Attached
18:30 - 19:30
Concurrent and Distributed SystemsVMCAI at VMCAI
Chair(s): Dana Drachsler CohenTechnion
18:30
15m
Talk
Concurrent Correctness in Vector Space
VMCAI
Christina PetersonUniversity of Central Florida, Victor CookUniversity of Central Florida, Damian DechevUniversity of Central Florida
Media Attached
18:45
15m
Talk
Verification of Concurrent Programs Using Petri Net Unfoldings
VMCAI
Daniel DietschUniversity of Freiburg, Matthias HeizmannUniversity of Freiburg, Germany, Dominik KlumppUniversity of Freiburg, Mehdi NaouarUniversity of Freiburg, Andreas PodelskiUniversity of Freiburg, Germany, Claus SchätzleUniversity of Freiburg
Media Attached
19:00
15m
Talk
Eliminating Message Counters in Synchronous Threshold Automata
VMCAI
Ilina StoilkovskaVienna University of Technology , Igor KonnovInformal Systems Inc, Josef WidderInformal Systems, Florian ZulegerVienna University of Technology
Media Attached
19:15
15m
Talk
A Reduction Theorem for Randomized Distributed Algorithms under Weak Adversaries
VMCAI
Nathalie BertrandINRIA Rennes, Marijana LazicTechnical University of Munich, Josef WidderInformal Systems
Media Attached

Conference Day
Mon 18 Jan

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

16:00 - 17:00
Invited talkVMCAI at VMCAI
Chair(s): Yakir VizelTechnion—Israel Institute of Technology
16:00
60m
Keynote
Algebra-based Synthesis of Loops and their Invariants
VMCAI
I: Laura KovacsVienna University of Technology (TU Wien), Andreas HumenbergerVienna University of Technology
Media Attached
17:00 - 17:30
Abstract InterpretationVMCAI at VMCAI
Chair(s): Xavier RivalINRIA/CNRS/ENS Paris
17:00
15m
Talk
Runtime Abstract Interpretation for Numerical Accuracy and Robustness
VMCAI
Franck VédrineCEA LIST, Maxime JacqueminCEA LIST, France, Nikolai KosmatovThales Research and Technology, Julien SignolesCEA LIST
Media Attached
17:15
15m
Talk
Twinning automata and regular expressions for string static analysis
VMCAI
Luca NegriniCa’ Foscari University of Venice, Julia S.r.l., Vincenzo ArceriCa’ Foscari University of Venice, Pietro FerraraUniversità Ca' Foscari, Venezia, Italy, Agostino CortesiUniversità Ca' Foscari Venezia
Media Attached
18:00 - 18:30
Model CheckingVMCAI at VMCAI
Chair(s): James R. WilcoxUniversity of Washington
18:00
15m
Talk
Unbounded Procedure Summaries from Bounded Environments
VMCAI
Lauren PickPrinceton University, Grigory FedyukovichFlorida State University, Aarti GuptaPrinceton University
Media Attached
18:15
15m
Talk
Syntax-Guided Synthesis for Lemma Generation in Hardware Model Checking
VMCAI
Hongce ZhangPrinceton University, Aarti GuptaPrinceton University, Sharad MalikPrinceton University
Media Attached
18:30 - 19:15
Synthesis and RepairVMCAI at VMCAI
Chair(s): Aws AlbarghouthiUniversity of Wisconsin-Madison, USA
18:30
15m
Talk
Approximate Bit Dependency Analysis to Identify Program Synthesis Problems as Infeasible
VMCAI
Marius KampFriedrich-Alexander University Erlangen-Nürnberg, Michael PhilippsenFriedrich-Alexander University Erlangen-Nürnberg (FAU)
Media Attached
18:45
15m
Talk
Automated Repair of Heap-Manipulating Programs using Deductive Synthesis
VMCAI
Thanh-Toan NguyenNational University of Singapore, Quang-Trung TaNational University of Singapore, Ilya SergeyYale-NUS College and National University of Singapore, Wei-Ngan ChinNational University of Singapore
Media Attached
19:00
15m
Talk
GPURepair: Automated Repair of GPU Kernels
VMCAI
Saurabh JoshiIIT Hyderabad, Gautam MudugantiIIT Hyderabad
Media Attached

Conference Day
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 SteffenTU Dortmund, Alnis MurtoviTU Dortmund, David SchmidtKansas State University
Media Attached
17:00 - 17:30
ApplicationsVMCAI at VMCAI
Chair(s): Rayna DimitrovaCISPA Helmholtz Center for Information Security
17:00
15m
Talk
A Synchronous Effects Logic for Temporal Verification of Pure Esterel
VMCAI
Yahui SongNational University of Singapore, Wei-Ngan ChinNational University of Singapore
Media Attached
17:15
15m
Talk
A Design of GPU-Based Quantitative Model Checking
VMCAI
YoungMin KwonSUNY Korea, Eunhee Kim2e Consulting Corp.
Media Attached
18:00 - 18:30
Case StudiesVMCAI at VMCAI
Chair(s): Roderick BloemInstitute of Software Technology, Graz University of Technology
18:00
15m
Talk
Formal Semantics and Verification of Network Based Biocomputation Circuits
VMCAI
Michelle Aluf-MedinaBar Ilan University, Till KortenTU Dresden, Avraham RavivBar Ilan University, Dan Nicolau Jr.Molecular Sense, Hillel KuglerBar Ilan University
Media Attached
18:15
15m
Talk
Netter: Probabilistic, Stateful Network Models
VMCAI
Han ZhangCarnegie Mellon University, Chi Zhang, Arthur Azevedo de AmorimCarnegie Mellon University, USA, Yuvraj AgarwalCarnegie Mellon University, Matt FredriksonCarnegie Mellon University, Limin JiaCarnegie Mellon University
Media Attached
18:30 - 19:30
Decision ProceduresVMCAI at VMCAI
Chair(s): Alexander J. SummersUniversity of British Columbia
18:30
15m
Talk
Deciding the Bernays-Schoenfinkel Fragment over Bounded Difference Constraints by Simple Clause Learning over Theories
VMCAI
Martin BrombergerMPI-INF, Alberto FioriMax Planck Institute for Informatics, Christoph WeidenbachMPI-INF
Media Attached
18:45
15m
Talk
Incremental Search for Conflict and Unit Instances of Quantified Formulas with E-Matching
VMCAI
Jochen HoenickeUniversity of Freiburg, Tanja SchindlerUniversity of Freiburg
Media Attached
19:00
15m
Talk
On Pre- and Inprocessing for Weighted MaxSAT
VMCAI
Tobias PaxianUniversity of Freiburg, Pascal RaiolaUniversity of Freiburg, Bernd BeckerAlbert-Ludwigs-University Freiburg
Media Attached
19:15
15m
Talk
Compositional Satisfiability Solving in Separation Logic
VMCAI
Quang Loc LeUniversity College London, UK
Media Attached

Conference Day
Sun 17 Jan

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

Conference Day
Mon 18 Jan

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

Conference Day
Tue 19 Jan

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