Silvio Ranise

Orcid: 0000-0001-7269-9285

Affiliations:
  • INRIA, France


According to our database1, Silvio Ranise authored at least 191 papers between 1998 and 2024.

Collaborative distances:
  • Dijkstra number2 of two.
  • Erdős number3 of four.

Timeline

Legend:

Book 
In proceedings 
Article 
PhD thesis 
Dataset
Other 

Links

Online presence:

On csauthors.net:

Bibliography

2024
On Cryptographic Mechanisms for the Selective Disclosure of Verifiable Credentials.
CoRR, 2024

Multi-Objective Microservice Orchestration: Balancing Security and Performance in CCAM.
Proceedings of the 27th Conference on Innovation in Clouds, Internet and Networks, 2024

2023
Identifying and quantifying trade-offs in multi-stakeholder risk evaluation with applications to the data protection impact assessment of the GDPR.
Comput. Secur., June, 2023

A First Appraisal of Cryptographic Mechanisms for the Selective Disclosure of Verifiable Credentials.
Proceedings of the 20th International Conference on Security and Cryptography, 2023

Assurance, Consent and Access Control for Privacy-Aware OIDC Deployments.
Proceedings of the Data and Applications Security and Privacy XXXVII, 2023

Control is Nothing Without Trust a First Look into Digital Identity Wallet Trends.
Proceedings of the Data and Applications Security and Privacy XXXVII, 2023

Cross-Domain Sharing of User Claims: A Design Proposal for OpenID Connect Attribute Authorities.
Proceedings of the 18th International Conference on Availability, Reliability and Security, 2023

2022
Smart Card-Based Identity Management Protocols for V2V and V2I Communications in CCAM: A Systematic Literature Review.
IEEE Trans. Intell. Transp. Syst., 2022

Formal Modelling and Automated Trade-off Analysis of Enforcement Architectures for Cryptographic Access Control in the Cloud.
ACM Trans. Priv. Secur., 2022

Empirical Validation on the Usability of Security Reports for Patching TLS Misconfigurations: User- and Case-Studies on Actionable Mitigations.
J. Wirel. Mob. Networks Ubiquitous Comput. Dependable Appl., 2022

Best current practices for OAuth/OIDC Native Apps: A study of their adoption in popular providers and top-ranked Android clients.
J. Inf. Secur. Appl., 2022

Extending access control in AWS IoT through event-driven functions: an experimental evaluation using a smart lock system.
Int. J. Inf. Sec., 2022

Demo: TLSAssistant v2: A Modular and Extensible Framework for Securing TLS.
Proceedings of the SACMAT '22: The 27th ACM Symposium on Access Control Models and Technologies, New York, NY, USA, June 8, 2022

End-to-End Protection of IoT Communications Through Cryptographic Enforcement of Access Control Policies.
Proceedings of the Data and Applications Security and Privacy XXXVI, 2022

A Modular and Extensible Framework for Securing TLS.
Proceedings of the CODASPY '22: Twelveth ACM Conference on Data and Application Security and Privacy, Baltimore, MD, USA, April 24, 2022

SoK: A Survey on Technological Trends for (pre)Notified eIDAS Electronic Identity Schemes.
Proceedings of the ARES 2022: The 17th International Conference on Availability, Reliability and Security, Vienna,Austria, August 23, 2022

Distributed Enforcement of Access Control policies in Intelligent Transportation System (ITS) for Situation Awareness.
Proceedings of the ARES 2022: The 17th International Conference on Availability, Reliability and Security, Vienna,Austria, August 23, 2022

2021
Safety-Related Cooperative, Connected, and Automated Mobility Services: Interplay Between Functional and Security Requirements.
IEEE Veh. Technol. Mag., 2021

Blockchain Based RAN Data Sharing.
Proceedings of the IEEE International Conference on Smart Data Services, 2021

Assessing the Effectiveness of the Shared Responsibility Model for Cloud Databases: the Case of Google's Firebase.
Proceedings of the IEEE International Conference on Smart Data Services, 2021

A Framework for Security and Risk Analysis of Enrollment Procedures: Application to Fully-remote Solutions based on eDocuments.
Proceedings of the 18th International Conference on Security and Cryptography, 2021

