TACAS 2022 accepted papers

Gourav Takhar, Ramesh Karri, Christian Pilato and Subhajit Roy. HOLL: Program Synthesis for Higher Order Logic Locking
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
Steffan Sølvsten, Jaco van de Pol, Anna Blume Jakobsen and Mathias Weller Berg Thomasen. Adiar: Binary Decision Diagrams in External Memory
Dirk Beyer and Sudeep Kanav. CoVeriTeam: On-Demand Composition of Cooperative Verification Systems
Nicolas Amat, Silvano Dal Zilio and Thomas Hujsa. Property Directed Reachability for Generalized Petri Nets
Jonas Krämer, Lionel Blatter, Eva Darulova and Mattias Ulbrich. Inferring Interval-Valued Floating-Point Preconditions
Ji Guan and Nengkun Yu. A Probabilistic Logic for Verifying Continuous-time Markov Chains
Haoze Wu, Aleksandar Zeljić, Guy Katz and Clark Barrett. Efficient Neural Network Analysis with Sum-of-Infeasibilities
Luca Bortolussi, Giuseppe Maria Gallo, Jan Kretinsky and Laura Nenzi. Learning Model Checking and the Kernel Trick for Signal Temporal Logic on Stochastic Processes
Yi Lin, Lucas M. Tabajara and Moshe Y. Vardi. ZDD Boolean Synthesis
Franck Cassez, Joanne Fuller and Aditya Asgaonkar. Formal Verification of the Ethereum 2.0 Beacon Chain
Lei Shi, Yuepeng Wang, Boon Thau Loo and Rajeev Alur. Automatic Repair for Network Programs
Fabian Birkmann, Hans-Peter Deifel and Stefan Milius. Distributed Coalgebraic Partition Refinement
Frits Vaandrager, Bharat Garhewal, Jurriaan Rot and Thorsten Wissmann. A New Approach for Active Automata Learning Based on Apartness
Vojtěch Havlena, Ondrej Lengal and Barbora Šmahlíková. Sky Is Not the Limit: Tighter Rank Bounds for Elevator Automata in Büchi Automata Complementation
Véronique Bruyère, Guillermo Pérez and Gaëtan Staquet. Learning Realtime One-Counter Automata
Ritam Raha, Rajarshi Roy, Nathanaël Fijalkow and Daniel Neider. Scalable Anytime Algorithms for Learning Formulas in Linear Temporal Logic
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
Haniel Barbosa, Clark Barrett, Martin Brain, Gereon Kremer, Hanna Lachnitt, Makai Mann, Abdalrhman Mohamed, Mudathir Mohamed, Aina Niemetz, Andres Noetzli, Alex Ozdemir, Mathias Preiner, Andrew Reynolds, Ying Sheng, Cesare Tinelli and Yoni Zohar. cvc5: A Versatile and Industrial-Strength SMT Solver
Orna Kupferman and Noam Shenwald. The Complexity of LTL Rational Synthesis
Ömer Şakar, Mohsen Safari, Marieke Huisman and Anton Wijs. Alpinist: an Annotation-Aware GPU Program Optimizer
Kedar Namjoshi and Nisarg Patel. Synthesis of Compact Strategies for Coordination Programs
Randal Bryant, Armin Biere and Marijn Heule. Clausal Proofs for Pseudo-Boolean Reasoning
Martin Blicha, Grigory Fedyukovich, Antti Hyvärinen and Natasha Sharygina. Transition Power Abstractions for Deep Counterexample Detection
Elvira Albert, Pablo Gordillo, Alejandro Hernández-Cerezo and Albert Rubio. A Max-SMT Superoptimizer for EVM handling Memory and Storage
Keigo Imai, Julien Lange and Rumyana Neykova. Kmclib: Automated Inference and Verification of Session Types from OCaml Programs
Tamajit Banerjee, Majumdar Rupak, Mallik Kaushik, Anne-Kathrin Schmuck and Sadegh Soudjani. A Direct Symbolic Algorithm for Solving Stochastic Rabin Games
Alexander Bork, Joost-Pieter Katoen and Tim Quatmann. Under-Approximating Expected Total Rewards in POMDPs
Joseph Reeves, Marijn Heule and Randal Bryant. Moving Definition Variables in Quantified Boolean Formulas
Maurice Laveaux, Wieger Wesselink and Tim Willemse. On-The-Fly Solving for Symbolic Parity Games
Antonio Casares, Alexandre Duret-Lutz, Klara J. Meyer, Florian Renkin and Salomon Sickert. Practical Applications of the Alternating Cycle Decomposition
Vasileios Koutavas, Yu-Yang Lin and Nikos Tzevelekos. From Bounded Checking to Verification of Equivalence via Symbolic Up-to Techniques
Brandon Paulsen and Chao Wang. LinSyn: Synthesizing Tight Linear Bounds for Arbitrary Neural Network Activation Functions
Dawei Sun and Sayan Mitra. NeuReach: Learning Reachability Functions from Simulations
Pu Yi, Hao Wang, Tao Xie, Darko Marinov and Wing Lam. A Theoretical Analysis of Random Regression Test Prioritization
Ivan Perez, Anastasia Mavridou, Tom Pressburger, Alwyn Goodloe and Dimitra Giannakopoulou. Automated Translation of Natural Language Requirements to Runtime Monitors
Luciano Putruele, Ramiro Demasi, Pablo Castro and Pedro R. D'Argenio. MaskD: A Tool for Measuring Masking Fault-Tolerance
Arnd Hartmanns. Correct Probabilistic Model Checking with Floating-Point Arithmetic
Aleksandar Chakarov, Aleksandr Fedchin, Zvonimir Rakamarić and Neha Rungta. Better Counterexamples for Dafny
Wenhao Wu, Jan Hueckelheim, Paul Hovland and Stephen Siegel. Verifying Fortran Programs with CIVL
Martin Bromberger, Irina Dragoste, Rasha Faqeh, Christof Fetzer, Larry González, Markus Krötzsch, Maximilian Marx, Harish K Murali and Christoph Weidenbach. A Sorted Datalog Hammer for Supervisor Verification Conditions Modulo Simple Linear Arithmetic
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
Jason Koenig, Oded Padon, Sharon Shoham and Alex Aiken. Inferring Invariants with Quantifier Alternations: Taming the Search Space Explosion
Simon Guilloud and Viktor Kunčak. Equivalence Checking for Orthocomplemented Bisemilattices in Log-Linear Time
Alnis Murtovi, Alexander Bainczyk and Bernhard Steffen. Forest GUMP: A Tool for Explanation
Sheila Zingg, Srdjan Krstic, Martin Raszyk, Joshua Schneider and Dmitriy Traytel. Verified First-Order Monitoring with Recursive Rules
Marco Bozzano, Alessandro Cimatti, Alberto Griggio and Martin Jonáš. Efficient Analysis of Cyclic Redundancy Architectures via Boolean Fault Propagation
Marta Kwiatkowska, Gethin Norman, David Parker and Gabriel Santos. Correlated Equilibria and Fairness in Concurrent Stochastic Games
Marco Bozzano, Alessandro Cimatti, Stefano Tonetta and Viktória Vozárová. Searching for Ribbon-Shaped Paths in Fair Transition Systems
Ilia Zlatkin and Grigory Fedyukovich. Maximizing Branch Coverage with Constrained Horn Clauses