Cited in
(only showing first 100 items - show all)- Combined Decision Techniques for the Existential Theory of the Reals
- Solving disjunctive temporal problems with preferences using maximum satisfiability
- Heaps and Data Structures: A Challenge for Automated Provers
- Combined task- and network-level scheduling for distributed time-triggered systems
- Extending Sledgehammer with SMT solvers
- Confluence by critical pair analysis revisited
- Analyzing program termination and complexity automatically with \textsf{AProVE}
- Verifying Whiley programs with Boogie
- \textsc{LTL} falsification in infinite-state systems
- Interpolation and model checking for nonlinear arithmetic
- Conflict-driven satisfiability for theory combination: lemmas, modules, and proofs
- \textsc{OptiMathSAT}: a tool for optimization modulo theories
- Automatic generation of logical models with AGES
- Automatic discovery of fair paths in infinite-state transition systems
- Architecting Solvers for SAT Modulo Theories: Nelson-Oppen with DPLL
- Design of fixed points in Boolean networks using feedback vertex sets and model reduction
- Being careful about theory combination
- URBiVA: uniform reduction to bit-vector arithmetic
- Automated verification and refinement for physical-layer protocols
- HOL-Boogie -- an interactive prover-backend for the verifying C compiler
- The axiomatization of override and update
- Translation-based approaches for solving disjunctive temporal problems with preferences
- Wombit: a portfolio bit-vector solver using word-level propagation
- scientific article; zbMATH DE number 7453201 (Why is no real title available?)
- Optimization modulo theories with linear rational costs
- SAT Modulo the Theory of Linear Arithmetic: Exact, Inexact and Commercial Solvers
- A note on the comparison between Bernoulli and limited policies in vacation models
- Supercharging plant configurations using Z3
- Rewriting, inference, and proof
- Synthesis of domain specific CNF encoders for bit-vector solvers
- Schemata of SMT-problems
- SMELS: Satisfiability Modulo Equality with Lazy Superposition
- A superposition calculus for abductive reasoning
- SMT-based verification of data-aware processes: a model-theoretic approach
- On solving quantified bit-vector constraints using invertibility conditions
- Encoding first order proofs in SMT
- Solving Non-linear Polynomial Arithmetic via SAT Modulo Linear Arithmetic
- Parallelizing SMT solving: lazy decomposition and conciliation
- An instantiation scheme for satisfiability modulo theories
- 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
- An iterative approach to precondition inference using constrained Horn clauses
- Invariant checking of NRA transition systems via incremental reduction to LRA with EUF
- Search-space partitioning for parallelizing SMT solvers
- Incomplete SMT techniques for solving non-linear formulas over the integers
- Optimal length resolution refutations of difference constraint systems
- Automated theorem provers for multiple-valued logics with satisfiability modulo theory solvers
- An SMT theory of fixed-point arithmetic
- Solving bitvectors with MCSAT: explanations from bits and pieces
- Runtime complexity analysis of logically constrained rewriting
- Termination of cycle rewriting by transformation and matrix interpretation
- Expressing polymorphic types in a many-sorted language
- Cutting the mix
- Efficient representation of piecewise linear functions into Łukasiewicz logic modulo satisfiability
- Testing-based formal verification for theorems and its application in software specification verification
- Multiple mutation testing from FSM
- New complexity results for Łukasiewicz logic
- Refutation-based synthesis in SMT
- Cuts from proofs: a complete and practical technique for solving linear inequalities over integers
- 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
- Structured derivations: a unified proof style for teaching mathematics
- Don't care words with an application to the automata-based approach for real addition
- Termination and complexity analysis for programs with bitvector arithmetic by symbolic execution
- Automated synthesis of distributed self-stabilizing protocols
- A combinatorial algorithm for Horn programs
- 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
- Translating FSP into LOTOS and networks of automata
- Beaver
- Boolector
- CoCoALib
- CPBPV
- GAVS
- GNT
- HOL-Boogie
- jETI
- JMLUnit
- MiniSat
- Reveal
- SDSAT
- SYNRAC
- TESTAS
- Cogent
- Prosper
- BarcelogicTools
- WoLFram
- LOGEN
- FLATA
- SMT-LIB
- Alt-Ergo
- cvc3
- Aspic
- KLEE
- Dagger
- UCLID
This page was built for software: Yices
