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 BellmanFord 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.