swMATH4436MaRDI QIDQ16612FDOQ16612
Author name not available (Why is that?)
Official website: http://yices.csl.sri.com/
Cited In (only showing first 100 items - show all)
- Heaps and Data Structures: A Challenge for Automated Provers
- Verifying Whiley programs with Boogie
- \textsc{LTL} falsification in infinite-state systems
- Automatic discovery of fair paths in infinite-state transition systems
- Design of fixed points in Boolean networks using feedback vertex sets and model reduction
- URBiVA: uniform reduction to bit-vector arithmetic
- Title not available (Why is that?)
- Translation-based approaches for solving disjunctive temporal problems with preferences
- Supercharging plant configurations using Z3
- Synthesis of domain specific CNF encoders for bit-vector solvers
- SMT-based verification of data-aware processes: a model-theoretic approach
- A superposition calculus for abductive reasoning
- On solving quantified bit-vector constraints using invertibility conditions
- Encoding first order proofs in SMT
- Zephyrus2
- Parallelizing SMT solving: lazy decomposition and conciliation
- Search-space partitioning for parallelizing SMT solvers
- CVC4SY
- Automated synthesis of distributed self-stabilizing protocols
- The sample analysis machine scheduling problem: definition and comparison of exact solving approaches
- Automatic verification of concurrent stochastic systems
- Proving termination of programs automatically with AProVE
- Finding DFAs with maximal shortest synchronizing word length
- Predicate Generation for Learning-Based Quantifier-Free Loop Invariant Inference
- Protocol analysis with time and space
- Program synthesis using dual interpretation
- dot
- On the parametrized complexity of read-once refutations in UTVPI+ constraint systems
- Feasibility checking in Horn constraint systems through a reduction based approach
- \textsc{Conjure}: automatic generation of constraint models from problem specifications
- Programming and symbolic computation in Maude
- Positive solutions of systems of signed parametric polynomial inequalities
- From model completeness to verification of data aware processes
- SAT modulo discrete event simulation applied to railway design capacity analysis
- Sharing is caring: combination of theories
- Extending SMT solvers with support for finite domain \texttt{alldifferent} constraint
- The SAT+CAS method for combinatorial search with applications to best matrices
- Title not available (Why is that?)
- Small Formulas for Large Programs: On-Line Constraint Simplification in Scalable Static Analysis
- JMLAutoTest
- Whiteoak
- Aeon
- TreeAutomizer
- Exact and parameterized algorithms for read-once refutations in Horn constraint systems
- New records of pre-image search of reduced SHA-1 using SAT solvers
- Counterexample-Guided Model Synthesis
- A complete and terminating approach to linear integer solving
- Modular strategic SMT solving with \textbf{SMT-RAT}
- Analyzing fractional Horn constraint systems
- On the lengths of tree-like and dag-like cutting plane refutations of Horn constraint systems. Horn constraint systems and cutting plane refutations
- eThor
- Solving disjunctive temporal problems with preferences using maximum satisfiability
- Confluence by critical pair analysis revisited
- Architecting Solvers for SAT Modulo Theories: Nelson-Oppen with DPLL
- Interpolation and model checking for nonlinear arithmetic
- Conflict-driven satisfiability for theory combination: lemmas, modules, and proofs
- Automated verification and refinement for physical-layer protocols
- SAT Modulo the Theory of Linear Arithmetic: Exact, Inexact and Commercial Solvers
- Optimization modulo theories with linear rational costs
- Rewriting, inference, and proof
- SMELS: Satisfiability Modulo Equality with Lazy Superposition
- An iterative approach to precondition inference using constrained Horn clauses
- A generalised branch-and-bound approach and its application in SAT modulo nonlinear integer arithmetic
- Solving nonlinear integer arithmetic with MCSAT
- Randomized algorithms for finding the shortest negative cost cycle in networks
- Incomplete SMT techniques for solving non-linear formulas over the integers
- Invariant checking of NRA transition systems via incremental reduction to LRA with EUF
- Automated theorem provers for multiple-valued logics with satisfiability modulo theory solvers
- Optimal length resolution refutations of difference constraint systems
- An SMT theory of fixed-point arithmetic
- Solving bitvectors with MCSAT: explanations from bits and pieces
- Expressing polymorphic types in a many-sorted language
- Runtime complexity analysis of logically constrained rewriting
- New complexity results for Łukasiewicz logic
- Refutation-based synthesis in SMT
- Conflict-driven satisfiability for theory combination: transition system and completeness
- SPASS-SATT. A CDCL(LA) solver
- A framework for verifying bit-level pipelined machines based on automated deduction and decision procedures
- A combinatorial algorithm for Horn programs
- Structured derivations: a unified proof style for teaching mathematics
- Termination and complexity analysis for programs with bitvector arithmetic by symbolic execution
- Don't care words with an application to the automata-based approach for real addition
- Effective use of SMT solvers for program equivalence checking through invariant-sketching and query-decomposition
- Translating FSP into LOTOS and networks of automata
- Proving termination of programs with bitvector arithmetic by symbolic execution
- Computing and estimating the volume of the solution space of SMT(LA) constraints
- Deciding Bit-Vector Formulas with mcSAT
- An SMT-based approach to weak controllability for disjunctive temporal problems with uncertainty
- A new probabilistic constraint logic programming language based on a generalised distribution semantics
- A combinatorial algorithm for Horn programs
- Fault localization of timed automata using maximum satisfiability
- Invariant generation through strategy iteration in succinctly represented control flow graphs
- Delayed theory combination vs. Nelson-Oppen for satisfiability modulo theories: a comparative analysis
- Automatically proving termination and memory safety for programs with pointer arithmetic
- Solving linear optimization over arithmetic constraint formula
- TotemBioNet
- Solving non-linear Horn clauses using a linear Horn clause solver
- Efficient Craig interpolation for linear Diophantine (dis)equations and linear modular equations
- The mechanical verification of a DPLL-based satisfiability solver
- Estimating the volume of solution space for satisfiability modulo linear real arithmetic
This page was built for software: Yices
