Computer Aided Verification

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

Mathematics Subject Classification ID

Specification and verification (program logics, model checking, etc.) (68Q60)

Related Items

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, 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