- Referenced in 64 articles
- unbounded quantification, (co)inductive predicates and datatypes, and (co)recursive functions. Fundamentally a finite model...
- Referenced in 66 articles
- programmer may declare inductive datatypes and primitive recursive functions for specification. Verification proceeds by symbolic ... separation logic assertion. Folding or unfolding abstract predicate assertions is performed through explicit ghost statements ... representation equivalences and facts about the primitive recursive functions. An SMT solver is used...
- Referenced in 45 articles
- recursively enumerable, a defeasible reasoner based upon a rich logic like the predicate calculus cannot...
- Referenced in 1 article
- computational graph mimics the structure of recursive calls of the algorithm and serves both ... guideline for the definition of a domain predicate of which the inductive structure ... compatible with recursive calls; and (b) as a conformity predicate to ensure that ... illustrate the Braga method on various concrete recursive algorithms, including unbounded search, “fold-left” from...
- Referenced in 5 articles
- very powerful ASP system supporting (recursive) functions, sets, and lists, along with libraries for their ... inherits the possibility of defining external predicates...
- Referenced in 1 article
- database query supports recursion, allows Prolog as a language, and uses predicate calculus...
- Referenced in 2 articles
- this paper on model-checking non-recursive concurrent programs. Boom implements a recent variant ... model checking system-level code via predicate abstraction. We present experimental results for the verification...
- Referenced in 1906 articles
- Coq is a formal proof management system. It...
- Referenced in 74 articles
- Dafny is an imperative object-based language with...
- Referenced in 289 articles
- GMP is a free library for arbitrary precision...
- Referenced in 719 articles
- Isabelle is a generic proof assistant. It allows...
- Referenced in 5403 articles
- The result of over 30 years of cutting...
- Referenced in 6445 articles
- Almost any workflow involves computing results, and that...
- Referenced in 13702 articles
- MATLAB® is a high-level language and interactive...
- Referenced in 584 articles
- An extensible SAT-solver. MiniSat is a minimalistic...
- Referenced in 10196 articles
- R is a language and environment for statistical...
- Referenced in 746 articles
- REDUCE is an interactive system for general algebraic...
- Referenced in 20 articles
- SOLAR (SOL for Advanced Reasoning) is a first...
- Referenced in 554 articles
- SCIP is currently one of the fastest non...