Search

Your search keyword '"Department of Formal Methods (LORIA - FM)"' showing total 12 results
Start Over Author "Department of Formal Methods (LORIA - FM)" Journal journal of automated reasoning
12 results on '"Department of Formal Methods (LORIA - FM)"'

1. A Formal Proof of the Expressiveness of Deep Learning

Author

Dietrich Klakow, Jasmin Christian Blanchette, Alexander Bentkamp, Theoretical Computer Science, Network Institute, Vrije Universiteit Amsterdam [Amsterdam] (VU), Max-Planck-Institut für Informatik (MPII), Max-Planck-Gesellschaft, Modeling and Verification of Distributed Algorithms and Systems (VERIDIS), Department of Formal Methods (LORIA - FM), Laboratoire Lorrain de Recherche en Informatique et ses Applications (LORIA), Institut National de Recherche en Informatique et en Automatique (Inria)-Université de Lorraine (UL)-Centre National de la Recherche Scientifique (CNRS)-Institut National de Recherche en Informatique et en Automatique (Inria)-Université de Lorraine (UL)-Centre National de la Recherche Scientifique (CNRS)-Laboratoire Lorrain de Recherche en Informatique et ses Applications (LORIA), Institut National de Recherche en Informatique et en Automatique (Inria)-Université de Lorraine (UL)-Centre National de la Recherche Scientifique (CNRS)-Institut National de Recherche en Informatique et en Automatique (Inria)-Université de Lorraine (UL)-Centre National de la Recherche Scientifique (CNRS)-Inria Nancy - Grand Est, Institut National de Recherche en Informatique et en Automatique (Inria)-Max-Planck-Institut für Informatik (MPII), Max-Planck-Gesellschaft-Max-Planck-Gesellschaft, Institut National de Recherche en Informatique et en Automatique (Inria)-Université de Lorraine (UL)-Centre National de la Recherche Scientifique (CNRS), Universität des Saarlandes [Saarbrücken], Max-Planck-Gesellschaft-Max-Planck-Gesellschaft-Inria Nancy - Grand Est, Institut National de Recherche en Informatique et en Automatique (Inria)-Institut National de Recherche en Informatique et en Automatique (Inria)-Department of Formal Methods (LORIA - FM), Institut National de Recherche en Informatique et en Automatique (Inria)-Université de Lorraine (UL)-Centre National de la Recherche Scientifique (CNRS)-Université de Lorraine (UL)-Centre National de la Recherche Scientifique (CNRS), Centre National de la Recherche Scientifique (CNRS)-Université de Lorraine (UL)-Institut National de Recherche en Informatique et en Automatique (Inria)-Centre National de la Recherche Scientifique (CNRS)-Université de Lorraine (UL)-Institut National de Recherche en Informatique et en Automatique (Inria)-Laboratoire Lorrain de Recherche en Informatique et ses Applications (LORIA), and Centre National de la Recherche Scientifique (CNRS)-Université de Lorraine (UL)-Institut National de Recherche en Informatique et en Automatique (Inria)-Centre National de la Recherche Scientifique (CNRS)-Université de Lorraine (UL)

Subjects
Formalization, Theoretical computer science, Computer science, HOL, Tensors, 02 engineering and technology, Type (model theory), Mathematical proof, 01 natural sciences, Formal proof, Development (topology), Artificial Intelligence, Computer Science::Logic in Computer Science, 020204 information systems, Machine learning, 0502 economics and business, 0202 electrical engineering, electronic engineering, information engineering, 0101 mathematics, Borel measure, business.industry, Deep learning, 010102 general mathematics, 05 social sciences, [INFO.INFO-LO]Computer Science [cs]/Logic in Computer Science [cs.LO], 020207 software engineering, Multivariate polynomials, TheoryofComputation_MATHEMATICALLOGICANDFORMALLANGUAGES, Computational Theory and Mathematics, TheoryofComputation_LOGICSANDMEANINGSOFPROGRAMS, Computer Science::Mathematical Software, Convolutional arithmetic circuits, 050211 marketing, Isabelle, Artificial intelligence, business, SDG 4 - Quality Education, Software
Abstract

Deep learning has had a profound impact on computer science in recentyears, with applications to image recognition, language processing, bioinformatics,and more. Recently, Cohen et al. provided theoretical evidence for the superiorityof deep learning over shallow learning. We formalized their mathematicalproof using Isabelle/HOL. The Isabelle development simplifies and generalizesthe original proof, while working around the limitations of the HOL type system.To support the formalization, we developed reusable libraries of formalizedmathematics, including results about the matrix rank, the Borel measure, andmultivariate polynomials as well as a library for tensor analysis.

Published
2018

2. A decision procedure for (co)datatypes in SMT solvers

Author

