Deprecated: $wgMWOAuthSharedUserIDs=false is deprecated, set $wgMWOAuthSharedUserIDs=true, $wgMWOAuthSharedUserSource='local' instead [Called from MediaWiki\HookContainer\HookContainer::run in /var/www/html/w/includes/HookContainer/HookContainer.php at line 135] in /var/www/html/w/includes/Debug/MWDebug.php on line 372
FOCI - MaRDI portal

FOCI

From MaRDI portal
Software:24792



swMATH12868MaRDI QIDQ24792


No author found.





Related Items (63)

Ground interpolation for the theory of equalityQuantifier-Free Interpolation of a Theory of ArraysMind the Gap: Bit-vector Interpolation recast over Linear Integer ArithmeticPreface: Special issue on interpolationLabelled interpolation systems for hyper-resolution, clausal, and local proofsProof tree preserving tree interpolationInterpolation systems for ground proofs in automated deduction: a surveyInterpolation and model checking for nonlinear arithmeticLatticed \(k\)-induction with an application to probabilistic programsUnnamed ItemCraig Interpolation in the Presence of Non-linear ConstraintsA Combination of Rewriting and Constraint Solving for the Quantifier-Free Interpolation of Arrays with Integer Difference ConstraintsSAT-Based Model CheckingSatisfiability Modulo TheoriesInterpolation and Model CheckingUnbounded Model-Checking with Interpolation for Regular Language ConstraintsAn institution-independent proof of the Robinson consistency theoremConstraint solving for interpolationCraig interpolation with clausal first-order tableauxEquality detection for linear arithmetic constraintsSAT-based verification for timed component connectorsAn interpolating sequent calculus for quantifier-free Presburger arithmeticHierarchical and Modular Reasoning in Complex Theories: The Case of Local Theory ExtensionsUnnamed ItemComplete instantiation-based interpolationPreservation of Craig interpolation by the product of matrix logicsInterpolants for Linear Arithmetic in SMTResolution proof transformation for compression and interpolationOn Interpolation in Decision ProceduresParallelizing SMT solving: lazy decomposition and conciliationImproved Single Pass Algorithms for Resolution Proof ReductionQuantifier-free interpolation in combinations of equality interpolating theoriesRewriting InterpolantsExperience of improving the BLAST static verification toolCraig interpolation in the presence of unreliable connectivesCompetent predicate abstraction in model checkingGene sorting in differential evolution with cross-generation mutationConstrained Monotonic Abstraction: A CEGAR for Parameterized VerificationA Tutorial on Satisfiability Modulo TheoriesInterpolant Generation for UTVPIGround Interpolation for Combined TheoriesInterpolation and Symbol EliminationChallenges in Constraint-Based Analysis of Hybrid SystemsState of the Union: Type Inference Via Craig InterpolationGround Interpolation for the Theory of EqualityEfficient Interpolant Generation in Satisfiability Modulo Linear Integer ArithmeticEfficient Interpolant Generation in Satisfiability Modulo TheoriesQuantified Invariant Generation Using an Interpolating Saturation ProverEfficient Interpolant Generation in Satisfiability Modulo Linear Integer ArithmeticBeyond Quantifier-Free Interpolation in Extensions of Presburger ArithmeticPredicate Generation for Learning-Based Quantifier-Free Loop Invariant InferencePredicate Generation for Learning-Based Quantifier-Free Loop Invariant InferenceInterpolant Synthesis for Quadratic Polynomial Inequalities and Combination with EUFOn Interpolation and Symbol Elimination in Theory ExtensionsInterpolating bit-vector formulas using uninterpreted predicates and Presburger arithmeticInterpolation in computing science: The semantics of modularizationA Survey of Satisfiability Modulo TheoryAbstract Counterexamples for Non-disjunctive AbstractionsEfficient Craig interpolation for linear Diophantine (dis)equations and linear modular equationsTools and Algorithms for the Construction and Analysis of SystemsAn interpolating theorem proverOn interpolation in automated theorem provingReasoning in the theory of heap: satisfiability and interpolation


This page was built for software: FOCI