Can Data Subject Perception of Privacy Risks Be Useful in a Data Protection Impact Assessment?
Proceedings of the 18th International Conference on Security and Cryptography, 2021

Cryptographic Enforcement of Access Control Policies in the Cloud: Implementation and Experimental Assessment.
Proceedings of the 18th International Conference on Security and Cryptography, 2021

Asset Sensitivity for Aligning Risk Assessment Across Multiple Units in Complex Organizations.
Proceedings of the Foundations and Practice of Security - 14th International Symposium, 2021

Integrating a Pentesting Tool for IdM Protocols in a Continuous Delivery Pipeline.
Proceedings of the Emerging Technologies for Authorization and Authentication, 2021

Automated Risk Assessment and What-if Analysis of OpenID Connect and OAuth 2.0 Deployments.
Proceedings of the Data and Applications Security and Privacy XXXV, 2021

Secure Pull Printing with QR Codes and National eID Cards: A Software-oriented Design and an Open-source Implementation.
Proceedings of the CODASPY '21: Eleventh ACM Conference on Data and Application Security and Privacy, 2021

DoS Attacks in Available MQTT Implementations: Investigating the Impact on Brokers and Devices, and supported Anti-DoS Protections.
Proceedings of the ARES 2021: The 16th International Conference on Availability, 2021

Do Security Reports Meet Usability?: Lessons Learned from Using Actionable Mitigations for Patching TLS Misconfigurations.
Proceedings of the ARES 2021: The 16th International Conference on Availability, 2021

2020
Formal Analysis of Mobile Multi-Factor Authentication with Single Sign-On Login.
ACM Trans. Priv. Secur., 2020

SARA: Secure Asynchronous Remote Attestation for IoT Systems.
IEEE Trans. Inf. Forensics Secur., 2020

Blockchain Tree as Solution for Distributed Storage of Personal ID Data and Document Access Control.
Sensors, 2020

Merging Datasets of CyberSecurity Incidents for Fun and Insight.
Frontiers Big Data, 2020

Collective Remote Attestation at the Internet of Things Scale: State-of-the-Art and Future Challenges.
IEEE Commun. Surv. Tutorials, 2020

Attestation-enabled secure and scalable routing protocol for IoT networks.
Ad Hoc Networks, 2020

Deploying Access Control Enforcement for IoT in the Cloud-Edge Continuum with the help of the CAP Theorem.
Proceedings of the 25th ACM Symposium on Access Control Models and Technologies, 2020

Multi-Stakeholder Cybersecurity Risk Assessment for Data Protection.
Proceedings of the 17th International Joint Conference on e-Business and Telecommunications, 2020

Automated and Secure Integration of the OpenID Connect iGov Profile in Mobile Native Applications.
Proceedings of the Emerging Technologies for Authorization and Authentication, 2020

Verifiable Contracting - A Use Case for Onboarding and Contract Offering in Financial Services with eIDAS and Verifiable Credentials.
Proceedings of the Computer Security - ESORICS 2020 International Workshops, 2020

Micro-Id-Gym: A Flexible Tool for Pentesting Identity Management Protocols in the Wild and in the Laboratory.
Proceedings of the Emerging Technologies for Authorization and Authentication, 2020

TLSAssistant Goes FINSEC A Security Platform Integration Extending Threat Intelligence Language.
Proceedings of the Cyber-Physical Security for Critical Infrastructures Protection, 2020

The Good, the Bad and the (Not So) Ugly of Out-of-Band Authentication with eID Cards and Push Notifications: Design, Formal and Risk Analysis.
Proceedings of the CODASPY '20: Tenth ACM Conference on Data and Application Security and Privacy, 2020

Exploring Architectures for Cryptographic Access Control Enforcement in the Cloud for Fun and Optimization.
Proceedings of the ASIA CCS '20: The 15th ACM Asia Conference on Computer and Communications Security, 2020

Security Considerations on 5G-Enabled Back-Situation Awareness for CCAM.
Proceedings of the 3rd IEEE 5G World Forum, 2020

2019
Blockchain Tree for eHealth.
CoRR, 2019

Audit-Based Access Control with a Distributed Ledger: Applications to Healthcare Organizations.
Proceedings of the Security and Trust Management - 15th International Workshop, 2019

