Modeling and Verifying Systems Using a Logic of Counter Arithmetic with Lambda Expressions and Uninterpreted Functions
No abstract available.
DOI 10.1007/3-540-45657-0_7
Related papers
- Flat Model Checking for Counting LTL Using Quantifier-Free Presburger Arithmetic VMCAI 2019
- Path-Sensitive Analysis for Linear Arithmetic and Uninterpreted Functions SAS 2004
- Assertion Checking over Combined Abstraction of Linear Arithmetic and Uninterpreted Functions ESOP 2006
- Axe 'Em: Eliminating Spurious States with Induction Axioms POPL 2025
- Bitwuzla CAV 2023
- Simplification by Cooperating Decision Procedures TOPLAS 1979
- Beyond Quantifier-Free Interpolation in Extensions of Presburger Arithmetic VMCAI 2011
- Augmenting Model-Based Instantiation with Fast Enumeration TACAS 2025