Jasmin Christian Blanchette, Andrew Reynolds, University of Iowa [Iowa City], Modeling and Verification of Distributed Algorithms and Systems (VERIDIS), Max-Planck-Institut für Informatik (MPII), Max-Planck-Gesellschaft-Max-Planck-Gesellschaft-Inria Nancy - Grand Est, Institut National de Recherche en Informatique et en Automatique (Inria)-Institut National de Recherche en Informatique et en Automatique (Inria)-Department of Formal Methods (LORIA - FM), Laboratoire Lorrain de Recherche en Informatique et ses Applications (LORIA), Centre National de la Recherche Scientifique (CNRS)-Université de Lorraine (UL)-Institut National de Recherche en Informatique et en Automatique (Inria)-Centre National de la Recherche Scientifique (CNRS)-Université de Lorraine (UL)-Institut National de Recherche en Informatique et en Automatique (Inria)-Laboratoire Lorrain de Recherche en Informatique et ses Applications (LORIA), Centre National de la Recherche Scientifique (CNRS)-Université de Lorraine (UL)-Institut National de Recherche en Informatique et en Automatique (Inria)-Centre National de la Recherche Scientifique (CNRS)-Université de Lorraine (UL), Proof-oriented development of computer-based systems (MOSEL), Department of Formal Methods (LORIA - FM), Centre National de la Recherche Scientifique (CNRS)-Université de Lorraine (UL)-Institut National de Recherche en Informatique et en Automatique (Inria)-Centre National de la Recherche Scientifique (CNRS)-Université de Lorraine (UL)-Institut National de Recherche en Informatique et en Automatique (Inria), The second author’s work was partially supported by the Deutsche Forschungsgemeinschaft project 'Den Hammer härten' (grant NI 491/14-1) and the Inria technological development action 'Contre-exemples utilisables par Isabelle et Coq' (CUIC)., Ecole Polytechnique Fédérale de Lausanne (EPFL), Centre National de la Recherche Scientifique (CNRS)-Université de Lorraine (UL)-Institut National de Recherche en Informatique et en Automatique (Inria)-Centre National de la Recherche Scientifique (CNRS)-Université de Lorraine (UL)-Institut National de Recherche en Informatique et en Automatique (Inria)-Inria Nancy - Grand Est, Institut National de Recherche en Informatique et en Automatique (Inria)-Max-Planck-Institut für Informatik (MPII), Max-Planck-Gesellschaft-Max-Planck-Gesellschaft, The second author’s research was partially supported by the Deutsche Forschungsgemeinschaft project 'Den Hammer härten' (grant NI 491/14-1) and the Inria technological development action 'Contre-exemples Utilisables par Isabelle et Coq' (CUIC)., Felty, Ap, Middeldorp, A, Institut National de Recherche en Informatique et en Automatique (Inria)-Université de Lorraine (UL)-Centre National de la Recherche Scientifique (CNRS)-Institut National de Recherche en Informatique et en Automatique (Inria)-Université de Lorraine (UL)-Centre National de la Recherche Scientifique (CNRS)-Laboratoire Lorrain de Recherche en Informatique et ses Applications (LORIA), Institut National de Recherche en Informatique et en Automatique (Inria)-Université de Lorraine (UL)-Centre National de la Recherche Scientifique (CNRS)-Université de Lorraine (UL)-Centre National de la Recherche Scientifique (CNRS), Institut National de Recherche en Informatique et en Automatique (Inria)-Université de Lorraine (UL)-Centre National de la Recherche Scientifique (CNRS)-Institut National de Recherche en Informatique et en Automatique (Inria)-Université de Lorraine (UL)-Centre National de la Recherche Scientifique (CNRS), Theoretical Computer Science, and Network Institute

Subjects
Theoretical computer science, SDG 16 - Peace, Computer science, 0102 computer and information sciences, 02 engineering and technology, computer.software_genre, 01 natural sciences, Artificial Intelligence, Satisfiability modulo theories, Computer Science::Logic in Computer Science, 0202 electrical engineering, electronic engineering, information engineering, Acyclic Rule, Uniqueness, Constraint satisfaction problem, Mathematics, Programming language, Nelson-Oppen Method, Cyclic Values, Proof assistant, SDG 16 - Peace, Justice and Strong Institutions, [INFO.INFO-LO]Computer Science [cs]/Logic in Computer Science [cs.LO], 020207 software engineering, DUAL (cognitive architecture), Solver, 16. Peace & justice, Justice and Strong Institutions, 020202 computer hardware & architecture, Datatype, Codatatypes, Automated theorem proving, TheoryofComputation_MATHEMATICALLOGICANDFORMALLANGUAGES, Computational Theory and Mathematics, 010201 computation theory & mathematics, TheoryofComputation_LOGICSANDMEANINGSOFPROGRAMS, Computer Science::Mathematical Software, 020201 artificial intelligence & image processing, computer, Software
Abstract

International audience; We present a decision procedure that combines reasoning about datatypes and codatatypes. The dual of the acyclicity rule for datatypes is a uniqueness rule that identifies observationally equal codatatype values, including cyclic values. The procedure decides universal problems and is composable via the Nelson–Oppen method. It has been implemented in CVC4, a state-of-the-art SMT solver. An evaluation based on problems generated from theories developed with Isabelle demonstrates the potential of the procedure.

Published
2017

3. Soundness and Completeness Proofs by Coinductive Methods

Author

Jasmin Christian Blanchette, Dmitriy Traytel, Andrei Popescu, Vrije Universiteit Amsterdam [Amsterdam] (VU), Max-Planck-Institut für Informatik (MPII), Max-Planck-Gesellschaft, Modeling and Verification of Distributed Algorithms and Systems (VERIDIS), Max-Planck-Gesellschaft-Max-Planck-Gesellschaft-Inria Nancy - Grand Est, Institut National de Recherche en Informatique et en Automatique (Inria)-Institut National de Recherche en Informatique et en Automatique (Inria)-Department of Formal Methods (LORIA - FM), Laboratoire Lorrain de Recherche en Informatique et ses Applications (LORIA), Institut National de Recherche en Informatique et en Automatique (Inria)-Université de Lorraine (UL)-Centre National de la Recherche Scientifique (CNRS)-Institut National de Recherche en Informatique et en Automatique (Inria)-Université de Lorraine (UL)-Centre National de la Recherche Scientifique (CNRS)-Laboratoire Lorrain de Recherche en Informatique et ses Applications (LORIA), Institut National de Recherche en Informatique et en Automatique (Inria)-Université de Lorraine (UL)-Centre National de la Recherche Scientifique (CNRS)-Université de Lorraine (UL)-Centre National de la Recherche Scientifique (CNRS), Middlesex University, Eidgenössische Technische Hochschule - Swiss Federal Institute of Technology [Zürich] (ETH Zürich), Centre National de la Recherche Scientifique (CNRS)-Université de Lorraine (UL)-Institut National de Recherche en Informatique et en Automatique (Inria)-Centre National de la Recherche Scientifique (CNRS)-Université de Lorraine (UL)-Institut National de Recherche en Informatique et en Automatique (Inria)-Laboratoire Lorrain de Recherche en Informatique et ses Applications (LORIA), Centre National de la Recherche Scientifique (CNRS)-Université de Lorraine (UL)-Institut National de Recherche en Informatique et en Automatique (Inria)-Centre National de la Recherche Scientifique (CNRS)-Université de Lorraine (UL), Department of Formal Methods (LORIA - FM), Institut National de Recherche en Informatique et en Automatique (Inria)-Université de Lorraine (UL)-Centre National de la Recherche Scientifique (CNRS)-Institut National de Recherche en Informatique et en Automatique (Inria)-Université de Lorraine (UL)-Centre National de la Recherche Scientifique (CNRS)-Inria Nancy - Grand Est, Institut National de Recherche en Informatique et en Automatique (Inria)-Max-Planck-Institut für Informatik (MPII), Max-Planck-Gesellschaft-Max-Planck-Gesellschaft, Theoretical Computer Science, and Network Institute

