|
10:30-12:30
|
TACAS: Synthesis
Room: HS1, online: link
Chair: Rupak Majumdar
- Gourav Takhar, Ramesh Karri, Christian Pilato and Subhajit Roy. HOLL: Program Synthesis for Higher Order Logic Locking
- Orna Kupferman and Noam Shenwald. The Complexity of LTL Rational Synthesis
- Kedar Namjoshi and Nisarg Patel. Synthesis of Compact Strategies for Coordination Programs
- Yi Lin, Lucas M. Tabajara and Moshe Y. Vardi. ZDD Boolean Synthesis
|
FASE: Verification Technology
Room: HS2, online: link
Chair: Heike Wehrheim
- Dirk Beyer, Sudeep Kanav and Cedric Richter. Construction of Verifier Combinations Based on Off-the-Shelf Verifiers
- Liqian Chen, Renjie Huang, Dan Luo, Chenghu Ma, Dengping Wei and Ji Wang. Estimating Worst-case Resource Usage by Resource-usage-aware Fuzzing
- Zunchen Huang and Chao Wang. Symbolic Predictive Cache Analysis for Out-of-Order Execution
- Marie-Christine Jakobs and Maik Wiesner. PEQtest: Testing Functional Equivalence
|
FoSSaCS: Program and System Analysis
Room: Interims HS1, online: link
Chair: Nathalie Bertrand
- Michael Blondin and Javier Esparza. Separators in Continuous Petri Nets
- A. R. Balasubramanian, Lucie Guillou and Chana Weil-Kennedy. Parameterized Analysis of Reconfigurable Broadcast Networks
- Georgiana Caltais, Hossein Hojjat, Mohammadreza Mousavi and Hünkar Can Tunç. DyNetKAT: An Algebra of Dynamic Networks [nominated for EASST best paper]
- Flavio Ascari, Roberto Bruni and Roberta Gori. Limits and difficulties in the design of under-approximation abstract domains
|
|
|
14:00-16:00
|
TACAS: Verification
Room: HS1, online: link
Chair: Javier Esparza
- André Greiner-Petter, Howard Cohl, Abdou Youssef, Moritz Schubotz, Avi Trost, Rajen Dey, Akiko Aizawa and Bela Gipp. Comparative Verification of the Digital Library of Mathematical Functions and Computer Algebra Systems
- Wenhao Wu, Jan Hueckelheim, Paul Hovland and Stephen Siegel. Verifying Fortran Programs with CIVL
- Arturo Amendola, Anna Becchi, Roberto Cavada, Alessandro Cimatti, Andrea Ferrando, Lorenzo Pilati, Giuseppe Scaglione, Alberto Tacchella and Marco Zamboni. NORMA: a tool for the analysis of Relay-based Railway Interlocking Systems
- Haoze Wu, Aleksandar Zeljić, Guy Katz and Clark Barrett. Efficient Neural Network Analysis with Sum-of-Infeasibilities
|
FASE: AI & Quantitative Methods
Room: HS2, online: link
Chair: Andrzej Wasowski
- Evangelos Papathomas, Themistoklis Diamantopoulos and Andreas Symeonidis. Semantic Code Search in Software Repos using Neural Machine Translation
- Sai Sathiesh Rajan, Sakshi Udeshi and Sudipta Chattopadhyay. AequeVox: Automated Fairness Testing of Speech Recognition Systems
- Saikat Dutta, Zixin Huang and Sasa Misailovic. SixthSense: Debugging Convergence Problems in Probabilistic Programs via Program Representation Learning
- Aleksandar S. Dimovski. Quantitative Program Sketching using Lifted Static Analysis
|
FoSSaCS: Temporal Logic and Processes
Room: Interims HS1, online: link
Chair: Stefan Milius
- Tobias Winkler, Christina Gehnen and Joost-Pieter Katoen. Model Checking Temporal Properties of Recursive Probabilistic Programs
- Christel Baier, Florian Funke, Jakob Piribauer and Robin Ziemek. On probability-raising causality in Markov decision processes [nominated for EATCS best paper]
- Bernd Finkbeiner, Philippe Heim and Noemi Passing. Temporal Stream Logic modulo Theories
|
FASE: Test-Comp 1
Room: HS3, online: link
Chair: Dirk Beyer
- Report.
Dirk Beyer
- CoVeriTest.
Marie-Christine Jakobs
- FuSeBMC. Kaled Alshmrany
- Legion/SymCC.
Gidon Ernst
- TestCov.
Thomas Lemberger
- VeriFuzz.
Ravindra Metta
|
|
16:30-18:00
|
TACAS: Blockchain
Room: HS1, online: link
Chair: Georgiana Caltais
- Franck Cassez, Joanne Fuller and Aditya Asgaonkar. Formal Verification of the Ethereum 2.0 Beacon Chain
- David Dill, Wolfgang Grieskamp, Junkil Park, Shaz Qadeer, Meng Xu and Emma Zhong. Fast and Reliable Formal Verification of Smart Contracts with the Move Prover [nominated for EAPLS best paper and SCP best tool paper]
- Elvira Albert, Pablo Gordillo, Alejandro Hernández-Cerezo and Albert Rubio. A Max-SMT Superoptimizer for EVM handling Memory and Storage
|
Invited tutorial: Stacey Jeffery
Quantum Algorithms
Room: Interims HS1, online: link
Chair: Lenore Zuck
|
FASE: Test-Comp 2
Room: HS3, online: link
Chair: Dirk Beyer
|