Silvio Ghilardi

Proceedings of the Foundations of Software Science and Computation Structures, 2021

Delta-BPMN: A Concrete Language and Verifier for Data-Aware BPMN.

[BibT_eX]

[DOI]

Proceedings of the Business Process Management - 19th International Conference, 2021

2020

Fixed-point Elimination in the Intuitionistic Propositional Calculus.

[BibT_eX]

[DOI]

Maria João Gouveia

ACM Trans. Comput. Log., 2020

Free Heyting algebra endomorphisms: Ruitenburg's Theorem and beyond.

[BibT_eX]

[DOI]

Math. Struct. Comput. Sci., 2020

SMT-based verification of data-aware processes: a model-theoretic approach.

[BibT_eX]

[DOI]

Math. Struct. Comput. Sci., 2020

Interpolation and Amalgamation for Arrays with MaxDiff (Extended Version).

[BibT_eX]

[DOI]

CoRR, 2020

Petri Nets with Parameterised Data: Modelling and Verification (Extended Version).

[BibT_eX]

[DOI]

CoRR, 2020

Compactly Representing Uniform Interpolants for EUF using (conditional) DAGS.

[BibT_eX]

[DOI]

CoRR, 2020

Computing Uniform Interpolants for EUF via (conditional) DAG-based Compact Representations.

[BibT_eX]

[DOI]

Proceedings of the 35th Italian Conference on Computational Logic, 2020

Combined Covers and Beth Definability.

[BibT_eX]

[DOI]

Proceedings of the Automated Reasoning - 10th International Joint Conference, 2020

Petri Nets with Parameterised Data - Modelling and Verification.

[BibT_eX]

[DOI]

Proceedings of the Business Process Management - 18th International Conference, 2020

Model Completeness and Π2-rules: The Case of Contact Algebras.

[BibT_eX]

[DOI]

Lucia Landi

Proceedings of the 13th Conference on Advances in Modal Logic, 2020

2019

Existentially closed Brouwerian Semilattices.

[BibT_eX]

[DOI]

Luca Carai

J. Symb. Log., 2019

Formal Modeling and SMT-Based Parameterized Verification of Data-Aware BPMN (Extended Version).

[BibT_eX]

[DOI]

CoRR, 2019

Formal Modeling and SMT-Based Parameterized Verification of Multi-Case Data-Aware BPMN.

[BibT_eX]

[DOI]

CoRR, 2019

Model Completeness, Covers and Superposition (Abridged Version).

[BibT_eX]

Proceedings of the 34th Italian Conference on Computational Logic, 2019

Model Completeness, Covers and Superposition.

[BibT_eX]

[DOI]

Proceedings of the Automated Deduction - CADE 27, 2019

Formal Modeling and SMT-Based Parameterized Verification of Data-Aware BPMN.

[BibT_eX]

[DOI]

Proceedings of the Business Process Management - 17th International Conference, 2019

From Model Completeness to Verification of Data Aware Processes.

[BibT_eX]

[DOI]

Proceedings of the Description Logic, Theory Combination, and All That, 2019

2018

Verification of Data-Aware Processes via Array-Based Systems (Extended Version).

[BibT_eX]

[DOI]

CoRR, 2018

Quantifier Elimination for Database Driven Verification.

[BibT_eX]

[DOI]

CoRR, 2018

Fixed-point elimination in the Intuitionistic Propositional Calculus (extended version).

[BibT_eX]

[DOI]

Maria João Gouveia

CoRR, 2018

Modularity results for interpolation, amalgamation and superamalgamation.

[BibT_eX]

[DOI]

Ann. Pure Appl. Log., 2018

Ruitenburg's Theorem via Duality and Bounded Bisimulations.

[BibT_eX]

[DOI]

Proceedings of the Advances in Modal Logic 12, 2018

2017

One-step Heyting Algebras and Hypersequent Calculi with the Bounded Proof Property.