Subjects
Completeness, HOL, 02 engineering and technology, Isabelle/HOL, Mathematical proof, 01 natural sciences, Artificial Intelligence, Computer Science::Logic in Computer Science, 0202 electrical engineering, electronic engineering, information engineering, Calculus, Lazy evaluation, Gentian systems, 0101 mathematics, Mathematics, Soundness, Discrete mathematics, 010102 general mathematics, Coinduction, [INFO.INFO-LO]Computer Science [cs]/Logic in Computer Science [cs.LO], 020207 software engineering, Predicate (mathematical logic), Specification language, Corecursion, First-order logic, Codatatypes, TheoryofComputation_MATHEMATICALLOGICANDFORMALLANGUAGES, Computational Theory and Mathematics, Proof assistants, TheoryofComputation_LOGICSANDMEANINGSOFPROGRAMS, Computer Science::Programming Languages, Software
Abstract

International audience; We show how codatatypes can be employed to produce compact, high-level proofs of key results in logic: the soundness and completeness of proof systems for variations of first-order logic. For the classical completeness result, we first establish an abstract property of possibly infinite derivation trees. The abstract proof can be instantiated for a wide range of Gentzen and tableau systems for various flavors of first-order logic. Soundness becomes interesting as soon as one allows infinite proofs of first-order formulas. This forms the subject of several cyclic proof systems for first-order logic augmented with inductive predicate definitions studied in the literature. All the discussed results are formalized using Isa-belle/HOL's recently introduced support for codatatypes and corecursion. The development illustrates some unique features of Isabelle/HOL's new coinductive specification language such as nesting through non-free types and mixed recursion–corecursion.

Published
2016

4. A Learning-Based Fact Selector for Isabelle/HOL

Author

Cezary Kaliszyk, Josef Urban, Jasmin Christian Blanchette, David Greenaway, Daniel Kühlwein, Modeling and Verification of Distributed Algorithms and Systems (VERIDIS), Max-Planck-Institut für Informatik (MPII), Max-Planck-Gesellschaft-Max-Planck-Gesellschaft-Inria Nancy - Grand Est, Institut National de Recherche en Informatique et en Automatique (Inria)-Institut National de Recherche en Informatique et en Automatique (Inria)-Department of Formal Methods (LORIA - FM), Laboratoire Lorrain de Recherche en Informatique et ses Applications (LORIA), Institut National de Recherche en Informatique et en Automatique (Inria)-Université de Lorraine (UL)-Centre National de la Recherche Scientifique (CNRS)-Institut National de Recherche en Informatique et en Automatique (Inria)-Université de Lorraine (UL)-Centre National de la Recherche Scientifique (CNRS)-Laboratoire Lorrain de Recherche en Informatique et ses Applications (LORIA), Institut National de Recherche en Informatique et en Automatique (Inria)-Université de Lorraine (UL)-Centre National de la Recherche Scientifique (CNRS)-Université de Lorraine (UL)-Centre National de la Recherche Scientifique (CNRS), Max-Planck-Gesellschaft, Proof-oriented development of computer-based systems (MOSEL), Department of Formal Methods (LORIA - FM), Institut National de Recherche en Informatique et en Automatique (Inria)-Université de Lorraine (UL)-Centre National de la Recherche Scientifique (CNRS)-Institut National de Recherche en Informatique et en Automatique (Inria)-Université de Lorraine (UL)-Centre National de la Recherche Scientifique (CNRS), National ICT Australia [Sydney] (NICTA), University of New South Wales [Sydney] (UNSW), Leopold Franzens Universität Innsbruck - University of Innsbruck, Radboud University [Nijmegen], Czech Technical University in Prague (CTU), Centre National de la Recherche Scientifique (CNRS)-Université de Lorraine (UL)-Institut National de Recherche en Informatique et en Automatique (Inria)-Centre National de la Recherche Scientifique (CNRS)-Université de Lorraine (UL)-Institut National de Recherche en Informatique et en Automatique (Inria)-Laboratoire Lorrain de Recherche en Informatique et ses Applications (LORIA), Centre National de la Recherche Scientifique (CNRS)-Université de Lorraine (UL)-Institut National de Recherche en Informatique et en Automatique (Inria)-Centre National de la Recherche Scientifique (CNRS)-Université de Lorraine (UL), Centre National de la Recherche Scientifique (CNRS)-Université de Lorraine (UL)-Institut National de Recherche en Informatique et en Automatique (Inria)-Centre National de la Recherche Scientifique (CNRS)-Université de Lorraine (UL)-Institut National de Recherche en Informatique et en Automatique (Inria), University of Innsbruck, and Radboud university [Nijmegen]

Subjects
Theoretical computer science, Computer science, HOL, 0102 computer and information sciences, 02 engineering and technology, Mathematical proof, computer.software_genre, 01 natural sciences, Set (abstract data type), Artificial Intelligence, Server, Component (UML), 0202 electrical engineering, electronic engineering, information engineering, Axiom, Programming language, Proof assistant, Data Science, [INFO.INFO-LO]Computer Science [cs]/Logic in Computer Science [cs.LO], 020207 software engineering, Workflow, TheoryofComputation_MATHEMATICALLOGICANDFORMALLANGUAGES, Computational Theory and Mathematics, 010201 computation theory & mathematics, TheoryofComputation_LOGICSANDMEANINGSOFPROGRAMS, ComputingMethodologies_DOCUMENTANDTEXTPROCESSING, computer, Software
Abstract

Sledgehammer integrates automatic theorem provers in the proof assistant Isabelle/HOL. A key component, the fact selector, heuristically ranks the thousands of facts (lemmas, definitions, or axioms) available and selects a subset, based on syntactic similarity to the current proof goal. We introduce MaSh, an alternative that learns from successful proofs. New challenges arose from our “zero click” vision: MaSh integrates seamlessly with the users’ workflow, so that they benefit from machine learning without having to install software, set up servers, or guide the learning. MaSh outperforms the old fact selector on large formalizations.

Published
2016

5. Polite Combination of Algebraic Datatypes

Author

