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

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

HyTech
 Referenced in 331 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 26 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 12 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 24 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 36 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 8 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...

MCGP
 Referenced in 15 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...

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

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

TDDS
 Referenced in 7 articles
[sw31513]
 given an additional equation, checking whether this equation is satisfied by all common solutions...

AMT
 Referenced in 13 articles
[sw38045]
 specification and checks, in an offline or incremental fashion, whether simulation traces satisfy the property...

Anteater
 Referenced in 4 articles
[sw32373]
 level network invariants into boolean satisfiability problems (SAT), checks them against network state using...