MQTTSA: A Tool for Automatically Assisting the Secure Deployments of MQTT Brokers.
Proceedings of the 2019 IEEE World Congress on Services, 2019

Tool-Assisted Risk Analysis for Data Protection Impact Assessment.
Proceedings of the Privacy and Identity Management. Data for Better Living: AI and Privacy, 2019

Remote Attestation as a Service for IoT.
Proceedings of the Sixth International Conference on Internet of Things: Systems, 2019

Learning from Others' Mistakes: An Analysis of Cyber-security Incidents.
Proceedings of the 4th International Conference on Internet of Things, 2019

A Wizard-based Approach for Secure Code Generation of Single Sign-On and Access Delegation Solutions for Mobile Native Apps.
Proceedings of the 16th International Joint Conference on e-Business and Telecommunications, 2019

A Tool-assisted Methodology for the Data Protection Impact Assessment.
Proceedings of the 16th International Joint Conference on e-Business and Telecommunications, 2019

Enroll, and Authentication Will Follow - eID-Based Enrollment for a Customized, Secure, and Frictionless Authentication Experience.
Proceedings of the Foundations and Practice of Security - 12th International Symposium, 2019

MuFASA: A Tool for High-level Specification and Analysis of Multi-factor Authentication Protocols.
Proceedings of the Emerging Technologies for Authorization and Authentication, 2019

An Open and Flexible CyberSecurity Training Laboratory in IT/OT Infrastructures.
Proceedings of the Computer Security - ESORICS 2019 International Workshops, 2019

Lost in TLS? No More! Assisted Deployment of Secure TLS Configurations.
Proceedings of the Data and Applications Security and Privacy XXXIII, 2019

2018
Automated and efficient analysis of administrative temporal RBAC policies with role hierarchies.
J. Comput. Secur., 2018

SPLIT: A Secure and Scalable RPL routing protocol for Internet of Things.
Proceedings of the 14th International Conference on Wireless and Mobile Computing, 2018

PADS: Practical Attestation for Highly Dynamic Swarm Topologies.
Proceedings of the 2018 International Workshop on Secure Internet of Things, 2018

Solving Multi-Objective Workflow Satisfiability Problems with Optimization Modulo Theories Techniques.
Proceedings of the 23nd ACM on Symposium on Access Control Models and Technologies, 2018

A Lazy Approach to Access Control as a Service (ACaaS) for IoT: An AWS Case Study.
Proceedings of the 23nd ACM on Symposium on Access Control Models and Technologies, 2018

Design and Security Assessment of Usable Multi-factor Authentication and Single Sign-On Solutions for Mobile Applications - A Workshop Experience Report.
Proceedings of the Privacy and Identity Management. Fairness, Accountability, and Transparency in the Age of Big Data, 2018

Design, Formal Specification and Analysis of Multi-Factor Authentication Solutions with a Single Sign-On Experience.
Proceedings of the Principles of Security and Trust - 7th International Conference, 2018

Validating Requirements of Access Control for Cloud-Edge IoT Solutions (Short Paper).
Proceedings of the Foundations and Practice of Security - 11th International Symposium, 2018

2017
Scalable Automated Analysis of Access Control and Privacy Policies.
Trans. Large Scale Data Knowl. Centered Syst., 2017

Automatically finding execution scenarios to deploy security-sensitive workflows.
J. Comput. Secur., 2017

A Survey on Workflow Satisfiability, Resiliency, and Related Problems.
CoRR, 2017

Formal analysis of XACML policies using SMT.
Comput. Secur., 2017

Anatomy of the Facebook solution for mobile single sign-on: Security assessment and improvements.
Comput. Secur., 2017

Toward secure and efficient attestation for highly dynamic swarms: poster.
Proceedings of the 10th ACM Conference on Security and Privacy in Wireless and Mobile Networks, 2017

On Run-Time Enforcement of Authorization Constraints in Security-Sensitive Workflows.
Proceedings of the Software Engineering and Formal Methods - 15th International Conference, 2017

Assisted Authoring, Analysis and Enforcement of Access Control Policies in the Cloud.
Proceedings of the ICT Systems Security and Privacy Protection, 2017

Automated Legal Compliance Checking by Security Policy Analysis.
Proceedings of the Computer Safety, Reliability, and Security, 2017