Ying Sheng, Yoni Zohar, Christophe Ringeissen, Jane Lange, Pascal Fontaine, Clark Barrett, Computer Science Department [Stanford], Stanford University, Department of Computer Science at Bar Ilan University, Bar-Ilan University [Israël], Proof techniques for security protocols (PESTO), Inria Nancy - Grand Est, Institut National de Recherche en Informatique et en Automatique (Inria)-Institut National de Recherche en Informatique et en Automatique (Inria)-Department of Formal Methods (LORIA - FM), Laboratoire Lorrain de Recherche en Informatique et ses Applications (LORIA), Institut National de Recherche en Informatique et en Automatique (Inria)-Université de Lorraine (UL)-Centre National de la Recherche Scientifique (CNRS)-Institut National de Recherche en Informatique et en Automatique (Inria)-Université de Lorraine (UL)-Centre National de la Recherche Scientifique (CNRS)-Laboratoire Lorrain de Recherche en Informatique et ses Applications (LORIA), Institut National de Recherche en Informatique et en Automatique (Inria)-Université de Lorraine (UL)-Centre National de la Recherche Scientifique (CNRS)-Université de Lorraine (UL)-Centre National de la Recherche Scientifique (CNRS), Massachusetts Institute of Technology, Computer Science and Artificial Intelligence Laboratory, Université de Liège, Modeling and Verification of Distributed Algorithms and Systems (VERIDIS), Max-Planck-Institut für Informatik (MPII), and Max-Planck-Gesellschaft-Max-Planck-Gesellschaft-Inria Nancy - Grand Est

Subjects
Algebraic datatypes, Satisfiability Modulo Theories, Polite combination, Computational Theory and Mathematics, Artificial Intelligence, [INFO.INFO-LO]Computer Science [cs]/Logic in Computer Science [cs.LO], Automated reasoning, Theory combination, Software
Abstract

International audience; Algebraic datatypes, and among them lists and trees, have attracted a lot of interest in automated reasoning and Satisfiability Modulo Theories (SMT). Since its latest stable version, the SMT-LIB standard defines a theory of algebraic datatypes, which is currently supported by several mainstream SMT solvers. In this paper, we study this particular theory of datatypes and prove that it is strongly polite, showing how it can be combined with other arbitrary disjoint theories using polite combination. The combination method uses a new, simple, and natural notion of additivity that enables deducing strong politeness from (weak) politeness.

Published
2022

6. A Posthumous Contribution by Larry Wos: Excerpts from an Unpublished Column

Author

Sophie Tourret, Christoph Weidenbach, Modeling and Verification of Distributed Algorithms and Systems (VERIDIS), Max-Planck-Institut für Informatik (MPII), Max-Planck-Gesellschaft-Max-Planck-Gesellschaft-Inria Nancy - Grand Est, Institut National de Recherche en Informatique et en Automatique (Inria)-Institut National de Recherche en Informatique et en Automatique (Inria)-Department of Formal Methods (LORIA - FM), Laboratoire Lorrain de Recherche en Informatique et ses Applications (LORIA), Institut National de Recherche en Informatique et en Automatique (Inria)-Université de Lorraine (UL)-Centre National de la Recherche Scientifique (CNRS)-Institut National de Recherche en Informatique et en Automatique (Inria)-Université de Lorraine (UL)-Centre National de la Recherche Scientifique (CNRS)-Laboratoire Lorrain de Recherche en Informatique et ses Applications (LORIA), Institut National de Recherche en Informatique et en Automatique (Inria)-Université de Lorraine (UL)-Centre National de la Recherche Scientifique (CNRS)-Université de Lorraine (UL)-Centre National de la Recherche Scientifique (CNRS), Inria Nancy - Grand Est, Institut National de Recherche en Informatique et en Automatique (Inria), and Max Planck Institute for Informatics [Saarbrücken]

Subjects
History of automated reasoning, Reasoning by instantiation, Puzzle, Computational Theory and Mathematics, Artificial Intelligence, First-order logic modulo arithmetic, Set of support, [INFO.INFO-LO]Computer Science [cs]/Logic in Computer Science [cs.LO], Software
Abstract

Shortly before Larry Wos passed away, he sent a manuscript for discussion to Sophie Tourret, the editor of the AAR newsletter. We present excerpts from this final manuscript, put it in its historic context and explain its relevance for today’s research in automated reasoning.

Published
2022

7. A Decidable Class of Security Protocols for Both Reachability and Equivalence Properties

Author

Stéphanie Delaune, Véronique Cortier, Vaishnavi Sundararajan, Proof techniques for security protocols (PESTO), Inria Nancy - Grand Est, Institut National de Recherche en Informatique et en Automatique (Inria)-Institut National de Recherche en Informatique et en Automatique (Inria)-Department of Formal Methods (LORIA - FM), Laboratoire Lorrain de Recherche en Informatique et ses Applications (LORIA), Institut National de Recherche en Informatique et en Automatique (Inria)-Université de Lorraine (UL)-Centre National de la Recherche Scientifique (CNRS)-Institut National de Recherche en Informatique et en Automatique (Inria)-Université de Lorraine (UL)-Centre National de la Recherche Scientifique (CNRS)-Laboratoire Lorrain de Recherche en Informatique et ses Applications (LORIA), Institut National de Recherche en Informatique et en Automatique (Inria)-Université de Lorraine (UL)-Centre National de la Recherche Scientifique (CNRS)-Université de Lorraine (UL)-Centre National de la Recherche Scientifique (CNRS), Institut de Recherche en Informatique et Systèmes Aléatoires (IRISA), Université de Rennes (UR)-Institut National des Sciences Appliquées - Rennes (INSA Rennes), Institut National des Sciences Appliquées (INSA)-Institut National des Sciences Appliquées (INSA)-Université de Bretagne Sud (UBS)-École normale supérieure - Rennes (ENS Rennes)-Institut National de Recherche en Informatique et en Automatique (Inria)-CentraleSupélec-Centre National de la Recherche Scientifique (CNRS)-IMT Atlantique (IMT Atlantique), Institut Mines-Télécom [Paris] (IMT)-Institut Mines-Télécom [Paris] (IMT), Security & PrIvaCY (SPICY), SYSTÈMES LARGE ÉCHELLE (IRISA-D1), Institut Mines-Télécom [Paris] (IMT)-Institut Mines-Télécom [Paris] (IMT)-Université de Rennes (UR)-Institut National des Sciences Appliquées - Rennes (INSA Rennes), Institut Mines-Télécom [Paris] (IMT)-Institut Mines-Télécom [Paris] (IMT)-Institut de Recherche en Informatique et Systèmes Aléatoires (IRISA), Institut National des Sciences Appliquées (INSA)-Institut National des Sciences Appliquées (INSA)-Université de Bretagne Sud (UBS)-École normale supérieure - Rennes (ENS Rennes)-Institut National de Recherche en Informatique et en Automatique (Inria)-Télécom Bretagne-CentraleSupélec-Centre National de la Recherche Scientifique (CNRS)-Université de Rennes (UR)-Institut National des Sciences Appliquées - Rennes (INSA Rennes), Institut National des Sciences Appliquées (INSA)-Institut National des Sciences Appliquées (INSA)-Université de Bretagne Sud (UBS)-École normale supérieure - Rennes (ENS Rennes)-Institut National de Recherche en Informatique et en Automatique (Inria)-Télécom Bretagne-CentraleSupélec-Centre National de la Recherche Scientifique (CNRS), The research leading to these results has received funding from the European Research Council under the European Union’s horizon 2020 research and innovation program (ERC grant agreement n◦ 714955-POPSTAR and ERC grant agreement n◦ 645865-SPOOC), as well as from the French National Research Agency (ANR) under the project TECAP., ANR-17-CE39-0004,TECAP,Analyse de protocoles - unir les outils existants(2017), European Project: 714955,H2020,ERC-2016-STG,ERC-POPSTAR(2017), European Project: 645865,H2020 ERC,ERC-2014-CoG,SPOOC(2015), Université de Bretagne Sud (UBS)-Institut National des Sciences Appliquées - Rennes (INSA Rennes), Institut National des Sciences Appliquées (INSA)-Université de Rennes (UNIV-RENNES)-Institut National des Sciences Appliquées (INSA)-Université de Rennes (UNIV-RENNES)-Institut National de Recherche en Informatique et en Automatique (Inria)-École normale supérieure - Rennes (ENS Rennes)-Centre National de la Recherche Scientifique (CNRS)-Université de Rennes 1 (UR1), and Université de Rennes (UNIV-RENNES)-CentraleSupélec-IMT Atlantique Bretagne-Pays de la Loire (IMT Atlantique)

