- Referenced in 36 articles
- path-bounded model-checking) to determine test inputs for Parameterized Unit Tests. Pex learns...
- Referenced in 6 articles
- Checker). ByMC is a toolset for parameterized model checking of threshold-guarded fault-tolerant distributed...
- Referenced in 36 articles
- finite-state systems, but combines model checking with deductive methods to allow the verification ... broad class of systems, including parameterized (N-component) circuit designs, parameterized (N-process) programs...
- Referenced in 10 articles
- supports proving safety and liveness properties of parameterized and infinite-state systems via three modes ... using an SMT solver, abstraction and model checking, and manual proofs using natural deduction...
- Referenced in 3 articles
- model parameterization, PyBNF supports uncertainty quantification by bootstrapping or Bayesian approaches, and model checking. PyBNF ... defining qualitative data for use in parameterization or checking. It runs on most Linux...
- Referenced in 8 articles
- checking capability to enable formal reasoning about thread behaviors. Using this framework, memory models ... specified in a parameterized style—designers can simply redefine a few bypassing rules and visibility ... specification of another memory model. We formalize several classical memory models, including Sequential Consistency, Coherence ... analyze Java thread semantics using model checking. We also compare our operational specification style with...
- Referenced in 5 articles
- express the constraint store. Finally, CPBPV is parameterized with a list of solvers which ... which other frameworks based on bounded model checking have failed...
- Referenced in 9 articles
- graph databases. Graphs are prevalently used to model the relationships between objects in various domains ... then perform verification on each candidate by checking subgraph isomorphism. Query performance is improved since ... size of the index in a parameterized way. Our extensive experiments verify that query processing...
- Referenced in 2 articles
- pipelined-machine-Verification problems. We present a parameterized suite of benchmark problems arising from ... models, but also have complex correctness statements, involving invariants and symbolic simulations of the models ... take hundreds of thousands of seconds to check using the UCLID decision procedure...
- Referenced in 1 article
- results, make decisions, change the model and check again the new design until an optimal ... design changes. PAM-OPT manages compute model parameterization, and launches pre-processing, solver and post...
- Referenced in 173 articles
- Axiom is a general purpose Computer Algebra system...
- Referenced in 659 articles
- CoCoA is a system for Computations in Commutative...
- Referenced in 1906 articles
- Coq is a formal proof management system. It...
- Referenced in 3221 articles
- GAP is a system for computational discrete algebra...
- 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 264 articles
- In the core computer science areas -- data structures...
- Referenced in 1958 articles
- Macaulay2 is a software system devoted to supporting...
- Referenced in 5403 articles
- The result of over 30 years of cutting...
- Referenced in 6445 articles
- Almost any workflow involves computing results, and that...