Silvio Ranise

Silvio Ranise: Symbolic backward reachability with effectively propositional logic - Applications to security policy analysis. Formal Methods in System Design 42(1): 24-45 (2013)

Roberto Bruttomesso, Silvio Ghilardi, Silvio Ranise: Quantifier-Free Interpolation of a Theory of Arrays. Logical Methods in Computer Science 8(2) (2012)

Alessandro Armando, Silvio Ranise: Scalable automated symbolic analysis of administrative role-based access control policies by SMT solving. Journal of Computer Security 20(4): 309-352 (2012)

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 8(1/2): 29-61 (2012)

Silvio Ranise: On the verification of security-aware E-services. J. Symb. Comput. 47(9): 1066-1088 (2012)

Roberto Bruttomesso, Silvio Ghilardi, Silvio Ranise: From Strong Amalgamability to Modularity of Quantifier-Free Interpolation. IJCAR 2012: 118-133

Francesco Alberti, Roberto Bruttomesso, Silvio Ghilardi, Silvio Ranise, Natasha Sharygina: SAFARI: SMT-Based Abstraction for Arrays with Interpolants. CAV 2012: 679-685

Alessandro Armando, Silvio Ranise, Fatih Turkmen, Bruno Crispo: Efficient run-time solving of RBAC user authorization queries: pushing the envelope. CODASPY 2012: 241-248

Alessandro Armando, Silvio Ranise: Automated and Efficient Analysis of Role-Based Access Control with Attributes. DBSec 2012: 25-40

Francesco Alberti, Roberto Bruttomesso, Silvio Ghilardi, Silvio Ranise, Natasha Sharygina: Lazy Abstraction with Interpolants for Arrays. LPAR 2012: 46-61

Roberto Bruttomesso, Alessandro Carioni, Silvio Ghilardi, Silvio Ranise: Automated Analysis of Parametric Timing-Based Mutual Exclusion Algorithms. NASA Formal Methods 2012: 279-294

Silvio Ranise, Alessandro Armando: On the Automated Analysis of Safety in Usage Control: A New Decidability Result. NSS 2012: 15-28

Roberto Bruttomesso, Silvio Ghilardi, Silvio Ranise: From Strong Amalgamability to Modularity of Quantifier-Free Interpolation. CoRR abs/1203.3730 (2012)

Michele Barletta, Silvio Ranise, Luca Viganò: Automated Analysis of Scenario-based Specifications of Distributed Access Control Policies with Non-Mechanizable Activities (Extended Version). CoRR abs/1206.3180 (2012)

Christopher Lynch, Silvio Ranise, Christophe Ringeissen, Duc-Khanh Tran: Automatic decidability and combinability. Inf. Comput. 209(7): 1026-1047 (2011)

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 12(1) (2011)

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 5(2): 105-137 (2011)

Francesco Alberti, Alessandro Armando, Silvio Ranise: ASASP: Automated Symbolic Analysis of Security Policies. CADE 2011: 26-33

Francesco Alberti, Alessandro Armando, Silvio Ranise: Efficient symbolic automated analysis of administrative attribute-based RBAC-policies. ASIACCS 2011: 165-175

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: 103-118

Alessandro Carioni, Silvio Ghilardi, Silvio Ranise: Automated Termination in Model Checking Modulo Theories. RP 2011: 110-124

Roberto Bruttomesso, Silvio Ghilardi, Silvio Ranise: Rewriting-based Quantifier-free Interpolation for a Theory of Arrays. RTA 2011: 171-186

Alessandro Armando, Roberto Carbone, Silvio Ranise: Automated Analysis of Semantic-Aware Access Control Policies: A Logic-Based Approach. ICSC 2011: 356-363

Alessandro Armando, Silvio Ranise: Automated Analysis of Infinite State Workflows with Access Control Policies. STM 2011: 157-174

Silvio Ghilardi, Silvio Ranise: Backward Reachability of Array-based Systems by SMT solving: Termination and Invariant Synthesis. Logical Methods in Computer Science 6(4) (2010)

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 35 (2010)

Duc-Khanh Tran, Christophe Ringeissen, Silvio Ranise, Hélène Kirchner: Combination of convex theories: Modularity, deduction completeness, and explanation. J. Symb. Comput. 45(2): 261-286 (2010)

Silvio Ghilardi, Silvio Ranise: MCMT: A Model Checker Modulo Theories. IJCAR 2010: 22-29

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: 3

