
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...

iProverEq
 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 ... modelchecking 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 fixpoints by solving Satisfiability Modulo Theories ... quantifier instantiation, specifically tailored to model checking, are at the very heart of the system...

DRATtrim
 Referenced in 28 articles
[sw13313]
 checking and trimming using expressive clausal proofs. The DRATtrim tool is a satisfiability proof ... techniques can be validated using DRATtrim. 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...