Computer Aided Verification
From MaRDI portal
Publication:5312898
DOI10.1007/B98490zbMath1103.68616OpenAlexW4298302743MaRDI QIDQ5312898
George Hagen, Robert Nieuwenhuis, Harald Ganzinger, Cesare Tinelli, Albert Oliveras
Publication date: 25 August 2005
Published in: Lecture Notes in Computer Science (Search for Journal in Brave)
Full work available at URL: https://doi.org/10.1007/b98490
Related Items (48)
A decision procedure for (co)datatypes in SMT solvers ⋮ Automated generation of exam sheets for automated deduction ⋮ Decision Procedures for Region Logic ⋮ Proof tree preserving tree interpolation ⋮ Satisfiability Modulo Theories ⋮ A Decision Procedure for (Co)datatypes in SMT Solvers ⋮ Generalizing DPLL and satisfiability for equalities ⋮ Design and results of the first satisfiability modulo theories competition (SMT-COMP 2005) ⋮ Applying SAT solving in classification of finite algebras ⋮ M\textbf{ath}SAT: Tight integration of SAT and mathematical decision procedures ⋮ Extending SMT solvers with support for finite domain \texttt{alldifferent} constraint ⋮ HOL-Boogie -- an interactive prover-backend for the verifying C compiler ⋮ Fast congruence closure and extensions ⋮ A framework for verifying bit-level pipelined machines based on automated deduction and decision procedures ⋮ Bounded Model Checking of Analog and Mixed-Signal Circuits Using an SMT Solver ⋮ Synthesising programs with non-trivial constants ⋮ Reasoning in the Bernays-Schönfinkel-Ramsey Fragment of Separation Logic ⋮ Weakly Equivalent Arrays ⋮ Efficient theory combination via Boolean search ⋮ Solving finite-domain linear constraints in presence of the $\texttt{alldifferent}$ ⋮ A Lambda-Free Higher-Order Recursive Path Order ⋮ SAT Modulo ODE: A Direct SAT Approach to Hybrid Systems ⋮ Automatic construction and verification of isotopy invariants ⋮ Deciding floating-point logic with abstract conflict driven clause learning ⋮ Design and results of the 2nd annual satisfiability modulo theories competition (SMT-COMP 2006) ⋮ Parametrized invariance for infinite state processes ⋮ Encoding OCL Data Types for SAT-Based Verification of UML/OCL Models ⋮ A search-based procedure for nonlinear real arithmetic ⋮ Harald Ganzinger’s Legacy: Contributions to Logics and Programming ⋮ CPBPV: a constraint-programming framework for bounded program verification ⋮ Volume Computation for Boolean Combination of Linear Arithmetic Constraints ⋮ Decidable \({\exists}^*{\forall}^*\) first-order fragments of linear rational arithmetic with uninterpreted predicates ⋮ Equivalence checking for orthocomplemented bisemilattices in log-linear time ⋮ SCIP: solving constraint integer programs ⋮ The SAT+CAS method for combinatorial search with applications to best matrices ⋮ Dashed strings for string constraint solving ⋮ SPASS-SATT. A CDCL(LA) solver ⋮ Applying computer algebra systems with SAT solvers to the Williamson conjecture ⋮ A framework for satisfiability modulo theories ⋮ Delayed theory combination vs. Nelson-Oppen for satisfiability modulo theories: a comparative analysis ⋮ Solving quantified verification conditions using satisfiability modulo theories ⋮ Combining Equational Reasoning ⋮ Subsumption demodulation in first-order theorem proving ⋮ Rewrite-Based Decision Procedures ⋮ Generating Minimum Transitivity Constraints in P-time for Deciding Equality Logic ⋮ Model-based Theory Combination ⋮ Distributing the Workload in a Lazy Theorem-Prover ⋮ SMELS: satisfiability modulo equality with lazy superposition
This page was built for publication: Computer Aided Verification