Alessandro Armando, Silvio Ranise: Automated Symbolic Analysis of ARBAC-Policies. STM 2010: 17-34

Michele Barletta, Alberto Calvi, Silvio Ranise, Luca Viganò, Luca Zanetti: WSSMT: Towards the Automated Analysis of Security-Sensitive Services and Applications. SYNASC 2010: 417-424

Alberto Calvi, Silvio Ranise, Luca Viganò: Automated Validation of Security-Sensitive Web Services Specified in BPEL and RBAC. SYNASC 2010: 456-464

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: 392-394

Alberto Calvi, Silvio Ranise, Luca Viganò: Automated Validation of Security-sensitive Web Services specified in BPEL and RBAC (Extended Version). CoRR abs/1009.4625 (2010)

Ranise Armando, Silvio Ranise: Automated Symbolic Analysis of ARBAC-Policies (Extended Version). CoRR abs/1012.5590 (2010)

Silvio Ranise, Ullrich Hustadt: Preface. Ann. Math. Artif. Intell. 55(1-2): 1-2 (2009)

Silvio Ghilardi, Silvio Ranise, Thomas Valsecchi: Light-Weight SMT-based Model Checking. Electr. Notes Theor. Comput. Sci. 250(2): 85-102 (2009)

David Déharbe, Silvio Ranise: Satisfiability solving for software verification. STTT 11(3): 255-260 (2009)

Alessandro Armando, Maria Paola Bonacina, Silvio Ranise, Stephan Schulz: New results on rewrite-based satisfiability procedures. ACM Trans. Comput. Log. 10(1) (2009)

Michele Barletta, Silvio Ranise, Luca Viganò: Verifying the Interplay of Authorization Policies and Workflow in Service-Oriented Architectures. CSE (3) 2009: 289-296

Silvio Ghilardi, Silvio Ranise: Goal-Directed Invariant Synthesis for Model Checking Modulo Theories. TABLEAUX 2009: 173-188

Michele Barletta, Silvio Ranise, Luca Viganò: Verifying the Interplay of Authorization Policies and Workflow in Service-Oriented Architectures (Full version). CoRR abs/0906.4570 (2009)

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. 14(1): 71-86 (2008)

Silvio Ghilardi, Enrica Nicolini, Silvio Ranise, Daniele Zucchelli: Towards SMT Model Checking of Array-Based Systems. IJCAR 2008: 67-82

Silvio Ghilardi, Enrica Nicolini, Silvio Ranise, Daniele Zucchelli: Decision procedures for extensions of the theory of arrays. Ann. Math. Artif. Intell. 50(3-4): 231-254 (2007)

David Déharbe, Silvio Ranise, Jorgiano Vidal: Distributing the Workload in a Lazy Theorem-Prover. Electr. Notes Theor. Comput. Sci. 184: 21-37 (2007)

Silvio Ghilardi, Enrica Nicolini, Silvio Ranise, Daniele Zucchelli: Combination Methods for Satisfiability and Model-Checking of Infinite-State Systems. CADE 2007: 362-378

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

Silvio Ghilardi, Enrica Nicolini, Silvio Ranise, Daniele Zucchelli: Noetherianity and Combination Problems. FroCoS 2007: 206-220

Silvio Ranise, Christophe Ringeissen, Duc-Khanh Tran: Combining Proof-Producing Decision Procedures. FroCoS 2007: 237-251

Silvio Ranise, Christelle Scharff: Building Extended Canonizers by Graph-Based Deduction. ICTAC 2007: 440-454

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 21(6): 71-81 (2006)

Marco Bozzano, Roberto Bruttomesso, Alessandro Cimatti, Tommi A. Junttila, Silvio Ranise, Peter van Rossum, Roberto Sebastiani: Efficient theory combination via boolean search. Inf. Comput. 204(10): 1493-1525 (2006)

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: 513-527

David Déharbe, Pascal Fontaine, Silvio Ranise, Christophe Ringeissen: Decision Procedures for the Formal Analysis of Software. ICTAC 2006: 366-370

Silvio Ghilardi, Enrica Nicolini, Silvio Ranise, Daniele Zucchelli: Deciding Extensions of the Theory of Arrays by Integrating Decision Procedures and Instantiation Strategies. JELIA 2006: 177-189

