783 papers · page 2 of 40
Synthesizing Abstract Transformers for Reduced-Product Domains
Abstract Interpretation of ReLU Neural Networks with Optimizable Polynomial Relaxations
Should We Balance? Towards Formal Verification of the Linux Kernel Scheduler
GoGuard: Efficient Static Blocking Bug Detection for Go
Verification of Programs with ADTs Using Shallow Horn Clauses
This paper considers verification of relational properties of programs over algebraic data types (ADTs) by translating programs and properties into Constrained Horn clauses (CHCs). Verification reduces to satisfiability of CHCs modulo the theory of algebraic data types, which can…
Quantitative Static Timing Analysis
Under-Approximating Memory Abstractions
Robustness Verification of Multi-label Neural Network Classifiers
An Order Theory Framework of Recurrence Equations for Static Cost Analysis - Dynamic Inference of Non-Linear Inequality Invariants
Fixing Latent Unsound Abstract Operators in the eBPF Verifier of the Linux Kernel
ConstraintFlow: A Declarative DSL for Easy Development of DNN Certifiers
BinSub: The Simple Essence of Polymorphic Type Inference for Machine Code
Verifying Components of Arm® Confidential Computing Architecture with ESBMC
Modular Optimization-Based Roundoff Error Analysis of Floating-Point Programs
Unconstrained Variable Oracles for Faster Numeric Static Analyses
Symbolic Transformation of Expressions in Modular Arithmetic
A Formal Framework to Measure the Incompleteness of Abstract Interpretations
BREWasm: A General Static Binary Rewriting Framework for WebAssembly
Quantum Constant Propagation
Abstract A quantum circuit is often executed on the initial state where each qubit is in the zero state. Therefore, we propose to perform a symbolic execution of the circuit. Our approach simulates groups of entangled qubits exactly up to a given complexity. Here, the complexity …