Security Analysis and Legal Compliance Checking for the Design of Privacy-friendly Information Systems.
Proceedings of the 22nd ACM on Symposium on Access Control Models and Technologies, 2017

Aegis: Automatic Enforcement of Security Policies in Workflow-driven Web Applications.
Proceedings of the Seventh ACM Conference on Data and Application Security and Privacy, 2017

2016
Parameterized model checking for security policy analysis.
Int. J. Softw. Tools Technol. Transf., 2016

Cerberus: Automated Synthesis of Enforcement Mechanisms for Security-Sensitive Business Processes.
Proceedings of the Tools and Algorithms for the Construction and Analysis of Systems, 2016

Security of Mobile Single Sign-On: A Rational Reconstruction of Facebook Login Solution.
Proceedings of the 13th International Joint Conference on e-Business and Telecommunications (ICETE 2016), 2016

Modular Synthesis of Enforcement Mechanisms for the Workflow Satisfiability Problem: Scalability and Reusability.
Proceedings of the 21st ACM on Symposium on Access Control Models and Technologies, 2016

A delegated authorization solution for smart-city mobile applications.
Proceedings of the 2nd IEEE International Forum on Research and Technologies for Society and Industry Leveraging a better tomorrow, 2016

Assisted content-based labelling and classification of documents.
Proceedings of the International Conference on Military Communications and Information Systems, 2016

ASASPXL: New Clother for Analysing ARBAC Policies.
Proceedings of the Future Data and Security Engineering - Third International Conference, 2016

SMT-based Enforcement and Analysis of NATO Content-based Protection and Release Policies.
Proceedings of the 2016 ACM International Workshop on Attribute Based Access Control, 2016

2015
Modularity for Security-Sensitive Workflows.
CoRR, 2015

A Declarative Framework for Specifying and Enforcing Purpose-Aware Policies.
Proceedings of the Security and Trust Management - 11th International Workshop, 2015

Modeling Authorization Policies for Web Services in Presence of Transitive Dependencies.
Proceedings of the SECRYPT 2015, 2015

A SMT-based Tool for the Analysis and Enforcement of NATO Content-based Protection and Release Policies.
Proceedings of the 20th ACM Symposium on Access Control Models and Technologies, 2015

Automated analysis of RBAC policies with temporal constraints and static role hierarchies.
Proceedings of the 30th Annual ACM Symposium on Applied Computing, 2015

Analysis of XACML Policies with SMT.
Proceedings of the Principles of Security and Trust - 4th International Conference, 2015

Assisting the Deployment of Security-Sensitive Workflows by Finding Execution Scenarios.
Proceedings of the Data and Applications Security and Privacy XXIX, 2015

Compiling NATO authorization policies for enforcement in the cloud and SDNs.
Proceedings of the 2015 IEEE Conference on Communications and Network Security, 2015

Automated Synthesis of Run-time Monitors to Enforce Authorization Policies in Business Processes.
Proceedings of the 10th ACM Symposium on Information, 2015

Mobile App Security Assessment with the MAVeriC Dynamic Analysis Module.
Proceedings of the 7th ACM CCS International Workshop on Managing Insider Security Threats, 2015

2014
Quantifier-free interpolation in combinations of equality interpolating theories.
ACM Trans. Comput. Log., 2014

An extension of lazy abstraction with interpolation for programs with arrays.
Formal Methods Syst. Des., 2014

ALPS: An Action Language for Policy Specification and Automated Safety Analysis.
Proceedings of the Security and Trust Management - 10th International Workshop, 2014

Selective Release of Smart Metering Data in Multi-domain Smart Grids.
Proceedings of the Smart Grid Security - Second International Workshop, 2014

Scalable and precise automated analysis of administrative temporal role-based access control.
Proceedings of the 19th ACM Symposium on Access Control Models and Technologies, 2014

Attribute based access control for APIs in spring security.
Proceedings of the 19th ACM Symposium on Access Control Models and Technologies, 2014

Towards a Reference Architecture for Access Control in Distributed Web Applications.
Proceedings of the 2014 ESSoS Doctoral Symposium co-located with the International Symposium on Engineering Secure Software and Systems (ESSoS 2014), 2014

