The 19th International Symposium on Automated Technology for Verification and Analysis

18 - 22 October 2021, Gold Coast (Online), Australia

List of Accepted Regular Papers

Tobias John, Simon Jantsch, Christel Baier and Sascha Klüppelholz. Determinization and Limit-determinization of Emerson-Lei automata (Best Paper Award)
Bernd Finkbeiner, Felix Klein, and Niklas Metzger. Live Synthesis
Vedad Hadžić, Robert Primas and Roderick Bloem. Proving SIFA Protection of Masked Redundant Circuits
Brae Webb, Mark Utting and Ian Hayes. A Formal Semantics of the GraalVM Intermediate Representation
Zixin Huang, Saikat Dutta and Sasa Misailovic. Aqua: Automated Quantized Inference for Probabilistic Programs
Siddharth Priya, Xiang Zhou, Yusen Su, Yakir Vizel, Yuyan Bao and Arie Gurfinkel. Verifying Verified Code
Orna Kupferman, Nir Lavee and Salomon Sickert. Certifying DFA Bounds for Recognition and Separation
Christel Baier, Florian Funke, Simon Jantsch, Jakob Piribauer and Robin Ziemek. Probabilistic causes in Markov Chains
Alessandro Cimatti, Alberto Griggio and Enrico Magnago. Automatic discovery of fair paths in infinite-state transition systems
Jean-Raphaël Gaglione, Daniel Neider, Rajarshi Roy, Ufuk Topcu and Zhe Xu. Learning Linear Temporal Properties from Noisy Data: A MaxSAT-based Approach
Bernd Finkbeiner and Noemi Passing. Compositional Synthesis of Modular Systems
Peter Gjøl Jensen, Stefan Schmid, Morten Konggaard Schou, Jiri Srba, Juan Vanerio and Ingo van Duijn. Faster Pushdown Reachability Analysis with Applications in Network Verification
Shaun Azzopardi, Nir Piterman and Gerardo Schneider. Incorporating Monitors in Reactive Synthesis without Paying the Price
Lukas Stevens and Tobias Nipkow. A Verified Decision Procedure for Orders in Isabelle/HOL
Murad Akhundov, Federico Mora, Nick Feng, Vincent Hui and Marsha Chechik. Verification by Gambling on Program Slices
Igor Khmelnitsky, Daniel Neider, Rajarshi Roy, Xuan Xie, Benoît Barbot, Benedikt Bollig, Alain Finkel, Serge Haddad, Martin Leucker and Lina Ye. Property-Directed Verification and Robustness Certification of Recurrent Neural Networks
Guillaume Dupont, Yamine Ait Ameur, Marc Pantel and Neeraj Singh. Event-B Refinement for Continuous Behaviours Approximation
Norine Coenen, Bernd Finkbeiner, Christopher Hahn, Jana Hofmann and Yannick Schillo. Runtime Enforcement of Hyperproperties
Sara Mohammadinejad, Jyotirmoy V. Deshmukh and Laura Nenzi. Mining Interpretable Spatio-temporal Logic Properties for Spatially Distributed Systems

List of Accepted Tool Papers

Stefan Pranger, Bettina Könighofer, Lukas Posch and Roderick Bloem. TEMPEST - Synthesis Tool for Reactive Systems and Shields in Probabilistic Environments
Edi Muškardin, Bernhard K. Aichernig, Ingo Pill, Martin Tappler and Andrea Pferscher. AALpy: An Active Automata Learning Library
Dirk Beyer, Karlheinz Friedberger and Stephan Holzner. PJBDD: A BDD Library for Java and Multi-Threading
Dario Guidotti, Luca Pulina and Armando Tacchella. pyNever: a Framework for Learning and Verification of Neural Networks

Official Sponsors

ATVA'21 is an outstanding opportunity for you to reach the ‘thought leaders’ in this industry with your message, and for your Software Engineering team to network and exchange ideas with their peers in this unique and innovative forum.

Sponsors are offered the opportunity to reach over 100 software engineering experts, including researchers and industry practitioners such as developers, QA and engineering managers.

New sponsorship are welcome and any entity wishing to become an official sponsor may contact the Program Co-chairs.