The following pages link to Yices (Q16612):
Displayed 50 items.
- Combined task- and network-level scheduling for distributed time-triggered systems (Q258438) (← links)
- Strategies for scalable symbolic execution-driven test generation for programs (Q350939) (← links)
- An instantiation scheme for satisfiability modulo theories (Q438578) (← links)
- Cuts from proofs: a complete and practical technique for solving linear inequalities over integers (Q453505) (← links)
- Verification conditions for source-level imperative programs (Q465685) (← links)
- Solving constraint satisfaction problems with SAT modulo theories (Q487632) (← links)
- Solving weighted CSPs with meta-constraints by reformulation into satisfiability modulo theories (Q487655) (← links)
- Parametrized invariance for infinite state processes (Q493122) (← links)
- Complexity of fixed-size bit-vector logics (Q504997) (← links)
- A search-based procedure for nonlinear real arithmetic (Q518407) (← links)
- Exploiting subproblem optimization in SAT-based maxsat algorithms (Q525063) (← links)
- Symbolic trajectory evaluation for word-level verification: theory and implementation (Q526779) (← links)
- Automated verification and refinement for physical-layer protocols (Q539420) (← links)
- Structured derivations: a unified proof style for teaching mathematics (Q607406) (← links)
- Translating FSP into LOTOS and networks of automata (Q613134) (← links)
- Time-budgeting: a component based development methodology for real-time embedded systems (Q736795) (← links)
- Interpolation and model checking for nonlinear arithmetic (Q832268) (← links)
- Conflict-driven satisfiability for theory combination: lemmas, modules, and proofs (Q832719) (← links)
- Optimal length resolution refutations of difference constraint systems (Q846163) (← links)
- A framework for verifying bit-level pipelined machines based on automated deduction and decision procedures (Q877828) (← links)
- An SMT-based approach to weak controllability for disjunctive temporal problems with uncertainty (Q892228) (← links)
- A new probabilistic constraint logic programming language based on a generalised distribution semantics (Q896427) (← links)
- The axiomatization of override and update (Q975885) (← links)
- Don't care words with an application to the automata-based approach for real addition (Q1028730) (← links)
- Delayed theory combination vs. Nelson-Oppen for satisfiability modulo theories: a comparative analysis (Q1037399) (← links)
- Efficient Craig interpolation for linear Diophantine (dis)equations and linear modular equations (Q1039847) (← links)
- Termination and complexity analysis for programs with bitvector arithmetic by symbolic execution (Q1647969) (← links)
- Effective use of SMT solvers for program equivalence checking through invariant-sketching and query-decomposition (Q1656596) (← links)
- Computing and estimating the volume of the solution space of SMT(LA) constraints (Q1659994) (← links)
- Solving linear optimization over arithmetic constraint formula (Q1675635) (← links)
- New techniques for linear arithmetic: cubes and equalities (Q1688532) (← links)
- Solving quantified linear arithmetic by counterexample-guided instantiation (Q1688537) (← links)
- Propagation based local search for bit-precise reasoning (Q1688546) (← links)
- Randomized algorithms for finding the shortest negative cost cycle in networks (Q1693163) (← links)
- Automated theorem provers for multiple-valued logics with satisfiability modulo theory solvers (Q1697332) (← links)
- Cutting the mix (Q1702886) (← links)
- Parallelizing SMT solving: lazy decomposition and conciliation (Q1749390) (← links)
- Positive solutions of systems of signed parametric polynomial inequalities (Q1798326) (← links)
- Probably half true: probabilistic satisfiability over Łukasiewicz infinitely-valued logic (Q1799080) (← links)
- Sharpening constraint programming approaches for bit-vector theory (Q2011567) (← links)
- A superposition calculus for abductive reasoning (Q2013317) (← links)
- Fault localization of timed automata using maximum satisfiability (Q2026559) (← links)
- On the parametrized complexity of Read-once refutations in UTVPI+ constraint systems (Q2049975) (← links)
- On solving quantified bit-vector constraints using invertibility conditions (Q2050109) (← links)
- SAT modulo discrete event simulation applied to railway design capacity analysis (Q2058381) (← links)
- New records of pre-image search of reduced SHA-1 using SAT solvers (Q2079908) (← links)
- On the lengths of tree-like and dag-like cutting plane refutations of Horn constraint systems. Horn constraint systems and cutting plane refutations (Q2095546) (← links)
- An SMT theory of fixed-point arithmetic (Q2096435) (← links)
- Solving bitvectors with MCSAT: explanations from bits and pieces (Q2096440) (← links)
- Verifying Whiley programs with Boogie (Q2102933) (← links)