Interpolation and model checking for nonlinear arithmetic (Q832268): Difference between revisions

@@ Property / describes a project that uses @@
+nuXmv
@@ Property / describes a project that uses: nuXmv / rank @@
+Normal rank
@@ Property / describes a project that uses @@
+Spacer
@@ Property / describes a project that uses: Spacer / rank @@
+Normal rank
@@ Property / describes a project that uses @@
+MiniSat
@@ Property / describes a project that uses: MiniSat / rank @@
+Normal rank
@@ Property / describes a project that uses @@
+Yices
@@ Property / describes a project that uses: Yices / rank @@
+Normal rank
@@ Property / describes a project that uses @@
+FOCI
@@ Property / describes a project that uses: FOCI / rank @@
+Normal rank
@@ Property / MaRDI profile type @@
+MaRDI publication profile
@@ Property / MaRDI profile type: MaRDI publication profile / rank @@
+Normal rank
@@ Property / OpenAlex ID @@
+W3184821935
@@ Property / OpenAlex ID: W3184821935 / rank @@
+Normal rank
@@ Property / arXiv ID @@
+.04340
@@ Property / arXiv ID: 2106.04340 / rank @@
+Normal rank
@@ Property / cites work @@
+Satisfiability Modulo Theories
@@ Property / cites work: Satisfiability Modulo Theories / rank @@
+Normal rank
@@ Property / cites work @@
+Algorithms in real algebraic geometry
@@ Property / cites work: Algorithms in real algebraic geometry / rank @@
+Normal rank
@@ Property / cites work @@
+Constructing a single cell in cylindrical algebraic decomposition
+Normal rank
@@ Property / cites work @@
+Q4385444
@@ Property / cites work: Q4385444 / rank @@
+Normal rank
@@ Property / cites work @@
+Q5739497
@@ Property / cites work: Q5739497 / rank @@
+Normal rank
@@ Property / cites work @@
+Invariant Checking of NRA Transition Systems via Incremental Reduction to LRA with EUF
+Normal rank
@@ Property / cites work @@
+Efficient Interpolant Generation in Satisfiability Modulo Theories
+Normal rank
@@ Property / cites work @@
+Q4079605
@@ Property / cites work: Q4079605 / rank @@
+Normal rank
@@ Property / cites work @@
+Three uses of the Herbrand-Gentzen theorem in relating model theory and proof theory
+Normal rank
@@ Property / cites work @@
+Generating Non-linear Interpolants by Semidefinite Programming
+Normal rank
@@ Property / cites work @@
+A Model-Constructing Satisfiability Calculus
@@ Property / cites work: A Model-Constructing Satisfiability Calculus / rank @@
+Normal rank
@@ Property / cites work @@
+Theory and Applications of Satisfiability Testing
@@ Property / cites work: Theory and Applications of Satisfiability Testing / rank @@
+Normal rank
@@ Property / cites work @@
+Q2845506
@@ Property / cites work: Q2845506 / rank @@
+Normal rank
@@ Property / cites work @@
+Interpolant Synthesis for Quadratic Polynomial Inequalities and Combination with EUF
+Normal rank
@@ Property / cites work @@
+Nonlinear Craig interpolant generation
@@ Property / cites work: Nonlinear Craig interpolant generation / rank @@
+Normal rank
@@ Property / cites work @@
+Interpolants in nonlinear theories over the reals
@@ Property / cites work: Interpolants in nonlinear theories over the reals / rank @@
+Normal rank
@@ Property / cites work @@
+A procedure for proving special function inequalities involving a discrete parameter
+Normal rank
@@ Property / cites work @@
+Solving bitvectors with MCSAT: explanations from bits and pieces
+Normal rank
@@ Property / cites work @@
+Abstractions from proofs
@@ Property / cites work: Abstractions from proofs / rank @@
+Normal rank
@@ Property / cites work @@
+Generalized Property Directed Reachability
@@ Property / cites work: Generalized Property Directed Reachability / rank @@
+Normal rank
@@ Property / cites work @@
+Efficient interpolation for the theory of arrays
@@ Property / cites work: Efficient interpolation for the theory of arrays / rank @@
+Normal rank
@@ Property / cites work @@
+Constructing Craig interpolation formulas
@@ Property / cites work: Constructing Craig interpolation formulas / rank @@
+Normal rank
@@ Property / cites work @@
+Solving Nonlinear Integer Arithmetic with MCSAT
@@ Property / cites work: Solving Nonlinear Integer Arithmetic with MCSAT / rank @@
+Normal rank
@@ Property / cites work @@
+Solving Non-linear Arithmetic
@@ Property / cites work: Solving Non-linear Arithmetic / rank @@
+Normal rank
@@ Property / cites work @@
+SMT-based model checking for recursive programs
@@ Property / cites work: SMT-based model checking for recursive programs / rank @@
+Normal rank
@@ Property / cites work @@
+Interpolation theorems, lower bounds for proof systems, and independence results for bounded arithmetic
+Normal rank
@@ Property / cites work @@
+Craig Interpolation in the Presence of Non-linear Constraints
+Normal rank
@@ Property / cites work @@
+An interpolating theorem prover
@@ Property / cites work: An interpolating theorem prover / rank @@
+Normal rank
@@ Property / cites work @@
+Quantified Invariant Generation Using an Interpolating Saturation Prover
+Normal rank
@@ Property / cites work @@
+Q4282674
@@ Property / cites work: Q4282674 / rank @@
+Normal rank
@@ Property / cites work @@
+Lower bounds for resolution and cutting plane proofs and monotone computations
+Normal rank
@@ Property / cites work @@
+Selfless Interpolation for Infinite-State Model Checking
+Normal rank