Yices

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
• Extending Sledgehammer with SMT solvers
• Analyzing program termination and complexity automatically with \textsf{AProVE}
• \textsc{OptiMathSAT}: a tool for optimization modulo theories
• Automatic generation of logical models with AGES
• Boolector
• GAVS
• GNT
• HOL-Boogie
• SDSAT
• TESTAS
• Cogent
• Prosper
• WoLFram
• SMT-LIB
• Alt-Ergo
• cvc3
• Aspic
• KLEE
• Dagger
• UCLID
• LogMIP
• SIMPLIFY
• z3
• PPL
• PURRS
• libpoly
• FlatZinc
• MiniZinc
• ASASP
• GiNaCRA
• bv2epr
• dReal
• ESC4
• ATGen
• DART
• GATeL
• Eclat
• SMTInterpol
• veriT
• Ultimate Automizer
• TRACER
• CVC Lite
• csp2B
• AProVE
• OpenSMT
• SYMBA
• StarExec
• CVC4
• MathSAT

This page was built for software: Yices