E-raamat: Tools and Algorithms for the Construction and Analysis of Systems: 28th International Conference, TACAS 2022, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2022, Munich, Germany, April 2-7, 2022, Proceedings, Part I

Synthesis.- HOLL: Program Synthesis for Higher Order Logic Locking.- The Complexity of LTL Rational Synthesis.- Synthesis of Compact Strategies for Coordination Programs.- ZDD Boolean Synthesis.- Verification.- Comparative Verification of the Digital Library of Mathematical.- Functions and Computer Algebra Systems.- Verifying Fortran Programs with CIVL.- NORMA: a tool for the analysis of Relay-based Railway Interlocking Systems.- Efficient Neural Network Analysis with Sum-of-Infeasibilities.- Blockchain.- Formal Verification of the Ethereum 2.0 Beacon Chain.- Fast and Reliable Formal Verification of Smart Contracts with the Move Prover.- A Max-SMT Superoptimizer for EVM handling Memory and Storage.- Grammatical Inference.- A New Approach for Active Automata Learning Based on Apartness.- Learning Realtime One-Counter Automata.- Scalable Anytime Algorithms for Learning Fragments of Linear Temporal Logic.- and Daniel NeiderLearning Model Checking and the Kernel Trick for Signal Temporal Logic on Stochastic Processes.- Verification Inference.- Inferring Interval-Valued Floating-Point Preconditions.- NeuReach: Learning Reachability Functions from Simulations.- Quantifier Alternations: Taming the Search Space Explosion.- LinSyn: Synthesizing Tight Linear Bounds for Arbitrary Neural Network Activation Functions.- Short papers.- Kmclib: Automated Inference and Verification of Session Types from OCaml Programs.- Automated Translation of Natural Language Requirements to Runtime Monitors.- MaskD: A Tool for Measuring Masking Fault-Tolerance.- Better Counterexamples for Dafny.- Constraint Solving.- cvc5: A Versatile and Industrial-Strength SMT Solver.- Clausal Proofs for Pseudo-Boolean Reasoning.- Moving Definition Variables in Quantified Boolean Formulas.- A Sorted Datalog Hammer for Supervisor Verification Conditions Modulo Simple Linear Arithmetic.- Model checking and verification.- Property Directed Reachability for Generalized Petri Nets.- Transition Power Abstractions for Deep Counterexample Detection.- Searching for Ribbon-Shaped Paths in Fair Transition Systems.- CoVeriTeam: On-Demand Composition of Cooperative Verification Systems.