Subjects
Theoretical computer science, Cryptographic primitive, Computer science, business.industry, Verification, Privacy properties, 020207 software engineering, 0102 computer and information sciences, 02 engineering and technology, Cryptographic protocol, Encryption, 01 natural sciences, Security protocols, Decidability, [INFO.INFO-CR]Computer Science [cs]/Cryptography and Security [cs.CR], Dependency graph, Computational Theory and Mathematics, 010201 computation theory & mathematics, Artificial Intelligence, Reachability, 0202 electrical engineering, electronic engineering, information engineering, Equivalence (formal languages), business, Software, Cryptographic nonce
Abstract

International audience; We identify a new decidable class of security protocols, both for reachability and equivalence properties. Our result holds for an unbounded number of sessions and for protocols with nonces. It covers all standard cryptographic primitives. Our class sets up three main assumptions. (i) Protocols need to be "simple", meaning that an attacker can precisely identify from which participant and which session a message originates from. We also consider protocols with no else branches (only positive test). (ii) Protocols should be type-compliant, which is intuitively guaranteed as soon as two encrypted messages of the protocol cannot be confused. (iii) Finally, we define the notion of a dependency graph, which, given a protocol, characterises how actions depend on the other ones (both sequential dependencies and data dependencies are taken into account). Whenever the graph is acyclic, then the protocol falls into our class. We show that many protocols of the literature belong to our decidable class, including for example some of the protocols embedded in the biometric passport.

Published
2020

8. Decidable $${\exists }^*{\forall }^*$$ First-Order Fragments of Linear Rational Arithmetic with Uninterpreted Predicates

Author

Marco Voigt, Max Planck Institute for Informatics [Saarbrücken], Modeling and Verification of Distributed Algorithms and Systems (VERIDIS), Max-Planck-Institut für Informatik (MPII), Max-Planck-Gesellschaft-Max-Planck-Gesellschaft-Inria Nancy - Grand Est, Institut National de Recherche en Informatique et en Automatique (Inria)-Institut National de Recherche en Informatique et en Automatique (Inria)-Department of Formal Methods (LORIA - FM), Laboratoire Lorrain de Recherche en Informatique et ses Applications (LORIA), Institut National de Recherche en Informatique et en Automatique (Inria)-Université de Lorraine (UL)-Centre National de la Recherche Scientifique (CNRS)-Institut National de Recherche en Informatique et en Automatique (Inria)-Université de Lorraine (UL)-Centre National de la Recherche Scientifique (CNRS)-Laboratoire Lorrain de Recherche en Informatique et ses Applications (LORIA), and Institut National de Recherche en Informatique et en Automatique (Inria)-Université de Lorraine (UL)-Centre National de la Recherche Scientifique (CNRS)-Université de Lorraine (UL)-Centre National de la Recherche Scientifique (CNRS)

Subjects
Rational number, Finite model property, Arity, Decidability, Undecidable problem, Computational Theory and Mathematics, Fragment (logic), Artificial Intelligence, Bounded function, [INFO]Computer Science [cs], Arithmetic, Boolean satisfiability problem, Software, Mathematics
Abstract

International audience; First-order linear rational arithmetic enriched with uninterpreted predicates yields an interesting and very expressive modeling language. However, already the presence of a single uninterpreted predicate symbol of arity one or greater renders the associated satisfiability problem undecidable. We identify two decidable fragments, both based on the Bernays– Schönfinkel–Ramsey prefix class. Due to the inherent infiniteness of the underlying domain, a finite model property in the usual sense cannot be established. Nevertheless, we show that satisfiable sentences always have a model that can be described by finite means. To this end, we restrict the syntax of arithmetic atoms. In the first fragment that is presented, arithmetic operations are only allowed over termswithout universally quantified variables. In the second fragment, arithmetic atoms are essentially confined to difference constraints over universally quantified variables with bounded range. We will call such atoms bounded difference constraints. As bounded intervals over the rationals still comprise infinitely many values, a trivial instantiation procedure is not sufficient to solve the satisfiability problem. After a slight shift of perspective, the positive decidability result for the first fragment can be restated in the framework of combinations of theories over non-disjoint vocabularies. More precisely, we combine first-order theories that share a dense total order without endpoints.

Published
2020

9. Politeness and Combination Methods for Theories with Bridging Functions

Author