Incremental Analysis of Evolving Administrative Role Based Access Control Policies.
Proceedings of the Data and Applications Security and Privacy XXVIII, 2014

2013
Automated Termination in Model-Checking Modulo Theories.
Int. J. Found. Comput. Sci., 2013

Symbolic backward reachability with effectively propositional logic - Applications to security policy analysis.
Formal Methods Syst. Des., 2013

Content-based information protection and release in NATO operations.
Proceedings of the 18th ACM Symposium on Access Control Models and Technologies, 2013

A methodology to build run-time monitors for security-aware workflows.
Proceedings of the 8th International Conference for Internet Technology and Secured Transactions, 2013

Verification of Composed Array-Based Systems with Applications to Security-Aware Workflows.
Proceedings of the Frontiers of Combining Systems, 2013

Formal Modelling of Content-Based Protection and Release for Access Control in NATO Operations.
Proceedings of the Foundations and Practice of Security - 6th International Symposium, 2013

2012
On the verification of security-aware E-services.
J. Symb. Comput., 2012

Universal Guards, Relativization of Quantifiers, and Failure Models in Model Checking Modulo Theories.
J. Satisf. Boolean Model. Comput., 2012

Scalable automated symbolic analysis of administrative role-based access control policies by SMT solving.
J. Comput. Secur., 2012

Automated Analysis of Scenario-based Specifications of Distributed Access Control Policies with Non-Mechanizable Activities (Extended Version).
CoRR, 2012

Quantifier-Free Interpolation of a Theory of Arrays
Log. Methods Comput. Sci., 2012

Boosting Model Checking to Analyse Large ARBAC Policies.
Proceedings of the Security and Trust Management - 8th International Workshop, 2012

Automated Analysis of Scenario-Based Specifications of Distributed Access Control Policies with Non-mechanizable Activities.
Proceedings of the Security and Trust Management - 8th International Workshop, 2012

On the Automated Analysis of Safety in Usage Control: A New Decidability Result.
Proceedings of the Network and System Security - 6th International Conference, 2012

Automated Analysis of Parametric Timing-Based Mutual Exclusion Algorithms.
Proceedings of the NASA Formal Methods, 2012

Lazy Abstraction with Interpolants for Arrays.
Proceedings of the Logic for Programming, Artificial Intelligence, and Reasoning, 2012

Automated and Efficient Analysis of Role-Based Access Control with Attributes.
Proceedings of the Data and Applications Security and Privacy XXVI, 2012

Efficient run-time solving of RBAC user authorization queries: pushing the envelope.
Proceedings of the Second ACM Conference on Data and Application Security and Privacy, 2012

SAFARI: SMT-Based Abstraction for Arrays with Interpolants.
Proceedings of the Computer Aided Verification - 24th International Conference, 2012

From Strong Amalgamability to Modularity of Quantifier-Free Interpolation.
Proceedings of the Automated Reasoning - 6th International Joint Conference, 2012

Reachability Modulo Theory Library.
Proceedings of the 10th International Workshop on Satisfiability Modulo Theories, 2012

2011
A declarative two-level framework to specify and verify workflow and authorization policies in service-oriented architectures.
Serv. Oriented Comput. Appl., 2011

Workflow and Access Control Reloaded: a Declarative Specification Framework for the Automated Analysis of Web Services.
Scalable Comput. Pract. Exp., 2011

Automatic decidability and combinability.
Inf. Comput., 2011

Automated Analysis of Infinite State Workflows with Access Control Policies.
Proceedings of the Security and Trust Management - 7th International Workshop, 2011

Automated Analysis of Semantic-Aware Access Control Policies: A Logic-Based Approach.
Proceedings of the 5th IEEE International Conference on Semantic Computing (ICSC 2011), 2011

Rewriting-based Quantifier-free Interpolation for a Theory of Arrays.
Proceedings of the 22nd International Conference on Rewriting Techniques and Applications, 2011

A Combination of Rewriting and Constraint Solving for the Quantifier-Free Interpolation of Arrays with Integer Difference Constraints.
Proceedings of the Frontiers of Combining Systems, 8th International Symposium, 2011

Efficient symbolic automated analysis of administrative attribute-based RBAC-policies.
Proceedings of the 6th ACM Symposium on Information, Computer and Communications Security, 2011

