An Online Proof-Producing Decision Procedure for Mixed-Integer Linear Arithmetic
No abstract available.
Related papers
- Proof Tree Preserving Interpolation TACAS 2013
- Decision Procedures for Automating Termination Proofs VMCAI 2011
- Satisfiability Modulo Finite Fields CAV 2023
- On Using Floating-Point Computations to Help an Exact Linear Arithmetic Decision Procedure CAV 2009
- Reasoning in the Bernays-Schönfinkel-Ramsey Fragment of Separation Logic VMCAI 2017
- Formal verification of a program obfuscation based on mixed Boolean-arithmetic expressions CPP 2019
- Simplification by Cooperating Decision Procedures TOPLAS 1979
- Synthesizing MILP Constraints for Efficient and Robust Optimization PLDI 2023