• UCLID

  • Referenced in 25 articles [sw04657]
  • based verification. As a stand-alone decision procedure for the theories of uninterpreted functions...
  • Cyclist

  • Referenced in 21 articles [sw18519]
  • addition, over the years several decision procedures or algorithms have been integrated, focusing on Separation...
  • ICS

  • Referenced in 20 articles [sw21618]
  • Canonizer and Solver) is an efficient decision procedure for a fragment of first-order logic...
  • dReach

  • Referenced in 19 articles [sw20164]
  • numbers, which are solved by delta-decision procedures in the SMT solver dReach. In this...
  • ModLeanTAP

  • Referenced in 19 articles [sw12368]
  • restrictions and fairness strategies, giving a decision procedure for the logics...
  • FULPAL

  • Referenced in 19 articles [sw09138]
  • inequalities and in soft constraints. The decision procedure is modelled as an interactive man-machine...
  • TABLEAUX

  • Referenced in 18 articles [sw11674]
  • their transitive closure and converse. The decision procedure we use is basically a semantic tableaux...
  • M-MACBETH

  • Referenced in 104 articles [sw16199]
  • help a decision maker or a decision-advising group quantify the relative attractiveness of options ... employs an initial, interactive, questioning procedure that compares two elements at a time, requesting only ... that is entirely consistent with all the decision maker ’s judgements. Through a similar process...
  • CSIsat

  • Referenced in 15 articles [sw11407]
  • present CSIsat, an interpolating decision procedure for the quantifier-free theory of rational linear arithmetic...
  • DCVALID

  • Referenced in 15 articles [sw20416]
  • based on an automata theoretic decision procedure for Quantified Discrete-time Duration Calculus (QDDC...
  • Metagraphs

  • Referenced in 20 articles [sw01368]
  • contain stored data, data analysis procedures, and decision models. However, many DSS have grown...
  • CoLoSS

  • Referenced in 14 articles [sw07016]
  • Moreover, CoLoSS is compositional: it synthesises decision procedures for modular combinations of logics that include...
  • LIRA

  • Referenced in 8 articles [sw21270]
  • tasks relies on efficient implementations of decision procedures for fragments of first-order logic. Interactive ... also make use of such decision procedures to increase the level of automation. Our tool ... lira implements decision procedures based on automata-theoretic techniques for first-order logics with linear...
  • KRIPKE

  • Referenced in 8 articles [sw01162]
  • appropriate vocabulary) the decision procedure for each of these logics describes a way of recursively ... nite. However in practice this decision procedure tends to be impossible ... question of whether this decision procedure could be mechanized via computer was asked...
  • Regex_Equivalence

  • Referenced in 7 articles [sw32229]
  • Unified Decision Procedures for Regular Expression Equivalence. We formalize a unified framework for verified decision ... Five recently published formalizations of such decision procedures (three based on derivatives, two on marked ... compare the performance of the different decision procedures in a meaningful way. The formalization...
  • Spacer

  • Referenced in 12 articles [sw19496]
  • summaries. Under-approximations are used to analyze procedure calls without inlining. Over-approximations are used ... programs, the algorithm is a polynomial decision procedure, matching the worst-case bounds...
  • JPF-SE

  • Referenced in 12 articles [sw12038]
  • uses off-the-shelf decision procedures to manipulate numeric constraints...
  • MSO_Regex_Equivalence

  • Referenced in 7 articles [sw32230]
  • Decision Procedures for MSO on Words Based on Derivatives of Regular Expressions. Monadic second-order ... decidable yet expressive logic into which many decision problems can be encoded. Since MSO formulas ... automata). We verify an executable decision procedure for MSO formulas that is not based ... automata but on regular expressions. Decision procedures for regular expression equivalence have been formalized before...
  • VeriML

  • Referenced in 8 articles [sw13522]
  • users can develop complex tactics and decision procedures using a rich programming model ... users avoid developing domain-specific tactics and decision procedures.par In this paper, we present VeriML ... number of type-safe tactics and decision procedures written in VeriML...
  • PAGAI

  • Referenced in 8 articles [sw13095]
  • algorithms combining abstract interpretation and decision procedures (SMT-solving), focusing on distinction of paths inside ... iteration algorithm, and the decision procedure. We compared the time and precision of various combinations...