783 papers · page 1 of 40
A Programming Language for Feasible Solutions
Runtime efficiency and termination are crucial properties in the studies of program verification. Instead of dealing with these issues in an ad hoc manner, it would be useful to develop a robust framework in which such properties are guaranteed by design. This paper introduces a …
On a Simple Problem Due to Yves Bertot
Contextual Equality Saturation
. Equality saturation is a semantics-based technique for automatically and efficiently proving that two programs are equivalent modulo a fixed set of equality axioms. In this paper, we extend the equality saturation technique with contextual reasoning in order to perform rewritin…
Delta Store Semantics: Abstract Garbage Collection for Abstract Definitional Interpreters
Ductape: Optimizing Dynamically Typed Programs Using Ahead-of-Time Compilation and Data-Flow Analysis
AURA: Precise Abstract Interpretation of Probabilistic Programs with Interval Data Uncertainty
Automated Catamorphism Synthesis for Solving Constrained Horn Clauses over Algebraic Data Types
Formal Analysis of Networked PLC Controllers Interacting with Physical Environments
Verifying Neural Networks with PyRAT
Comparing the Precision of Abstract Operators in the eBPF Verifier Using Differential Synthesis
Specifying and Verifying Future Conditions
Abstracting Concolic Execution for Soft Contract Verification
Monarch: A Modular Framework for Abstract Definitional Interpreters in Haskell
Enhancing Neural Network Robustness via Synthesis of Repair Programs
Bounded-Exhaustive Subspace Diversification for SMT Solver Testing
Static Analysis of Quantum Programs
Trace Partitioning as an Optimization Problem
. Imprecision is a very common phenomenon in static analyses that results in false alarms when used for program verification. Designing automatic techniques to improve static analysis precision is an old dream, but it is highly non-trivial. In the last two decades, static analysi…