[BibT_eX]

[DOI]

Frederik Möllerström Lauridsen

J. Log. Comput., 2017

A Model-Theoretic characterization of Monadic second order Logic on Infinite Words.

[BibT_eX]

[DOI]

Samuel J. van Gool

J. Symb. Log., 2017

A Framework for the Verification of Parameterized Infinite-state Systems.

[BibT_eX]

[DOI]

Fundam. Informaticae, 2017

Cardinality constraints for arrays (decidability results and applications).

[BibT_eX]

[DOI]

Formal Methods Syst. Des., 2017

Counter Simulations via Higher Order Quantifier Elimination: a preliminary report.

[BibT_eX]

[DOI]

Proceedings of the Fifth Workshop on Proof eXchange for Theorem Proving, 2017

Formal verification of data-intensive applications through model checking modulo theories.

[BibT_eX]

[DOI]

Proceedings of the 24th ACM SIGSOFT International SPIN Symposium on Model Checking of Software, 2017

Second Order Quantifier Elimination: Towards Verification Applications.

[BibT_eX]

[DOI]

Proceedings of the Workshop on Second-Order Quantifier Elimination and Related Topics (SOQE 2017), 2017

Formal Verification of ARP (Address Resolution Protocol) Through SMT-Based Model Checking - A Case Study -.

[BibT_eX]

[DOI]

Proceedings of the Integrated Formal Methods - 13th International Conference, 2017

Interpolation, Amalgamation and Combination (The Non-disjoint Signatures Case).

[BibT_eX]

[DOI]

Proceedings of the Frontiers of Combining Systems - 11th International Symposium, 2017

2016

Admissible Bases Via Stable Canonical Rules.

[BibT_eX]

[DOI]

Stud Logica, 2016

Monadic second order logic as the model companion of temporal logic.

[BibT_eX]

[DOI]

Sam van Gool

Proceedings of the 31st Annual ACM/IEEE Symposium on Logic in Computer Science, 2016

Counter Abstractions in Model Checking of Distributed Broadcast Algorithms: Some Case Studies.

[BibT_eX]

[DOI]

Proceedings of the 31st Italian Conference on Computational Logic, 2016

Counting Constraints in Flat Array Fragments.

[BibT_eX]

[DOI]

Proceedings of the Automated Reasoning - 8th International Joint Conference, 2016

2015

Decision Procedures for Flat Array Properties.

[BibT_eX]

[DOI]

J. Autom. Reason., 2015

A New Acceleration-Based Combination Framework for Array Properties.

[BibT_eX]

[DOI]

Proceedings of the Frontiers of Combining Systems - 10th International Symposium, 2015

2014

Quantifier-free interpolation in combinations of equality interpolating theories.

[BibT_eX]

[DOI]

ACM Trans. Comput. Log., 2014

The logic of transitive and dense frames: from the step-frame analysis to full cut-elimination.

[BibT_eX]

[DOI]

Grigori Mints

Log. J. IGPL, 2014

An extension of lazy abstraction with interpolation for programs with arrays.

[BibT_eX]

[DOI]

Formal Methods Syst. Des., 2014

Monotonic Abstraction Techniques: from Parametric to Software Model Checking.

[BibT_eX]

[DOI]

Proceedings of the Proceedings First Workshop on Logics and Model-checking for Self-* Systems, 2014

The bounded proof property via step algebras and step frames.

[BibT_eX]

[DOI]

Ann. Pure Appl. Log., 2014

Booster: An Acceleration-Based Verification Framework for Array Programs.

[BibT_eX]

[DOI]

Proceedings of the Automated Technology for Verification and Analysis, 2014

Multiple-conclusion Rules, Hypersequents Syntax and Step Frames.

[BibT_eX]

[DOI]

Proceedings of the Advances in Modal Logic 10, 2014

Unified Correspondence.

[BibT_eX]

[DOI]

