Yices
From MaRDI portal
Software:16612
swMATH4436MaRDI QIDQ16612FDOQ16612
Author name not available (Why is that?)
Cited In (only showing first 100 items - show all)
- Solving disjunctive temporal problems with preferences using maximum satisfiability
- Confluence by critical pair analysis revisited
- Analyzing program termination and complexity automatically with \textsf{AProVE}
- Combined task- and network-level scheduling for distributed time-triggered systems
- Architecting Solvers for SAT Modulo Theories: Nelson-Oppen with DPLL
- \textsc{OptiMathSAT}: a tool for optimization modulo theories
- Automatic generation of logical models with AGES
- Interpolation and model checking for nonlinear arithmetic
- Conflict-driven satisfiability for theory combination: lemmas, modules, and proofs
- HOL-Boogie -- an interactive prover-backend for the verifying C compiler
- Automated verification and refinement for physical-layer protocols
- Wombit: a portfolio bit-vector solver using word-level propagation
- The axiomatization of override and update
- Automatic Proof and Disproof in Isabelle/HOL
- Solving Non-linear Polynomial Arithmetic via SAT Modulo Linear Arithmetic
- An iterative approach to precondition inference using constrained Horn clauses
- Automated Confluence Proof by Decreasing Diagrams based on Rule-Labelling.
- An instantiation scheme for satisfiability modulo theories
- Randomized algorithms for finding the shortest negative cost cycle in networks
- Optimal length resolution refutations of difference constraint systems
- An SMT theory of fixed-point arithmetic
- Solving bitvectors with MCSAT: explanations from bits and pieces
- The Mechanical Verification of a DPLL-Based Satisfiability Solver
- Runtime complexity analysis of logically constrained rewriting
- Cutting the mix
- One Logic to Use Them All
- 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
- Optimization Modulo Theories with Linear Rational Costs
- Cuts from proofs: a complete and practical technique for solving linear inequalities over integers
- 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
- Don't care words with an application to the automata-based approach for real addition
- Translating FSP into LOTOS and networks of automata
- Deciding Bit-Vector Formulas with mcSAT
- Multi-Prover Verification of Floating-Point Programs
- A Generalised Branch-and-Bound Approach and Its Application in SAT Modulo Nonlinear Integer Arithmetic
- An SMT-based approach to weak controllability for disjunctive temporal problems with uncertainty
- Verification conditions for source-level imperative programs
- Solving Nonlinear Integer Arithmetic with MCSAT
- Extending Sledgehammer with SMT Solvers
- A System for Solving Constraint Satisfaction Problems with SMT
- A new probabilistic constraint logic programming language based on a generalised distribution semantics
- Deciding Bit-Vector Arithmetic with Abstraction
- Invariant Checking of NRA Transition Systems via Incremental Reduction to LRA with EUF
- Fault localization of timed automata using maximum satisfiability
- Delayed theory combination vs. Nelson-Oppen for satisfiability modulo theories: a comparative analysis
- Solving constraint satisfaction problems with SAT modulo theories
- Expressing Polymorphic Types in a Many-Sorted Language
- Time-budgeting: a component based development methodology for real-time embedded systems
- Solving weighted CSPs with meta-constraints by reformulation into satisfiability modulo theories
- Efficient Craig interpolation for linear Diophantine (dis)equations and linear modular equations
- Strategies for scalable symbolic execution-driven test generation for programs
- Extending Sledgehammer with SMT solvers
- Parametrized invariance for infinite state processes
- A Combinatorial Algorithm for Horn Programs
- Verification of clock synchronization algorithms: experiments on a combination of deductive tools
- Complexity of fixed-size bit-vector logics
- Model-based theory combination
- Probably half true: probabilistic satisfiability over Łukasiewicz infinitely-valued logic
- Incomplete SMT Techniques for Solving Non-Linear Formulas over the Integers
- Satisfiability Modulo Theories
- A search-based procedure for nonlinear real arithmetic
- Hammering towards QED
- Interpolants for Linear Arithmetic in SMT
- Solving strong controllability of temporal problems with uncertainty using SMT
- Cooperating techniques for solving nonlinear real arithmetic in the \texttt{cvc5} SMT solver (system description)
- Combining Instance Generation and Resolution
- Combined Decision Techniques for the Existential Theory of the Reals
- Exploiting subproblem optimization in SAT-based maxsat algorithms
- Symbolic trajectory evaluation for word-level verification: theory and implementation
- Proving Termination of Programs with Bitvector Arithmetic by Symbolic Execution
- Sharing Is Caring: Combination of Theories
- Heaps and Data Structures: A Challenge for Automated Provers
- Fast Cube Tests for LIA Constraint Solving
- Title not available (Why is that?)
- Verifying Whiley programs with Boogie
- \textsc{LTL} falsification in infinite-state systems
- Automatic discovery of fair paths in infinite-state transition systems
- Title not available (Why is that?)
- SAT Modulo the Theory of Linear Arithmetic: Exact, Inexact and Commercial Solvers
- Supercharging plant configurations using Z3
- Satisfiability Solving and Model Generation for Quantified First-Order Logic Formulas
- SMELS: Satisfiability Modulo Equality with Lazy Superposition
- SMT-based verification of data-aware processes: a model-theoretic approach
- Finding DFAs with Maximal Shortest Synchronizing Word Length
- A superposition calculus for abductive reasoning
- On solving quantified bit-vector constraints using invertibility conditions
- Encoding first order proofs in SMT
- Title not available (Why is that?)
- Parallelizing SMT solving: lazy decomposition and conciliation
- Automated theorem provers for multiple-valued logics with satisfiability modulo theory solvers
- Synthesis of Domain Specific CNF Encoders for Bit-Vector Solvers
- Termination and complexity analysis for programs with bitvector arithmetic by symbolic execution
- The sample analysis machine scheduling problem: definition and comparison of exact solving approaches
- Automatic verification of concurrent stochastic systems
- Effective use of SMT solvers for program equivalence checking through invariant-sketching and query-decomposition
This page was built for software: Yices