Yices

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