Willem Conradie

Alessandra Palmigiano

Proceedings of the Johan van Benthem on Logic and Information Dynamics, 2014

2013

Automated Termination in Model-Checking Modulo Theories.

[BibT_eX]

[DOI]

Alessandro Carioni

Int. J. Found. Comput. Sci., 2013

Abstraction and Acceleration in SMT-based Model-Checking for Array Programs

[BibT_eX]

[DOI]

CoRR, 2013

From free algebras to proof bounds.

[BibT_eX]

[DOI]

Proceedings of the TACL 2013. Sixth International Conference on Topology, Algebra and Categories in Logic, Vanderbilt University, Nashville, Tennessee, USA, July 28, 2013

Bounded Proofs and Step Frames.

[BibT_eX]

[DOI]

Proceedings of the Automated Reasoning with Analytic Tableaux and Related Methods, 2013

Acceleration-based safety decision procedure for programs with arrays.

[BibT_eX]

[DOI]

Proceedings of the LPAR 2013, 2013

Definability of Accelerated Relations in a Theory of Arrays and Its Applications.

[BibT_eX]

[DOI]

Proceedings of the Frontiers of Combining Systems, 2013

2012

LTL over description logic axioms.

[BibT_eX]

[DOI]

Carsten Lutz

ACM Trans. Comput. Log., 2012

Universal Guards, Relativization of Quantifiers, and Failure Models in Model Checking Modulo Theories.

[BibT_eX]

[DOI]

J. Satisf. Boolean Model. Comput., 2012

Quantifier-Free Interpolation of a Theory of Arrays

[BibT_eX]

[DOI]

Log. Methods Comput. Sci., 2012

Automated Analysis of Parametric Timing-Based Mutual Exclusion Algorithms.

[BibT_eX]

[DOI]

Proceedings of the NASA Formal Methods, 2012

Lazy Abstraction with Interpolants for Arrays.

[BibT_eX]

[DOI]

Proceedings of the Logic for Programming, Artificial Intelligence, and Reasoning, 2012

SAFARI: SMT-Based Abstraction for Arrays with Interpolants.

[BibT_eX]

[DOI]

Proceedings of the Computer Aided Verification - 24th International Conference, 2012

From Strong Amalgamability to Modularity of Quantifier-Free Interpolation.

[BibT_eX]

[DOI]

Proceedings of the Automated Reasoning - 6th International Joint Conference, 2012

Reachability Modulo Theory Library.

[BibT_eX]

[DOI]

Proceedings of the 10th International Workshop on Satisfiability Modulo Theories, 2012

2011

An Algebraic Approach to Subframe Logics. Modal Case.

[BibT_eX]

[DOI]

Guram Bezhanishvili

Mamuka Jibladze

Notre Dame J. Formal Log., 2011

Unification in modal and description logics.

[BibT_eX]

[DOI]

Log. J. IGPL, 2011

Rewriting-based Quantifier-free Interpolation for a Theory of Arrays.

[BibT_eX]

[DOI]

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.

[BibT_eX]

[DOI]

Proceedings of the Frontiers of Combining Systems, 8th International Symposium, 2011

2010

Book Reviews.

[BibT_eX]

[DOI]

Stud Logica, 2010

Special issue on automated deduction: Decidability, complexity, tractability.

[BibT_eX]

[DOI]

Viorica Sofronie-Stokkermans

Ulrike Sattler

Ashish Tiwari

J. Symb. Comput., 2010

Continuity, freeness, and filtrations.

[BibT_eX]

[DOI]

J. Appl. Non Class. Logics, 2010

Automated Support for the Design and Validation of Fault Tolerant Parameterized Systems: a case study.

[BibT_eX]

[DOI]

Electron. Commun. Eur. Assoc. Softw. Sci. Technol., 2010

Backward Reachability of Array-based Systems by SMT solving: Termination and Invariant Synthesis