ASASP: Automated Symbolic Analysis of Security Policies.
Proceedings of the Automated Deduction - CADE-23 - 23rd International Conference on Automated Deduction, Wroclaw, Poland, July 31, 2011

2010
Combination of convex theories: Modularity, deduction completeness, and explanation.
J. Symb. Comput., 2010

Automated Support for the Design and Validation of Fault Tolerant Parameterized Systems: a case study.
Electron. Commun. Eur. Assoc. Softw. Sci. Technol., 2010

Automated Symbolic Analysis of ARBAC-Policies (Extended Version)
CoRR, 2010

Backward Reachability of Array-based Systems by SMT solving: Termination and Invariant Synthesis
Log. Methods Comput. Sci., 2010

Automated Validation of Security-sensitive Web Services specified in BPEL and RBAC (Extended Version)
CoRR, 2010

Brief Announcement: Automated Support for the Design and Validation of Fault Tolerant Parameterized Systems - A Case Study.
Proceedings of the Distributed Computing, 24th International Symposium, 2010

Automated Validation of Security-Sensitive Web Services Specified in BPEL and RBAC.
Proceedings of the 12th International Symposium on Symbolic and Numeric Algorithms for Scientific Computing, 2010

WSSMT: Towards the Automated Analysis of Security-Sensitive Services and Applications.
Proceedings of the 12th International Symposium on Symbolic and Numeric Algorithms for Scientific Computing, 2010

Automated Symbolic Analysis of ARBAC-Policies.
Proceedings of the Security and Trust Management - 6th International Workshop, 2010

The SMT-LIB Initiative and the Rise of SMT - (HVC 2010 Award Talk).
Proceedings of the Hardware and Software: Verification and Testing, 2010

MCMT: A Model Checker Modulo Theories.
Proceedings of the Automated Reasoning, 5th International Joint Conference, 2010

MCMT in the Land of Parametrized Timed Automata.
Proceedings of the 6th International Verification Workshop, 2010

2009
New results on rewrite-based satisfiability procedures.
ACM Trans. Comput. Log., 2009

Satisfiability solving for software verification.
Int. J. Softw. Tools Technol. Transf., 2009

Verifying the Interplay of Authorization Policies and Workflow in Service-Oriented Architectures (Full version)
CoRR, 2009

Preface.
Ann. Math. Artif. Intell., 2009

Goal-Directed Invariant Synthesis for Model Checking Modulo Theories.
Proceedings of the Automated Reasoning with Analytic Tableaux and Related Methods, 2009

Towards the Verification of Security-Aware Transaction E-services.
Proceedings of the 7th International Workshop on First-Order Theorem Proving, 2009

Verifying the Interplay of Authorization Policies and Workflow in Service-Oriented Architectures.
Proceedings of the 12th IEEE International Conference on Computational Science and Engineering, 2009

2008
A Prototype Implementation of a Distributed Satisfiability Modulo Theories Solver in the ToolBus Framework.
J. Braz. Comput. Soc., 2008

Light-Weight SMT-based Model Checking.
Proceedings of the Eighth International Workshop on Automated Verification of Critical Systems, 2008

Towards SMT Model Checking of Array-Based Systems.
Proceedings of the Automated Reasoning, 4th International Joint Conference, 2008

2007
Decision procedures for extensions of the theory of arrays.
Ann. Math. Artif. Intell., 2007

Building Extended Canonizers by Graph-Based Deduction.
Proceedings of the Theoretical Aspects of Computing, 2007

Combining Proof-Producing Decision Procedures.
Proceedings of the Frontiers of Combining Systems, 6th International Symposium, 2007

Noetherianity and Combination Problems.
Proceedings of the Frontiers of Combining Systems, 6th International Symposium, 2007

From Non-Disjoint Combination to Satisfiability and Model-Checking of Infinite State Systems.
Proceedings of the Deduction and Decision Procedures, 30.09. - 05.10.2007, 2007

Combination Methods for Satisfiability and Model-Checking of Infinite-State Systems.
Proceedings of the Automated Deduction, 2007

2006
Efficient theory combination via boolean search.
Inf. Comput., 2006

Intelligent Systems and Formal Methods in Software Engineering.
IEEE Intell. Syst., 2006

