Assertion Checking over Combined Abstraction of Linear Arithmetic and Uninterpreted Functions
Abstract elided by the publisher.
Related papers
- Path-Sensitive Analysis for Linear Arithmetic and Uninterpreted Functions SAS 2004
- Invariant Checking of NRA Transition Systems via Incremental Reduction to LRA with EUF TACAS 2017
- ALASCA: Reasoning in Quantified Linear Arithmetic TACAS 2023
- Proof Tree Preserving Interpolation TACAS 2013
- Modeling and Verifying Systems Using a Logic of Counter Arithmetic with Lambda Expressions and Uninterpreted Functions CAV 2002
- Beyond Quantifier-Free Interpolation in Extensions of Presburger Arithmetic VMCAI 2011
- Breaking the Mold: Nonlinear Ranking Function Synthesis Without Templates CAV 2024
- What's Decidable About Program Verification Modulo Axioms? TACAS 2020