Christophe Ringeissen, Pascal Fontaine, Paula Chocron, European Research Council, Artificial Intelligence Research Institute / Spanish Scientific Research Council (IIIA / CSIC), Universitat Autònoma de Barcelona (UAB), Modeling and Verification of Distributed Algorithms and Systems (VERIDIS), Department of Formal Methods (LORIA - FM), Laboratoire Lorrain de Recherche en Informatique et ses Applications (LORIA), Institut National de Recherche en Informatique et en Automatique (Inria)-Université de Lorraine (UL)-Centre National de la Recherche Scientifique (CNRS)-Institut National de Recherche en Informatique et en Automatique (Inria)-Université de Lorraine (UL)-Centre National de la Recherche Scientifique (CNRS)-Laboratoire Lorrain de Recherche en Informatique et ses Applications (LORIA), Institut National de Recherche en Informatique et en Automatique (Inria)-Université de Lorraine (UL)-Centre National de la Recherche Scientifique (CNRS)-Institut National de Recherche en Informatique et en Automatique (Inria)-Université de Lorraine (UL)-Centre National de la Recherche Scientifique (CNRS)-Inria Nancy - Grand Est, Institut National de Recherche en Informatique et en Automatique (Inria)-Max-Planck-Institut für Informatik (MPII), Max-Planck-Gesellschaft-Max-Planck-Gesellschaft, Proof-oriented development of computer-based systems (MOSEL), Institut National de Recherche en Informatique et en Automatique (Inria)-Université de Lorraine (UL)-Centre National de la Recherche Scientifique (CNRS)-Institut National de Recherche en Informatique et en Automatique (Inria)-Université de Lorraine (UL)-Centre National de la Recherche Scientifique (CNRS), Proof techniques for security protocols (PESTO), Inria Nancy - Grand Est, Institut National de Recherche en Informatique et en Automatique (Inria)-Institut National de Recherche en Informatique et en Automatique (Inria)-Department of Formal Methods (LORIA - FM), Institut National de Recherche en Informatique et en Automatique (Inria)-Université de Lorraine (UL)-Centre National de la Recherche Scientifique (CNRS)-Université de Lorraine (UL)-Centre National de la Recherche Scientifique (CNRS), This work has been partially supported by the European Research Council (ERC) starting grant Matryoshka (713999)., European Project: 713999,H2020,Matryoshka(2017), Max-Planck-Institut für Informatik (MPII), and Max-Planck-Gesellschaft-Max-Planck-Gesellschaft-Inria Nancy - Grand Est

Subjects
Non-disjoint theories, Combination method, Computer science, media_common.quotation_subject, Combination Method, 0102 computer and information sciences, 02 engineering and technology, Disjoint sets, 01 natural sciences, Bridging (programming), Bridging functions, Artificial Intelligence, Satisfiability modulo theories, 0202 electrical engineering, electronic engineering, information engineering, Bridging Functions, media_common, Non-Disjoint Theories, Politeness, [INFO.INFO-LO]Computer Science [cs]/Logic in Computer Science [cs.LO], 020207 software engineering, Data structure, Decidability, Algebra, Satisfiability Modulo Theories, Computational Theory and Mathematics, 010201 computation theory & mathematics, Software
Abstract

The Nelson–Oppen combination method is ubiquitous in Satisfiability Modulo Theories solvers. However, one of its major drawbacks is to be restricted to disjoint unions of theories. We investigate the problem of extending this combination method to particular non-disjoint unions of theories defined by connecting disjoint theories via bridging functions. A possible application is to solve verification problems expressed in a combination of data structures connected to arithmetic with bridging functions such as the length of lists and the size of trees. We present a sound and complete combination method à la Nelson–Oppen for the theory of absolutely free data structures, including lists and trees. This combination procedure is then refined for standard interpretations. The resulting theory has a nice politeness property, enabling combinations with arbitrary decidable theories of elements. In addition, we have identified a class of polite data structure theories for which the combination method remains sound and complete. This class includes all the subtheories of absolutely free data structures (e.g, the empty theory, injectivity, projection). Again, the politeness property holds for any theory in this class, which can thus be combined with bridging functions and arbitrary decidable theories of elements. This illustrates the significance of politeness in the context of non-disjoint combinations of theories., This work has been partially supported by the European Research Council (ERC) starting Grant Matryoshka (713999)

Full Text
View/download PDF

10. Reducing Equational Theories for the Decision of Static Equivalence

Author

Antoine Mercier, Steve Kremer, Ralf Treinen, Laboratoire Spécification et Vérification [Cachan] (LSV), École normale supérieure - Cachan (ENS Cachan)-Centre National de la Recherche Scientifique (CNRS), Preuves, Programmes et Systèmes (PPS), Université Paris Diderot - Paris 7 (UPD7)-Centre National de la Recherche Scientifique (CNRS), Anupam Datta, Combination of approaches to the security of infinite states systems (CASSIS), Franche-Comté Électronique Mécanique, Thermique et Optique - Sciences et Technologies (UMR 6174) (FEMTO-ST), Université de Technologie de Belfort-Montbeliard (UTBM)-Ecole Nationale Supérieure de Mécanique et des Microtechniques (ENSMM)-Centre National de la Recherche Scientifique (CNRS)-Université de Franche-Comté (UFC), Université Bourgogne Franche-Comté [COMUE] (UBFC)-Université Bourgogne Franche-Comté [COMUE] (UBFC)-Université de Technologie de Belfort-Montbeliard (UTBM)-Ecole Nationale Supérieure de Mécanique et des Microtechniques (ENSMM)-Centre National de la Recherche Scientifique (CNRS)-Université de Franche-Comté (UFC), Université Bourgogne Franche-Comté [COMUE] (UBFC)-Université Bourgogne Franche-Comté [COMUE] (UBFC)-Inria Nancy - Grand Est, Institut National de Recherche en Informatique et en Automatique (Inria)-Institut National de Recherche en Informatique et en Automatique (Inria)-Department of Formal Methods (LORIA - FM), Laboratoire Lorrain de Recherche en Informatique et ses Applications (LORIA), Institut National de Recherche en Informatique et en Automatique (Inria)-Université de Lorraine (UL)-Centre National de la Recherche Scientifique (CNRS)-Institut National de Recherche en Informatique et en Automatique (Inria)-Université de Lorraine (UL)-Centre National de la Recherche Scientifique (CNRS)-Laboratoire Lorrain de Recherche en Informatique et ses Applications (LORIA), Institut National de Recherche en Informatique et en Automatique (Inria)-Université de Lorraine (UL)-Centre National de la Recherche Scientifique (CNRS)-Université de Lorraine (UL)-Centre National de la Recherche Scientifique (CNRS), Centre National de la Recherche Scientifique (CNRS)-Université Paris Diderot - Paris 7 (UPD7), Université de Technologie de Belfort-Montbeliard (UTBM)-Ecole Nationale Supérieure de Mécanique et des Microtechniques (ENSMM)-Université de Franche-Comté (UFC), Université Bourgogne Franche-Comté [COMUE] (UBFC)-Université Bourgogne Franche-Comté [COMUE] (UBFC)-Centre National de la Recherche Scientifique (CNRS)-Université de Technologie de Belfort-Montbeliard (UTBM)-Ecole Nationale Supérieure de Mécanique et des Microtechniques (ENSMM)-Université de Franche-Comté (UFC), and Université Bourgogne Franche-Comté [COMUE] (UBFC)-Université Bourgogne Franche-Comté [COMUE] (UBFC)-Centre National de la Recherche Scientifique (CNRS)-Inria Nancy - Grand Est