[BibT_eX]

[DOI]

Log. Methods Comput. Sci., 2010

Brief Announcement: Automated Support for the Design and Validation of Fault Tolerant Parameterized Systems - A Case Study.

[BibT_eX]

[DOI]

Proceedings of the Distributed Computing, 24th International Symposium, 2010

MCMT: A Model Checker Modulo Theories.

[BibT_eX]

[DOI]

Proceedings of the Automated Reasoning, 5th International Joint Conference, 2010

MCMT in the Land of Parametrized Timed Automata.

[BibT_eX]

[DOI]

Alessandro Carioni

Proceedings of the 6th International Verification Workshop, 2010

2009

Goal-Directed Invariant Synthesis for Model Checking Modulo Theories.

[BibT_eX]

[DOI]

Proceedings of the Automated Reasoning with Analytic Tableaux and Related Methods, 2009

Model-Checking of Array-Based Systems: from Foundations to Implementation.

[BibT_eX]

[DOI]

Proceedings of the 7th International Workshop on First-Order Theorem Proving, 2009

2008

A comprehensive combination framework.

[BibT_eX]

[DOI]

Enrica Nicolini

Daniele Zucchelli

ACM Trans. Comput. Log., 2008

Light-Weight SMT-based Model Checking.

[BibT_eX]

[DOI]

Thomas Valsecchi

Proceedings of the Eighth International Workshop on Automated Verification of Critical Systems, 2008

Towards SMT Model Checking of Array-Based Systems.

[BibT_eX]

[DOI]

Proceedings of the Automated Reasoning, 4th International Joint Conference, 2008

2007

Connecting many-sorted theories.

[BibT_eX]

[DOI]

J. Symb. Log., 2007

An algebraic approach to subframe logics. Intuitionistic case.

[BibT_eX]

[DOI]

Guram Bezhanishvili

Ann. Pure Appl. Log., 2007

Decision procedures for extensions of the theory of arrays.

[BibT_eX]

[DOI]

Ann. Math. Artif. Intell., 2007

Noetherianity and Combination Problems.

[BibT_eX]

[DOI]

Proceedings of the Frontiers of Combining Systems, 6th International Symposium, 2007

From Non-Disjoint Combination to Satisfiability and Model-Checking of Infinite State Systems.

[BibT_eX]

[DOI]

Proceedings of the Deduction and Decision Procedures, 30.09. - 05.10.2007, 2007

Combination Methods for Satisfiability and Model-Checking of Infinite-State Systems.

[BibT_eX]

[DOI]

Proceedings of the Automated Deduction, 2007

First-order modal logic.

[BibT_eX]

[DOI]

Torben Braüner

Proceedings of the Handbook of Modal Logic., 2007

2006

A new combination procedure for the word problem that generalizes fusion decidability results in modal logics.

[BibT_eX]

[DOI]

Cesare Tinelli

Inf. Comput., 2006

Did I Damage My Ontology? A Case for Conservative Extensions in Description Logics.

[BibT_eX]

[DOI]

Carsten Lutz

Frank Wolter

Proceedings of the Proceedings, 2006

Deciding Extensions of the Theory of Arrays by Integrating Decision Procedures and Instantiation Strategies.

[BibT_eX]

[DOI]

Proceedings of the Logics in Artificial Intelligence, 10th European Conference, 2006

Decidability and Undecidability Results for Nelson-Oppen and Rewrite-Based Decision Procedures.

[BibT_eX]

[DOI]

Proceedings of the Automated Reasoning, Third International Joint Conference, 2006

Conservative extensions in modal logic.

[BibT_eX]

[DOI]

Carsten Lutz

Frank Wolter

Michael Zakharyaschev

Proceedings of the Advances in Modal Logic 6, 2006

2005

A Comprehensive Framework for Combined Decision Procedures.

[BibT_eX]

[DOI]

Enrica Nicolini

Daniele Zucchelli

