| Hits ?▲ |
Authors |
Title |
Venue |
Year |
Link |
Author keywords |
| 1 | Francesco Alberti, Silvio Ghilardi, Elena Pagani, Silvio Ranise, Gian Paolo Rossi |
Universal Guards, Relativization of Quantifiers, and Failure Models in Model Checking Modulo Theories.  |
JSAT  |
2012 |
DBLP BibTeX RDF |
|
| 1 | Roberto Bruttomesso, Silvio Ghilardi, Silvio Ranise |
From Strong Amalgamability to Modularity of Quantifier-Free Interpolation |
CoRR |
2012 |
DBLP BibTeX RDF |
|
| 1 | Roberto Bruttomesso, Silvio Ghilardi, Silvio Ranise |
Quantifier-Free Interpolation of a Theory of Arrays |
Logical Methods in Computer Science |
2012 |
DBLP DOI BibTeX RDF |
|
| 1 | Alessandro Armando, Silvio Ranise, Fatih Turkmen, Bruno Crispo |
Efficient run-time solving of RBAC user authorization queries: pushing the envelope. |
CODASPY |
2012 |
DBLP DOI BibTeX RDF |
|
| 1 | Francesco Alberti, Roberto Bruttomesso, Silvio Ghilardi, Silvio Ranise, Natasha Sharygina |
Lazy Abstraction with Interpolants for Arrays. |
LPAR |
2012 |
DBLP DOI BibTeX RDF |
|
| 1 | Roberto Bruttomesso, Alessandro Carioni, Silvio Ghilardi, Silvio Ranise |
Automated Analysis of Parametric Timing-Based Mutual Exclusion Algorithms. |
NASA Formal Methods |
2012 |
DBLP DOI BibTeX RDF |
|
| 1 | Michele Barletta, Alberto Calvi, Silvio Ranise, Luca Viganò, Luca Zanetti |
Workflow and Access Control Reloaded: a Declarative Specification Framework for the Automated Analysis of Web Services. |
Scalable Computing: Practice and Experience |
2011 |
DBLP BibTeX RDF |
|
| 1 | Christopher Lynch, Silvio Ranise, Christophe Ringeissen, Duc-Khanh Tran |
Automatic decidability and combinability. |
Inf. Comput. |
2011 |
DBLP DOI BibTeX RDF |
|
| 1 | Michele Barletta, Silvio Ranise, Luca Viganò |
A declarative two-level framework to specify and verify workflow and authorization policies in service-oriented architectures. |
Service Oriented Computing and Applications |
2011 |
DBLP DOI BibTeX RDF |
|
| 1 | Francesco Alberti, Alessandro Armando, Silvio Ranise |
ASASP: Automated Symbolic Analysis of Security Policies. |
CADE |
2011 |
DBLP DOI BibTeX RDF |
|
| 1 | Alessandro Armando, Silvio Ranise |
Automated Analysis of Infinite State Workflows with Access Control Policies. |
STM |
2011 |
DBLP DOI BibTeX RDF |
|
| 1 | Alessandro Carioni, Silvio Ghilardi, Silvio Ranise |
Automated Termination in Model Checking Modulo Theories. |
RP |
2011 |
DBLP DOI BibTeX RDF |
|
| 1 | Roberto Bruttomesso, Silvio Ghilardi, Silvio Ranise |
Rewriting-based Quantifier-free Interpolation for a Theory of Arrays. |
RTA |
2011 |
DBLP DOI BibTeX RDF |
|
| 1 | Roberto Bruttomesso, Silvio Ghilardi, Silvio Ranise |
A Combination of Rewriting and Constraint Solving for the Quantifier-Free Interpolation of Arrays with Integer Difference Constraints. |
FroCos |
2011 |
DBLP DOI BibTeX RDF |
|
| 1 | Alessandro Armando, Roberto Carbone, Silvio Ranise |
Automated Analysis of Semantic-Aware Access Control Policies: A Logic-Based Approach. |
ICSC |
2011 |
DBLP DOI BibTeX RDF |
semantic-aware access control, logic-based methods, automatic analysis |
| 1 | Francesco Alberti, Alessandro Armando, Silvio Ranise |
Efficient symbolic automated analysis of administrative attribute-based RBAC-policies. |
ASIACCS |
2011 |
DBLP DOI BibTeX RDF |
|
| 1 | Francesco Alberti, Silvio Ghilardi, Elena Pagani, Silvio Ranise, Gian Paolo Rossi |
Automated Support for the Design and Validation of Fault Tolerant Parameterized Systems: a case study. |
ECEASST |
2010 |
DBLP BibTeX RDF |
|
| 1 | Duc-Khanh Tran, Christophe Ringeissen, Silvio Ranise, Hélène Kirchner |
Combination of convex theories: Modularity, deduction completeness, and explanation. |
J. Symb. Comput. |
2010 |
DBLP DOI BibTeX RDF |
|
| 1 | Ranise Armando, Silvio Ranise |
Automated Symbolic Analysis of ARBAC-Policies (Extended Version) |
CoRR |
2010 |
DBLP BibTeX RDF |
|
| 1 | Silvio Ghilardi, Silvio Ranise |
Backward Reachability of Array-based Systems by SMT solving: Termination and Invariant Synthesis |
Logical Methods in Computer Science |
2010 |
DBLP DOI BibTeX RDF |
|
| 1 | Alberto Calvi, Silvio Ranise, Luca Viganò |
Automated Validation of Security-sensitive Web Services specified in BPEL and RBAC (Extended Version) |
CoRR |
2010 |
DBLP BibTeX RDF |
|
| 1 | Silvio Ghilardi, Silvio Ranise |
MCMT: A Model Checker Modulo Theories. |
IJCAR |
2010 |
DBLP DOI BibTeX RDF |
|
| 1 | Alberto Calvi, Silvio Ranise, Luca Viganò |
Automated Validation of Security-Sensitive Web Services Specified in BPEL and RBAC. |
SYNASC |
2010 |
DBLP DOI BibTeX RDF |
|
| 1 | Michele Barletta, Alberto Calvi, Silvio Ranise, Luca Viganò, Luca Zanetti |
WSSMT: Towards the Automated Analysis of Security-Sensitive Services and Applications. |
SYNASC |
2010 |
DBLP DOI BibTeX RDF |
|
| 1 | Alessandro Armando, Silvio Ranise |
Automated Symbolic Analysis of ARBAC-Policies. |
STM |
2010 |
DBLP DOI BibTeX RDF |
|
| 1 | Francesco Alberti, Silvio Ghilardi, Elena Pagani, Silvio Ranise, Gian Paolo Rossi |
Brief Announcement: Automated Support for the Design and Validation of Fault Tolerant Parameterized Systems - A Case Study. |
DISC |
2010 |
DBLP DOI BibTeX RDF |
|
| 1 | Clark Barrett, Leonardo Mendonça de Moura, Silvio Ranise, Aaron Stump, Cesare Tinelli |
The SMT-LIB Initiative and the Rise of SMT - (HVC 2010 Award Talk). |
Haifa Verification Conference |
2010 |
DBLP DOI BibTeX RDF |
|
| 1 | Silvio Ghilardi, Silvio Ranise, Thomas Valsecchi |
Light-Weight SMT-based Model Checking. |
Electr. Notes Theor. Comput. Sci. |
2009 |
DBLP DOI BibTeX RDF |
|
| 1 | Michele Barletta, Silvio Ranise, Luca Viganò |
Verifying the Interplay of Authorization Policies and Workflow in Service-Oriented Architectures (Full version) |
CoRR |
2009 |
DBLP BibTeX RDF |
|
| 1 | Alessandro Armando, Maria Paola Bonacina, Silvio Ranise, Stephan Schulz |
New results on rewrite-based satisfiability procedures. |
ACM Trans. Comput. Log. |
2009 |
DBLP DOI BibTeX RDF |
combination of theories, satisfiability modulo a theory, scalability, inference, termination, Automated reasoning, decision procedures, rewriting, superposition |
| 1 | Silvio Ranise, Ullrich Hustadt |
Preface. |
Ann. Math. Artif. Intell. |
2009 |
DBLP DOI BibTeX RDF |
|
| 1 | David Déharbe, Silvio Ranise |
Satisfiability solving for software verification. |
STTT |
2009 |
DBLP DOI BibTeX RDF |
Equational theorem proving, Boolean solving, Theory reasoning, Software verification |
| 1 | Michele Barletta, Silvio Ranise, Luca Viganò |
Verifying the Interplay of Authorization Policies and Workflow in Service-Oriented Architectures. |
CSE |
2009 |
DBLP DOI BibTeX RDF |
|
| 1 | Silvio Ghilardi, Silvio Ranise |
Goal-Directed Invariant Synthesis for Model Checking Modulo Theories. |
TABLEAUX |
2009 |
DBLP DOI BibTeX RDF |
|
| 1 | David Déharbe, Silvio Ranise, Jorgiano Vidal |
A Prototype Implementation of a Distributed Satisfiability Modulo Theories Solver in the ToolBus Framework. |
J. Braz. Comp. Soc. |
2008 |
DBLP DOI BibTeX RDF |
|
| 1 | Silvio Ghilardi, Enrica Nicolini, Silvio Ranise, Daniele Zucchelli |
Towards SMT Model Checking of Array-Based Systems. |
IJCAR |
2008 |
DBLP DOI BibTeX RDF |
|
| 1 | David Déharbe, Silvio Ranise, Jorgiano Vidal |
Distributing the Workload in a Lazy Theorem-Prover. |
Electr. Notes Theor. Comput. Sci. |
2007 |
DBLP DOI BibTeX RDF |
|
| 1 | Silvio Ghilardi, Enrica Nicolini, Silvio Ranise, Daniele Zucchelli |
Decision procedures for extensions of the theory of arrays. |
Ann. Math. Artif. Intell. |
2007 |
DBLP DOI BibTeX RDF |
Mathematics Subject Classifications (2000) 68T27, 03B25, 03B70, 68T15 |
| 1 | Silvio Ghilardi, Enrica Nicolini, Silvio Ranise, Daniele Zucchelli |
Combination Methods for Satisfiability and Model-Checking of Infinite-State Systems. |
CADE |
2007 |
DBLP DOI BibTeX RDF |
|
| 1 | Silvio Ranise, Christelle Scharff |
Building Extended Canonizers by Graph-Based Deduction. |
ICTAC |
2007 |
DBLP DOI BibTeX RDF |
|
| 1 | Silvio Ghilardi, Silvio Ranise, Enrica Nicolini, Daniele Zucchelli |
From Non-Disjoint Combination to Satisfiability and Model-Checking of Infinite State Systems. |
Deduction and Decision Procedures |
2007 |
DBLP BibTeX RDF |
|
| 1 | Silvio Ranise, Christophe Ringeissen, Duc-Khanh Tran |
Combining Proof-Producing Decision Procedures. |
FroCos |
2007 |
DBLP DOI BibTeX RDF |
|
| 1 | Silvio Ghilardi, Enrica Nicolini, Silvio Ranise, Daniele Zucchelli |
Noetherianity and Combination Problems. |
FroCos |
2007 |
DBLP DOI BibTeX RDF |
|
| 1 | Marco Bozzano, Roberto Bruttomesso, Alessandro Cimatti, Tommi A. Junttila, Silvio Ranise, Peter van Rossum, Roberto Sebastiani |
Efficient theory combination via boolean search. |
Inf. Comput. |
2006 |
DBLP DOI BibTeX RDF |
|
| 1 | Alessandro Armando, Maria Paola Bonacina, Silvio Ranise, Stephan Schulz |
New results on rewrite-based satisfiability procedures |
CoRR |
2006 |
DBLP BibTeX RDF |
|
| 1 | Bernhard Beckert, Tony Hoare, Reiner Hähnle, Douglas R. Smith, Cordell Green, Silvio Ranise, Cesare Tinelli, Thomas Ball, Sriram K. Rajamani |
Intelligent Systems and Formal Methods in Software Engineering. |
IEEE Intelligent Systems |
2006 |
DBLP DOI BibTeX RDF |
deductive software verification, software engineering, formal methods, program verification, software synthesis, satisfiability modulo theories |
| 1 | Silvio Ranise, Calogero G. Zarba |
A Theory of Singly-Linked Lists and its Extensible Decision Procedure. |
SEFM |
2006 |
DBLP DOI BibTeX RDF |
|
| 1 | Maria Paola Bonacina, Silvio Ghilardi, Enrica Nicolini, Silvio Ranise, Daniele Zucchelli |
Decidability and Undecidability Results for Nelson-Oppen and Rewrite-Based Decision Procedures. |
IJCAR |
2006 |
DBLP DOI BibTeX RDF |
|
| 1 | Hélène Kirchner, Silvio Ranise, Christophe Ringeissen, Duc-Khanh Tran |
Automatic Combinability of Rewriting-Based Satisfiability Procedures. |
LPAR |
2006 |
DBLP DOI BibTeX RDF |
|
| 1 | David Déharbe, Pascal Fontaine, Silvio Ranise, Christophe Ringeissen |
Decision Procedures for the Formal Analysis of Software. |
ICTAC |
2006 |
DBLP DOI BibTeX RDF |
|
| 1 | Silvio Ghilardi, Enrica Nicolini, Silvio Ranise, Daniele Zucchelli |
Deciding Extensions of the Theory of Arrays by Integrating Decision Procedures and Instantiation Strategies. |
JELIA |
2006 |
DBLP DOI BibTeX RDF |
|
| 1 | Wolfgang Ahrendt, Peter Baumgartner, Hans de Nivelle, Silvio Ranise, Cesare Tinelli |
Preface. |
Electr. Notes Theor. Comput. Sci. |
2005 |
DBLP DOI BibTeX RDF |
|
| 1 | Hélène Kirchner, Silvio Ranise, Christophe Ringeissen, Duc-Khanh Tran |
On Superposition-Based Satisfiability Procedures and Their Combination. |
ICTAC |
2005 |
DBLP DOI BibTeX RDF |
|
| 1 | Silvio Ranise, Christophe Ringeissen, Calogero G. Zarba |
Combining Data Structures with Nonstably Infinite Theories Using Many-Sorted Logic. |
FroCos |
2005 |
DBLP DOI BibTeX RDF |
|
| 1 | Alessandro Armando, Maria Paola Bonacina, Silvio Ranise, Stephan Schulz |
On a Rewriting Approach to Satisfiability Procedures: Extension, Combination of Theories and an Experimental Appraisal. |
FroCos |
2005 |
DBLP DOI BibTeX RDF |
|
| 1 | Alessandro Armando, Luca Compagna, Silvio Ranise |
Rewriting and Decision Procedure Laboratory: Combining Rewriting, Satisfiability Checking, and Lemma Speculation. |
Mechanizing Mathematical Reasoning |
2005 |
DBLP DOI BibTeX RDF |
|
| 1 | Marco Bozzano, Roberto Bruttomesso, Alessandro Cimatti, Tommi A. Junttila, Silvio Ranise, Peter van Rossum, Roberto Sebastiani |
Efficient Satisfiability Modulo Theories via Delayed Theory Combination. |
CAV |
2005 |
DBLP DOI BibTeX RDF |
|
| 1 | Jean-François Couchot, David Déharbe, Alain Giorgetti, Silvio Ranise |
Scalable Automated Proving and Debugging of Set-Based Specifications. |
J. Braz. Comp. Soc. |
2004 |
DBLP DOI BibTeX RDF |
|
| 1 | Jean-François Couchot, Frédéric Dadeau, David Déharbe, Alain Giorgetti, Silvio Ranise |
Proving and Debugging Set-Based Specifications. |
Electr. Notes Theor. Comput. Sci. |
2004 |
DBLP DOI BibTeX RDF |
|
| 1 | Pascal Fontaine, Silvio Ranise, Calogero G. Zarba |
Combining Lists with Non-stably Infinite Theories. |
LPAR |
2004 |
DBLP DOI BibTeX RDF |
|
| 1 | Silvio Ranise, Christophe Ringeissen, Duc-Khanh Tran |
Nelson-Oppen, Shostak and the Extended Canonizer: A Family Picture with a Newborn. |
ICTAC |
2004 |
DBLP DOI BibTeX RDF |
|
| 1 | David Déharbe, Abdessamad Imine, Silvio Ranise |
Abstraction-Driven Verification of Array Programs. |
AISC |
2004 |
DBLP DOI BibTeX RDF |
|
| 1 | Alessandro Armando, Silvio Ranise |
Constraint contextual rewriting. |
J. Symb. Comput. |
2003 |
DBLP DOI BibTeX RDF |
|
| 1 | Alessandro Armando, Silvio Ranise, Michaël Rusinowitch |
A rewriting approach to satisfiability procedures. |
Inf. Comput. |
2003 |
DBLP DOI BibTeX RDF |
|
| 1 | Silvio Ranise, David Déharbe |
Applying Light-Weight Theorem Proving to Debugging and Verifying Pointer Programs. |
Electr. Notes Theor. Comput. Sci. |
2003 |
DBLP DOI BibTeX RDF |
|
| 1 | David Déharbe, Silvio Ranise |
Light-Weight Theorem Proving for Debugging and Verifying Units of Code. |
SEFM |
2003 |
DBLP DOI BibTeX RDF |
|
| 1 | Silvio Ranise |
Combining Generic and Domain Specific Reasoning by Using Contexts. |
AISC |
2002 |
DBLP DOI BibTeX RDF |
|
| 1 | Alessandro Armando, Alessandro Coglio, Fausto Giunchiglia, Silvio Ranise |
The Control Layer in Open Mechanized Reasoning Systems: Annotations and Tactics. |
J. Symb. Comput. |
2001 |
DBLP DOI BibTeX RDF |
|
| 1 | Alessandro Armando, Silvio Ranise |
A Practical Extension Mechanism for Decision Procedures: the Case Study of Universal Presburger Arithmetic. |
J. UCS |
2001 |
DBLP BibTeX RDF |
|
| 1 | Alessandro Armando, Luca Compagna, Silvio Ranise |
System Description: RDL : Rewrite and Decision Procedure Laboratory. |
IJCAR |
2001 |
DBLP DOI BibTeX RDF |
|
| 1 | Alessandro Armando, Silvio Ranise, Michaël Rusinowitch |
Uniform Derivation of Decision Procedures by Superposition. |
CSL |
2001 |
DBLP DOI BibTeX RDF |
Arrays with Extensionality, Term Rewriting, Decision Procedures, Homomorphism, Automated Deduction, Lists, Superposition, Equational Logic |
| 1 | Alessandro Armando, Felice Peccia, Silvio Ranise |
The Phase Transition of the Linear Inequalities Problem. |
CP |
2001 |
DBLP DOI BibTeX RDF |
|
| 1 | Alessandro Armando, Silvio Ranise |
Termination of Constraint Contextual Rewriting. |
FroCos |
2000 |
DBLP DOI BibTeX RDF |
|
| 1 | Alessandro Armando, Silvio Ranise |
From Integrated Reasoning Specialists to ``Plug-and-Play'' Reasoning Components. |
AISC |
1998 |
DBLP DOI BibTeX RDF |
|
| 1 | Alessandro Armando, Erica Melis, Silvio Ranise |
Constraint Solving in Logic Programming and in Automated Deduction: A Comparison. |
AIMSA |
1998 |
DBLP DOI BibTeX RDF |
|
![[Valid RSS]](Pics/valid-rss.png "Validate my RSS feed")