A Theory of Singly-Linked Lists and its Extensible Decision Procedure.
Proceedings of the Fourth IEEE International Conference on Software Engineering and Formal Methods (SEFM 2006), 2006

Automatic Combinability of Rewriting-Based Satisfiability Procedures.
Proceedings of the Logic for Programming, 2006

Deciding Extensions of the Theory of Arrays by Integrating Decision Procedures and Instantiation Strategies.
Proceedings of the Logics in Artificial Intelligence, 10th European Conference, 2006

Decision Procedures for the Formal Analysis of Software.
Proceedings of the Theoretical Aspects of Computing, 2006

Decidability and Undecidability Results for Nelson-Oppen and Rewrite-Based Decision Procedures.
Proceedings of the Automated Reasoning, Third International Joint Conference, 2006

2005
Distributing the Workload in a Lazy Theorem-Prover.
Proceedings of the Second Brazilian Symposium on Formal Methods, 2005

On Superposition-Based Satisfiability Procedures and Their Combination.
Proceedings of the Theoretical Aspects of Computing, 2005

Combining Data Structures with Nonstably Infinite Theories Using Many-Sorted Logic.
Proceedings of the Frontiers of Combining Systems, 5th International Workshop, 2005

On a Rewriting Approach to Satisfiability Procedures: Extension, Combination of Theories and an Experimental Appraisal.
Proceedings of the Frontiers of Combining Systems, 5th International Workshop, 2005

Efficient Satisfiability Modulo Theories via Delayed Theory Combination.
Proceedings of the Computer Aided Verification, 17th International Conference, 2005

Rewriting and Decision Procedure Laboratory: Combining Rewriting, Satisfiability Checking, and Lemma Speculation.
Proceedings of the Mechanizing Mathematical Reasoning, 2005

2004
Scalable Automated Proving and Debugging of Set-Based Specifications.
J. Braz. Comput. Soc., 2004

Preface.
Proceedings of the Selected Papers from the Workshops on Disproving, 2004

Combining Lists with Non-stably Infinite Theories.
Proceedings of the Logic for Programming, 2004

Nelson-Oppen, Shostak and the Extended Canonizer: A Family Picture with a Newborn.
Proceedings of the Theoretical Aspects of Computing, 2004

Abstraction-Driven Verification of Array Programs.
Proceedings of the Artificial Intelligence and Symbolic Computation, 2004

2003
Constraint contextual rewriting.
J. Symb. Comput., 2003

A rewriting approach to satisfiability procedures.
Inf. Comput., 2003

Applying Light-Weight Theorem Proving to Debugging and Verifying Pointer Programs.
Proceedings of the 4th International Workshop on First-Order Theorem Proving, 2003

Proving and Debugging Set-Based Specifications.
Proceedings of the 6th Brazilian Workshop on Formal Methods, 2003

Light-Weight Theorem Proving for Debugging and Verifying Units of Code.
Proceedings of the 1st International Conference on Software Engineering and Formal Methods (SEFM 2003), 2003

2002
Combining Generic and Domain Specific Reasoning by Using Contexts.
Proceedings of the Artificial Intelligence, 2002

2001
A Practical Extension Mechanism for Decision Procedures: the Case Study of Universal Presburger Arithmetic.
J. Univers. Comput. Sci., 2001

The Control Layer in Open Mechanized Reasoning Systems: Annotations and Tactics.
J. Symb. Comput., 2001

Uniform Derivation of Decision Procedures by Superposition.
Proceedings of the Computer Science Logic, 15th International Workshop, 2001

The Phase Transition of the Linear Inequalities Problem.
Proceedings of the Principles and Practice of Constraint Programming, 2001

System Description: RDL : Rewrite and Decision Procedure Laboratory.
Proceedings of the Automated Reasoning, First International Joint Conference, 2001

2000
Termination of Constraint Contextual Rewriting.
Proceedings of the Frontiers of Combining Systems, 2000

1998
From Integrated Reasoning Specialists to "Plug-and-Play" Reasoning Components.
Proceedings of the Artificial Intelligence and Symbolic Computation, 1998

Constraint Solving in Logic Programming and in Automated Deduction: A Comparison.
Proceedings of the Artificial Intelligence: Methodology, 1998


  Loading...