Subjects
Theoretical computer science, Logical equivalence, Modulo, Bilinear interpolation, 0102 computer and information sciences, 02 engineering and technology, 01 natural sciences, [INFO.INFO-CR]Computer Science [cs]/Cryptography and Security [cs.CR], Artificial Intelligence, ComputingMethodologies_SYMBOLICANDALGEBRAICMANIPULATION, 0202 electrical engineering, electronic engineering, information engineering, Equivalence (formal languages), Axiom, Mathematics, Cryptographic primitive, [INFO.INFO-LO]Computer Science [cs]/Logic in Computer Science [cs.LO], Bilinear pairing, 020206 networking & telecommunications, Cryptographic protocol, 16. Peace & justice, Formal methods, Algebra, Computational Theory and Mathematics, 010201 computation theory & mathematics, Algorithm, Software
Abstract

International audience; Static equivalence is a well established notion of indistinguishability of sequences of terms which is useful in the symbolic analysis of cryptographic protocols. Static equivalence modulo equational theories allows for a more accurate representation of cryptographic primitives by modelling properties of operators by equational axioms. We develop a method that allows us in some cases to simplify the task of deciding static equivalence in a multi-sorted setting, by removing a symbol from the term signature and reducing the problem to several simpler equational theories. We illustrate our technique at hand of bilinear pairings.

Published
2010

11. Computing Knowledge in Security Protocols Under Convergent Equational Theories

Author

Ştefan Ciobâcă, Stéphanie Delaune, Steve Kremer, Laboratoire Spécification et Vérification [Cachan] (LSV), École normale supérieure - Cachan (ENS Cachan)-Centre National de la Recherche Scientifique (CNRS), Security of information systems (SECSI), École normale supérieure - Cachan (ENS Cachan)-Centre National de la Recherche Scientifique (CNRS)-École normale supérieure - Cachan (ENS Cachan)-Centre National de la Recherche Scientifique (CNRS)-Inria Saclay - Ile de France, Institut National de Recherche en Informatique et en Automatique (Inria)-Institut National de Recherche en Informatique et en Automatique (Inria), Combination of approaches to the security of infinite states systems (CASSIS), Franche-Comté Électronique Mécanique, Thermique et Optique - Sciences et Technologies (UMR 6174) (FEMTO-ST), Université de Technologie de Belfort-Montbeliard (UTBM)-Ecole Nationale Supérieure de Mécanique et des Microtechniques (ENSMM)-Université de Franche-Comté (UFC), Université Bourgogne Franche-Comté [COMUE] (UBFC)-Université Bourgogne Franche-Comté [COMUE] (UBFC)-Centre National de la Recherche Scientifique (CNRS)-Université de Technologie de Belfort-Montbeliard (UTBM)-Ecole Nationale Supérieure de Mécanique et des Microtechniques (ENSMM)-Université de Franche-Comté (UFC), Université Bourgogne Franche-Comté [COMUE] (UBFC)-Université Bourgogne Franche-Comté [COMUE] (UBFC)-Centre National de la Recherche Scientifique (CNRS)-Inria Nancy - Grand Est, Institut National de Recherche en Informatique et en Automatique (Inria)-Institut National de Recherche en Informatique et en Automatique (Inria)-Department of Formal Methods (LORIA - FM), Laboratoire Lorrain de Recherche en Informatique et ses Applications (LORIA), Institut National de Recherche en Informatique et en Automatique (Inria)-Université de Lorraine (UL)-Centre National de la Recherche Scientifique (CNRS)-Institut National de Recherche en Informatique et en Automatique (Inria)-Université de Lorraine (UL)-Centre National de la Recherche Scientifique (CNRS)-Laboratoire Lorrain de Recherche en Informatique et ses Applications (LORIA), Institut National de Recherche en Informatique et en Automatique (Inria)-Université de Lorraine (UL)-Centre National de la Recherche Scientifique (CNRS)-Université de Lorraine (UL)-Centre National de la Recherche Scientifique (CNRS), Université de Technologie de Belfort-Montbeliard (UTBM)-Ecole Nationale Supérieure de Mécanique et des Microtechniques (ENSMM)-Centre National de la Recherche Scientifique (CNRS)-Université de Franche-Comté (UFC), Université Bourgogne Franche-Comté [COMUE] (UBFC)-Université Bourgogne Franche-Comté [COMUE] (UBFC)-Université de Technologie de Belfort-Montbeliard (UTBM)-Ecole Nationale Supérieure de Mécanique et des Microtechniques (ENSMM)-Centre National de la Recherche Scientifique (CNRS)-Université de Franche-Comté (UFC), and Université Bourgogne Franche-Comté [COMUE] (UBFC)-Université Bourgogne Franche-Comté [COMUE] (UBFC)-Inria Nancy - Grand Est

Subjects
Cryptographic primitive, Theoretical computer science, business.industry, 0102 computer and information sciences, 02 engineering and technology, Decision problem, Cryptographic protocol, Formal methods, Encryption, 01 natural sciences, Term algebra, Undecidable problem, Decidability, [INFO.INFO-CR]Computer Science [cs]/Cryptography and Security [cs.CR], Computational Theory and Mathematics, 010201 computation theory & mathematics, Artificial Intelligence, 0202 electrical engineering, electronic engineering, information engineering, 020201 artificial intelligence & image processing, business, Software, Computer Science::Cryptography and Security, Mathematics
Abstract

