Fast and Efficient Bit-Level Precision Tuning.- Backward Symbolic Execution with Loop Folding.- Accelerating Program Analyses in Datalog by Merging Library Facts.- Abstract Interpretation.- Verified Functional Programming of an Abstract Interpreter.- Disjunctive Interval Analysis.- Static analysis of ReLU neural networks with tropical polyhedral.- Exploiting Verified Neural Networks via Floating Point Numerical Error.-Verifying Low-dimensional Input Neural Networks via Input Quantization.- Data Abstraction: A General Framework to Handle Program.- Verification of Data Structures.- Toward Neural-Network-Guided Program Synthesis and Verification.- Selective Context-Sensitivity for k-CFA with CFL-Reachability.- Selectively-Amortized Resource Bounding.- Reduced Products of Abstract Domains for Fairness Certification of Neural Networks.- A Multi-Language Static Analysis of Python Programs with Native C Extensions.- Automated Verification of the Parallel Bellman-Ford Algorithm.- Improving Thread-Modular Abstract Interpretation.- Thread-modular Analysis of Release-Acquire Concurrency.- Symbolic Automatic Relations and Their Applications to SMT and CHC Solving.- Compositional Verification of Smart Contracts Through Communication Abstraction.- Automatic Synthesis of Data-Flow Analyzer.