Pages that link to "Item:Q2473386"

The following pages link to Decision procedures. An algorithmic point of view. With foreword by Randal E. Bryant (Q2473386):

Displaying 50 items.

• Labelled interpolation systems for hyper-resolution, clausal, and local proofs (Q286731) (← links)
• Semantically-guided goal-sensitive reasoning: model representation (Q287333) (← links)
• A pearl on SAT and SMT solving in Prolog (Q428887) (← links)
• Towards a notion of unsatisfiable and unrealizable cores for LTL (Q433349) (← links)
• An approach to multicore parallelism using functional programming: a case study based on Presburger arithmetic (Q478379) (← links)
• Runtime verification of embedded real-time systems (Q479806) (← links)
• Complexity of fixed-size bit-vector logics (Q504997) (← links)
• Fixed points, Nash equilibria, and the existential theory of the reals (Q519892) (← links)
• Symbolic trajectory evaluation for word-level verification: theory and implementation (Q526779) (← links)
• Equality detection for linear arithmetic constraints (Q621462) (← links)
• Time-budgeting: a component based development methodology for real-time embedded systems (Q736795) (← links)
• Conflict-driven satisfiability for theory combination: lemmas, modules, and proofs (Q832719) (← links)
• Targeted and contextual redescription set exploration (Q1631833) (← links)
• Propagation based local search for bit-precise reasoning (Q1688546) (← links)
• On logical bifurcation diagrams (Q1739287) (← links)
• Experience of improving the BLAST static verification tool (Q1758710) (← links)
• Some results on parametric temporal logic (Q1944185) (← links)
• Superposition as a decision procedure for timed automata (Q1949086) (← links)
• Sharpening constraint programming approaches for bit-vector theory (Q2011567) (← links)
• IPL: an integration property language for multi-model cyber-physical systems (Q2024345) (← links)
• On neural network equivalence checking using SMT solvers (Q2112128) (← links)
• Data abstraction: a general framework to handle program verification of data structures (Q2145329) (← links)
• Region analysis for deductive verification of C programs (Q2216720) (← links)
• Wombit: a portfolio bit-vector solver using word-level propagation (Q2323450) (← links)
• A layered algorithm for quantifier elimination from linear modular constraints (Q2363817) (← links)
• Metalevel algorithms for variant satisfiability (Q2413027) (← links)
• Preface to the special issue ``SI: satisfiability modulo theories'' (Q2441769) (← links)
• Abstract interpretation of microcontroller code: intervals meet congruences (Q2442953) (← links)
• Satisfiability in composition-nominative logics (Q2445092) (← links)
• SLAP: specification logic of actions with probability (Q2447174) (← links)
• Range and Set Abstraction using SAT (Q2814098) (← links)
• $$\mathsf {SC}^\mathsf{2} $$ : Satisfiability Checking Meets Symbolic Computation (Q2817292) (← links)
• Colors Make Theories Hard (Q2817916) (← links)
• Metalevel Algorithms for Variant Satisfiability (Q2827841) (← links)
• A Survey of Satisfiability Modulo Theory (Q2830018) (← links)
• Decision Procedures for Region Logic (Q2891431) (← links)
• Matching Multiplications in Bit-Vector Formulas (Q2961559) (← links)
• Mutation-Based Test Case Generation for Simulink Models (Q3066126) (← links)
• On the Generation of Positivstellensatz Witnesses in Degenerate Cases (Q3088010) (← links)
• Virtual Substitution for SMT-Solving (Q3088298) (← links)
• Reconstruction of Z3’s Bit-Vector Proofs in HOL4 and Isabelle/HOL (Q3100212) (← links)
• Propositional SAT Solving (Q3176367) (← links)
• SAT-Based Model Checking (Q3176368) (← links)
• Satisfiability Modulo Theories (Q3176369) (← links)
• Mining Backbone Literals in Incremental SAT (Q3453214) (← links)
• Integrating Simplex with Tableaux (Q3455763) (← links)
• Satisfiability Checking: Theory and Applications (Q4571125) (← links)
• (Q5009416) (← links)
• Partial Order Reduction for Deep Bug Finding in Synchronous Hardware (Q5039518) (← links)
• Loop invariants (Q5176169) (← links)