Proceedings of the Frontiers of Combining Systems, 5th International Workshop, 2005

Connecting Many-Sorted Structures and Theories Through Adjoint Functions.

[BibT_eX]

[DOI]

Proceedings of the Frontiers of Combining Systems, 5th International Workshop, 2005

2004

Filtering unification and most general unifiers in modal logic.

[BibT_eX]

[DOI]

Lorenzo Sacchetti

J. Symb. Log., 2004

Model-Theoretic Methods in Combined Constraint Satisfiability.

[BibT_eX]

[DOI]

J. Autom. Reason., 2004

Unification, finite duality and projectivity in varieties of Heyting algebras.

[BibT_eX]

[DOI]

Ann. Pure Appl. Log., 2004

2003

Combining word problems through rewriting in categories with products.

[BibT_eX]

[DOI]

Camillo Fiorentini

Theor. Comput. Sci., 2003

Foreword.

[BibT_eX]

[DOI]

Daniele Mundici

Stud Logica, 2003

Quantifier Elimination and Provers Integration.

[BibT_eX]

[DOI]

Proceedings of the 4th International Workshop on First-Order Theorem Proving, 2003

Algebraic and Model Theoretic Techniques for Fusion Decidability in Modal Logics.

[BibT_eX]

[DOI]

Proceedings of the Logic for Programming, 2003

2002

A Resolution/Tableaux Algorithm for Projective Approximations in IPC.

[BibT_eX]

[DOI]

Log. J. IGPL, 2002

Sheaves, games, and model completions - a categorical approach to nonclassical propositional logics.

[BibT_eX]

Trends in logic 14, Springer, ISBN: 978-1-4020-0660-9, 2002

2000

Best Solving Modal Equations.

[BibT_eX]

[DOI]

Ann. Pure Appl. Log., 2000

From Bisimulation Quantifiers to Classifying Toposes.

[BibT_eX]

[DOI]

Proceedings of the Advances in Modal Logic 3, 2000

1999

On Canonicity and Strong Completeness Conditions in Intermediate Propositional Logics.

[BibT_eX]

[DOI]

Pierangelo Miglioli

Stud Logica, 1999

Unification in Intuitionistic Logic.

[BibT_eX]

[DOI]

J. Symb. Log., 1999

1997

Unification Through Projectivity.

[BibT_eX]

[DOI]

J. Log. Comput., 1997

Model Completions, r-Heyting Categories.

[BibT_eX]

[DOI]

Ann. Pure Appl. Log., 1997

Constructive Canonicity in Non-Classical Logics.

[BibT_eX]

[DOI]

Giancarlo Meloni

Ann. Pure Appl. Log., 1997

1996

Relational and Partial Variable Sets and Basic Predicate Logic.

[BibT_eX]

[DOI]

Giancarlo Meloni

J. Symb. Log., 1996

1995

Undefinability of propositional quantifiers in the modal system S4.

[BibT_eX]

[DOI]

Stud Logica, 1995

A Sheaf Representation and Duality for Finitely Presenting Heyting Algebras.

[BibT_eX]

[DOI]

J. Symb. Log., 1995

An Algebraic Theory of Normal Forms.

[BibT_eX]

[DOI]

Ann. Pure Appl. Log., 1995

1992

Quantified Extensions of Canonical Propositional Intermediate Logics.

[BibT_eX]

[DOI]

Stud Logica, 1992

1991

Incompleteness Results in Kripke Semantics.

[BibT_eX]

[DOI]

J. Symb. Log., 1991

1990

Modal logics with n-ary connectives.

[BibT_eX]

[DOI]

Giancarlo Meloni

Math. Log. Q., 1990

1989

Presheaf semantics and independence results for some non-classical first-order logics.

[BibT_eX]

[DOI]

Arch. Math. Log., 1989

Directed frames.

[BibT_eX]

[DOI]

Giovanna Corsi