The following pages link to Silvio Ranise (Q219438):
Displaying 49 items.
- On the verification of security-aware E-services (Q429592) (← links)
- An extension of lazy abstraction with interpolation for programs with arrays (Q479820) (← links)
- Combination of convex theories: modularity, deduction completeness, and explanation (Q1041593) (← links)
- A rewriting approach to satisfiability procedures. (Q1401930) (← links)
- Constraint contextual rewriting. (Q1404984) (← links)
- Efficient theory combination via Boolean search (Q2432765) (← links)
- Symbolic backward reachability with effectively propositional logic. Application to security policy analysis (Q2441771) (← links)
- Decision procedures for extensions of the theory of arrays (Q2457800) (← links)
- A practical extension mechanism for decision procedures: The case study of universal Presburger arithmetic (Q2709804) (← links)
- Communication protocols for mathematical services based on KQML and OMRS (Q2751535) (← links)
- Universal guards, relativization of quantifiers, and failure models in model checking modulo theories (Q2786907) (← links)
- Automated termination in model-checking modulo theories (Q2841996) (← links)
- Verification of Composed Array-Based Systems with Applications to Security-Aware Workflows (Q2849480) (← links)
- Distributing the workload in a lazy theorem-prover (Q2870323) (← links)
- Quantifier-free interpolation of a theory of arrays (Q2887061) (← links)
- Lazy Abstraction with Interpolants for Arrays (Q2891439) (← links)
- From Strong Amalgamability to Modularity of Quantifier-Free Interpolation (Q2908483) (← links)
- Backward Reachability of Array-based Systems by SMT solving: Termination and Invariant Synthesis (Q3081445) (← links)
- Automated Termination in Model Checking Modulo Theories (Q3172869) (← links)
- A Combination of Rewriting and Constraint Solving for the Quantifier-Free Interpolation of Arrays with Integer Difference Constraints (Q3172885) (← links)
- Noetherianity and Combination Problems (Q3525011) (← links)
- Combining Proof-Producing Decision Procedures (Q3525013) (← links)
- Building Extended Canonizers by Graph-Based Deduction (Q3525104) (← links)
- Deciding Extensions of the Theory of Arrays by Integrating Decision Procedures and Instantiation Strategies (Q3533130) (← links)
- Towards SMT Model Checking of Array-Based Systems (Q3541687) (← links)
- Combination Methods for Satisfiability and Model-Checking of Infinite-State Systems (Q3608784) (← links)
- Decidability and Undecidability Results for Nelson-Oppen and Rewrite-Based Decision Procedures (Q3613431) (← links)
- Goal-Directed Invariant Synthesis for Model Checking Modulo Theories (Q3648730) (← links)
- (Q4475649) (← links)
- (Q4518863) (← links)
- (Q4539649) (← links)
- (Q4785507) (← links)
- (Q4808727) (← links)
- Applying Light-Weight Theorem Proving to Debugging and Verifying Pointer Programs (Q4916225) (← links)
- Light-Weight SMT-based Model Checking (Q5178977) (← links)
- New results on rewrite-based satisfiability procedures (Q5277822) (← links)
- Automatic Combinability of Rewriting-Based Satisfiability Procedures (Q5387918) (← links)
- Rewriting-based Quantifier-free Interpolation for a Theory of Arrays. (Q5389080) (← links)
- Theoretical Aspects of Computing – ICTAC 2005 (Q5395131) (← links)
- Quantifier-free interpolation in combinations of equality interpolating theories (Q5410332) (← links)
- Artificial Intelligence and Symbolic Computation (Q5464711) (← links)
- Frontiers of Combining Systems (Q5491892) (← links)
- Frontiers of Combining Systems (Q5491893) (← links)
- Logic for Programming, Artificial Intelligence, and Reasoning (Q5705949) (← links)
- Theoretical Aspects of Computing - ICTAC 2004 (Q5709987) (← links)
- Computer Aided Verification (Q5716575) (← links)
- Mechanizing Mathematical Reasoning (Q5717459) (← links)
- MCMT: A Model Checker Modulo Theories (Q5747748) (← links)
- The control layer in open mechanized reasoning systems: Annotations and tactics (Q5950930) (← links)
