• clasp

  • Referenced in 90 articles [sw07095]
  • technique that proved very successful for satisfiability checking (SAT). Unlike other learning ASP solvers, clasp...
  • SLAM

  • Referenced in 150 articles [sw03136]
  • SLAM is a project for checking that software satisfies critical behavioral properties of the interfaces...
  • HyTech

  • Referenced in 320 articles [sw04125]
  • condition under which a linear hybrid system satisfies a temporal requirement. Hybrid systems are specified ... temporal requirements are verified by symbolic model checking. If the verification fails, then HyTech generates...
  • Quantor

  • Referenced in 22 articles [sw28381]
  • formulas (QBF) in the QDIMACS format. Checking satisfiability of QBF, the QBF problem ... deterministic planning or symbolic model checking can be formulated succinctly in QBF. In our recent...
  • LoLA

  • Referenced in 24 articles [sw04381]
  • state predicates and CTL model checking. For satisfiability, both exhaustive search and heuristically goal oriented...
  • iProver-Eq

  • Referenced in 8 articles [sw09452]
  • reasoning is combined with efficient ground satisfiability checking where the latter is delegated...
  • CCASat

  • Referenced in 10 articles [sw12924]
  • Local search for Boolean satisfiability with configuration checking and subscore. This paper presents and analyzes ... Satisfiability (SAT) problem. We start by proposing a local search strategy called configuration checking ... with great scores, if they do not satisfy the CC criterion. We improve ... variable selection heuristic called configuration checking with aspiration (CCA). The CCA heuristic leads...
  • Concurrency Workbench

  • Referenced in 12 articles [sw14749]
  • powerful modal logic and check whether a given process satisfies a specification formulated in this ... model-checking games to understand why a process does or does not satisfy a formula...
  • Mcmt

  • Referenced in 19 articles [sw11911]
  • unsafe states and checks for safety and fix-points by solving Satisfiability Modulo Theories ... quantifier instantiation, specifically tailored to model checking, are at the very heart of the system...
  • DRAT-trim

  • Referenced in 28 articles [sw13313]
  • checking and trimming using expressive clausal proofs. The DRAT-trim tool is a satisfiability proof ... techniques can be validated using DRAT-trim. Checking time of a proof is comparable...
  • EAGLE

  • Referenced in 7 articles [sw31989]
  • used in a number of practical model checking tools. Reactive Modules Games is a game ... strategically in an attempt to satisfy a temporal logic formula representing their individual goal ... representation of players strategies; it then checks whether these strategies form a Nash equilibrium ... conventional temporal logic satisfiability and model checking techniques. We first give an overview...
  • RoVerGeNe

  • Referenced in 13 articles [sw10954]
  • problems: robustness analysis: checking whether a dynamical property is satisfied by every parameter...
  • SMV

  • Referenced in 13 articles [sw04135]
  • model checking algorithm to efficiently determine whether specifications expressed in CTL are satisfied...
  • qtlsolver

  • Referenced in 2 articles [sw14602]
  • solver for checking satisfiability of Quantitative / Metric Interval Temporal Logic (MITL/QTL) over Reals...
  • MCGP

  • Referenced in 14 articles [sw00562]
  • generating new candidate solutions, while deep model checking is used for calculating to what extent ... only whether) a candidate solution program satisfies a property. The main challenge is to construct ... from the result of the deep model checking a fitness function that has a good...
  • Limboole

  • Referenced in 2 articles [sw28117]
  • Limboole is a simple tool for checking satisfiability respectively tautology on arbitrary structural formulas...
  • EufDPLL

  • Referenced in 1 article [sw11551]
  • EufDPLL -- A tool to check satisfiability of equality logic formulas. Decision procedures for subsets ... DPLL). EufDPLL is a tool to check satisfiability of EUF formulas based on this procedure...
  • TGC

  • Referenced in 1 article [sw11989]
  • Tableaux with Global Caching”, checks satisfiability of a set of concepts w.r.t...
  • RegStab

  • Referenced in 2 articles [sw00794]
  • regular schemata tableau) that solves the satisfiability problem for a class of propositional schemata ... integers). Our system allows one to check the satisfiability of sequences of formulae such...
  • APMC

  • Referenced in 27 articles [sw11483]
  • induce a prohibitive cost for the model checking algorithm. In this paper, we propose ... expressed by some positive LTL formula is satisfied with high confidence by a probabilistic system...