Yices

swMATH4436MaRDI QIDQ16612FDOQ16612

Author name not available (Why is that?)

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
• Title not available (Why is that?)
• SAT Modulo the Theory of Linear Arithmetic: Exact, Inexact and Commercial Solvers
• Supercharging plant configurations using Z3
• Rewriting, inference, and proof
• Synthesis of domain specific CNF encoders for bit-vector solvers
• SMELS: Satisfiability Modulo Equality with Lazy Superposition
• 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
• Parallelizing SMT solving: lazy decomposition and conciliation
• Search-space partitioning for parallelizing SMT solvers
• Automated theorem provers for multiple-valued logics with satisfiability modulo theory solvers
• Automated synthesis of distributed self-stabilizing protocols
• 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
• Proving termination of programs automatically with AProVE
• Finding DFAs with maximal shortest synchronizing word length
• Proving termination of programs with bitvector arithmetic by symbolic execution
• Protocol analysis with time and space
• Program synthesis using dual interpretation
• Computing and estimating the volume of the solution space of SMT(LA) constraints
• 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
• Invariant generation through strategy iteration in succinctly represented control flow graphs
• Automatically proving termination and memory safety for programs with pointer arithmetic
• Solving linear optimization over arithmetic constraint formula
• Positive solutions of systems of signed parametric polynomial inequalities
• From model completeness to verification of data aware processes
• Solving non-linear Horn clauses using a linear Horn clause solver
• SAT modulo discrete event simulation applied to railway design capacity analysis
• Estimating the volume of solution space for satisfiability modulo linear real arithmetic
• Sharing is caring: combination of theories
• The SAT+CAS method for combinatorial search with applications to best matrices
• Title not available (Why is that?)
• New techniques for linear arithmetic: cubes and equalities
• Propagation based local search for bit-precise reasoning
• Solving quantified linear arithmetic by counterexample-guided instantiation
• Small Formulas for Large Programs: On-Line Constraint Simplification in Scalable Static Analysis
• Fast cube tests for LIA constraint solving
• Exact and parameterized algorithms for read-once refutations in Horn constraint systems
• A probabilistic approximate logic for neuro-symbolic learning and reasoning
• New records of pre-image search of reduced SHA-1 using SAT solvers
• Satisfiability solving and model generation for quantified first-order logic formulas
• Sharpening constraint programming approaches for bit-vector theory
• Counterexample-Guided Model Synthesis
• MedleySolver: online SMT algorithm selection
• Smt-Switch: a solver-agnostic C++ API for SMT solving
• 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
• Solving disjunctive temporal problems with preferences using maximum satisfiability
• Extending Sledgehammer with SMT solvers
• 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
• Optimization modulo theories with linear rational costs
• Solving Non-linear Polynomial Arithmetic via SAT Modulo Linear Arithmetic
• 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
• An instantiation scheme for satisfiability modulo theories
• 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
• 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
• Cutting the mix
• 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
• 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
• An SMT-based approach to weak controllability for disjunctive temporal problems with uncertainty
• Verification conditions for source-level imperative programs

This page was built for software: Yices