Hélène Kirchner, Silvio Ranise, Christophe Ringeissen, Duc-Khanh Tran: Automatic Combinability of Rewriting-Based Satisfiability Procedures. LPAR 2006: 542-556

Silvio Ranise, Calogero G. Zarba: A Theory of Singly-Linked Lists and its Extensible Decision Procedure. SEFM 2006: 206-215

Alessandro Armando, Maria Paola Bonacina, Silvio Ranise, Stephan Schulz: New results on rewrite-based satisfiability procedures. CoRR abs/cs/0604054 (2006)

Wolfgang Ahrendt, Peter Baumgartner, Hans de Nivelle, Silvio Ranise, Cesare Tinelli: Preface. Electr. Notes Theor. Comput. Sci. 125(3): 1-2 (2005)

Alessandro Armando, Luca Compagna, Silvio Ranise: Rewriting and Decision Procedure Laboratory: Combining Rewriting, Satisfiability Checking, and Lemma Speculation. Mechanizing Mathematical Reasoning 2005: 30-45

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: 335-349

Silvio Ranise, Christophe Ringeissen, Calogero G. Zarba: Combining Data Structures with Nonstably Infinite Theories Using Many-Sorted Logic. FroCoS 2005: 48-64

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: 65-80

Hélène Kirchner, Silvio Ranise, Christophe Ringeissen, Duc-Khanh Tran: On Superposition-Based Satisfiability Procedures and Their Combination. ICTAC 2005: 594-608

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. 95: 189-208 (2004)

Jean-François Couchot, David Déharbe, Alain Giorgetti, Silvio Ranise: Scalable Automated Proving and Debugging of Set-Based Specifications. J. Braz. Comp. Soc. 9(2): 17-36 (2004)

David Déharbe, Abdessamad Imine, Silvio Ranise: Abstraction-Driven Verification of Array Programs. AISC 2004: 271-275

Silvio Ranise, Christophe Ringeissen, Duc-Khanh Tran: Nelson-Oppen, Shostak and the Extended Canonizer: A Family Picture with a Newborn. ICTAC 2004: 372-386

Pascal Fontaine, Silvio Ranise, Calogero G. Zarba: Combining Lists with Non-stably Infinite Theories. LPAR 2004: 51-66

Silvio Ranise, David Déharbe: Applying Light-Weight Theorem Proving to Debugging and Verifying Pointer Programs. Electr. Notes Theor. Comput. Sci. 86(1): 105-119 (2003)

Alessandro Armando, Silvio Ranise, Michaël Rusinowitch: A rewriting approach to satisfiability procedures. Inf. Comput. 183(2): 140-164 (2003)

Alessandro Armando, Silvio Ranise: Constraint contextual rewriting. J. Symb. Comput. 36(1-2): 193-216 (2003)

David Déharbe, Silvio Ranise: Light-Weight Theorem Proving for Debugging and Verifying Units of Code. SEFM 2003: 220-228

Silvio Ranise: Combining Generic and Domain Specific Reasoning by Using Contexts. AISC 2002: 305-318

Alessandro Armando, Alessandro Coglio, Fausto Giunchiglia, Silvio Ranise: The Control Layer in Open Mechanized Reasoning Systems: Annotations and Tactics. J. Symb. Comput. 32(4): 305-332 (2001)

Alessandro Armando, Silvio Ranise: A Practical Extension Mechanism for Decision Procedures: the Case Study of Universal Presburger Arithmetic. J. UCS 7(2): 124-140 (2001)

Alessandro Armando, Luca Compagna, Silvio Ranise: System Description: RDL : Rewrite and Decision Procedure Laboratory. IJCAR 2001: 663-669

Alessandro Armando, Felice Peccia, Silvio Ranise: The Phase Transition of the Linear Inequalities Problem. CP 2001: 422-432

Alessandro Armando, Silvio Ranise, Michaël Rusinowitch: Uniform Derivation of Decision Procedures by Superposition. CSL 2001: 513-527

Alessandro Armando, Silvio Ranise: Termination of Constraint Contextual Rewriting. FroCoS 2000: 47-61

Alessandro Armando, Erica Melis, Silvio Ranise: Constraint Solving in Logic Programming and in Automated Deduction: A Comparison. AIMSA 1998: 28-38

Alessandro Armando, Silvio Ranise: From Integrated Reasoning Specialists to ``Plug-and-Play'' Reasoning Components. AISC 1998: 42-54