Pages that link to "Item:Q2958376"

The following pages link to Abstract Logical Model Checking of Infinite-State Systems Using Narrowing (Q2958376):

Displaying 31 items.

• Rewriting modulo SMT and open system analysis (Q347384) (← links)
• A Maude environment for CafeOBJ (Q520244) (← links)
• Equational unification and matching, and symbolic reachability analysis in Maude 3.2 (system description) (Q2104541) (← links)
• Symbolic computation in Maude: some tapas (Q2119100) (← links)
• Strategies, model checking and branching-time properties in Maude (Q2239275) (← links)
• Generalized rewrite theories, coherence completion, and symbolic methods (Q2291817) (← links)
• Programming and symbolic computation in Maude (Q2291818) (← links)
• Infinite-state invariant checking with IC3 and predicate abstraction (Q2363814) (← links)
• Executing and verifying higher-order functional-imperative programs in Maude (Q2409629) (← links)
• Optimization of rewrite theories by equational partial evaluation (Q2667190) (← links)
• Verification of the ROS NavFn planner using executable specification languages (Q2693303) (← links)
• (Q2723916) (← links)
• Built-in Variant Generation and Unification, and Their Applications in Maude 2.7 (Q2817918) (← links)
• Two Decades of Maude (Q2945709) (← links)
• Generic Proof Scores for Generate & Check Method in CafeOBJ (Q2945712) (← links)
• Verifying Reachability-Logic Properties on Rewriting-Logic Specifications (Q2945720) (← links)
• (Q5020553) (← links)
• (Q5020960) (← links)
• All-Path Reachability Logic (Q5170834) (← links)
• Generate & Check Method for Verifying Transition Systems in CafeOBJ (Q5256348) (← links)
• Model Checking TLR* Guarantee Formulas on Infinite Systems (Q5403070) (← links)
• Functional Logic Programming in Maude (Q5403075) (← links)
• Mechanical Analysis of Reliable Communication in the Alternating Bit Protocol Using the Maude Invariant Analyzer Tool (Q5403085) (← links)
• Theorem Proving Based on Proof Scores for Rewrite Theory Specifications of OTSs (Q5403086) (← links)
• Reducing non-occurrence of specified runtime errors to all-path reachability problems of constrained rewriting (Q6052950) (← links)
• Symbolic Specialization of Rewriting Logic Theories with <tt>Presto</tt> (Q6063888) (← links)
• Variants and satisfiability in the infinitary unification wonderland (Q6113018) (← links)
• Symbolic analysis and parameter synthesis for time Petri nets using Maude and SMT solving (Q6535202) (← links)
• Building correct-by-construction systems with formal patterns (Q6562511) (← links)
• A rewriting-logic-with-SMT-based formal analysis and parameter synthesis framework for parametric time Petri nets (Q6622141) (← links)
• Maude2Lean: theorem proving for Maude specifications using Lean (Q6643468) (← links)