International audience; The analysis of security protocols requires reasoning about the knowledge an attacker acquires by eavesdropping on network traffic. In formal approaches, the messages exchanged over the network are modeled by a term algebra equipped with an equational theory axiomatizing the properties of the cryptographic primitives (e.g. encryption, signature). In this context, two classical notions of knowledge, deducibility and indistinguishability, yield corresponding decision problems.\par We propose a procedure for both problems under arbitrary convergent equational theories. Since the underlying problems are undecidable we cannot guarantee termination. Nevertheless, our procedure terminates on a wide range of equational theories. In particular, we obtain a new decidability result for a theory we encountered when studying electronic voting protocols. We also provide a prototype implementation.

Published
2010

12. A Survey of Symbolic Methods in Computational Analysis of Cryptographic Systems

Author

Véronique Cortier, Bogdan Warinschi, Steve Kremer, Combination of approaches to the security of infinite states systems (CASSIS), Franche-Comté Électronique Mécanique, Thermique et Optique - Sciences et Technologies (UMR 6174) (FEMTO-ST), Université de Technologie de Belfort-Montbeliard (UTBM)-Ecole Nationale Supérieure de Mécanique et des Microtechniques (ENSMM)-Centre National de la Recherche Scientifique (CNRS)-Université de Franche-Comté (UFC), Université Bourgogne Franche-Comté [COMUE] (UBFC)-Université Bourgogne Franche-Comté [COMUE] (UBFC)-Université de Technologie de Belfort-Montbeliard (UTBM)-Ecole Nationale Supérieure de Mécanique et des Microtechniques (ENSMM)-Centre National de la Recherche Scientifique (CNRS)-Université de Franche-Comté (UFC), Université Bourgogne Franche-Comté [COMUE] (UBFC)-Université Bourgogne Franche-Comté [COMUE] (UBFC)-Inria Nancy - Grand Est, Institut National de Recherche en Informatique et en Automatique (Inria)-Institut National de Recherche en Informatique et en Automatique (Inria)-Department of Formal Methods (LORIA - FM), Laboratoire Lorrain de Recherche en Informatique et ses Applications (LORIA), Institut National de Recherche en Informatique et en Automatique (Inria)-Université de Lorraine (UL)-Centre National de la Recherche Scientifique (CNRS)-Institut National de Recherche en Informatique et en Automatique (Inria)-Université de Lorraine (UL)-Centre National de la Recherche Scientifique (CNRS)-Laboratoire Lorrain de Recherche en Informatique et ses Applications (LORIA), Institut National de Recherche en Informatique et en Automatique (Inria)-Université de Lorraine (UL)-Centre National de la Recherche Scientifique (CNRS)-Université de Lorraine (UL)-Centre National de la Recherche Scientifique (CNRS), Laboratoire Spécification et Vérification [Cachan] (LSV), École normale supérieure - Cachan (ENS Cachan)-Centre National de la Recherche Scientifique (CNRS), Computer Science Department [Bristol], University of Bristol [Bristol], ANR-07-SESU-0002,AVOTE,Analyse formelle de protocoles de vote électronique(2007), Université de Technologie de Belfort-Montbeliard (UTBM)-Ecole Nationale Supérieure de Mécanique et des Microtechniques (ENSMM)-Université de Franche-Comté (UFC), Université Bourgogne Franche-Comté [COMUE] (UBFC)-Université Bourgogne Franche-Comté [COMUE] (UBFC)-Centre National de la Recherche Scientifique (CNRS)-Université de Technologie de Belfort-Montbeliard (UTBM)-Ecole Nationale Supérieure de Mécanique et des Microtechniques (ENSMM)-Université de Franche-Comté (UFC), Université Bourgogne Franche-Comté [COMUE] (UBFC)-Université Bourgogne Franche-Comté [COMUE] (UBFC)-Centre National de la Recherche Scientifique (CNRS)-Inria Nancy - Grand Est, Centre National de la Recherche Scientifique (CNRS)-Université de Lorraine (UL)-Institut National de Recherche en Informatique et en Automatique (Inria)-Centre National de la Recherche Scientifique (CNRS)-Université de Lorraine (UL)-Institut National de Recherche en Informatique et en Automatique (Inria)-Laboratoire Lorrain de Recherche en Informatique et ses Applications (LORIA), and Centre National de la Recherche Scientifique (CNRS)-Université de Lorraine (UL)-Institut National de Recherche en Informatique et en Automatique (Inria)-Centre National de la Recherche Scientifique (CNRS)-Université de Lorraine (UL)

Subjects
Theoretical computer science, Computer science, 0211 other engineering and technologies, Context (language use), Cryptography, 0102 computer and information sciences, 02 engineering and technology, 01 natural sciences, Computational hardness assumption, [INFO.INFO-CR]Computer Science [cs]/Cryptography and Security [cs.CR], Artificial Intelligence, symbolic methods, Soundness, 021110 strategic, defence & security studies, Computational model, cryptography, Cryptographic primitive, business.industry, Probabilistic logic, security protocol, Cryptographic protocol, 16. Peace & justice, Computational Theory and Mathematics, 010201 computation theory & mathematics, computational analysis, Artificial intelligence, business, Software
Abstract

International audience; Since the 1980s, two approaches have been developed for analyzing security protocols. One of the approaches relies on a computational model that considers issues of complexity and probability. This approach captures a strong notion of security, guaranteed against all probabilistic polynomial-time attacks. The other approach relies on a symbolic model of protocol executions in which cryptographic primitives are treated as black boxes. Since the seminal work of Dolev and Yao, it has been realized that this latter approach enables significantly simpler and often automated proofs. However, the guarantees that it offers with respect to the more detailed computational models have been quite unclear. For more than twenty years the two approaches have coexisted but evolved mostly independently. Recently, significant research efforts attempt to develop paradigms for cryptographic systems analysis that combines the best of both worlds. There are two broad directions that have been followed. Computational soundness aims to establish sufficient conditions under which results obtained using symbolic models imply security under computational models. The direct approach aims to apply the principles and the techniques developed in the context of symbolic models directly to computational ones. In this paper we survey existing results along both of these directions. Our goal is to provide a rather complete summary that could act as a quick reference for researchers who want to contribute to the field, want to make use of existing results, or just want to get a better picture of what results already exist.

Published
2010

Catalog

Books, media, physical & digital resources
See catalog results