Skip to Main content Skip to Navigation

hal-00762252v1  Conference papers
Philippe BeaucampsIsabelle GnaedigJean-Yves Marion. Abstraction-based Malware Analysis Using Rewriting and Model Checking
ESORICS - 17th European Symposium on Research in Computer Security - 2012, Sep 2012, Pisa, Italy. pp.806-823, ⟨10.1007/978-3-642-33167-1⟩
inria-00349353v1  Conference papers
Carlos OlarteFrank D. Valencia. The Expressivity of Universal Timed CCP: Undecidability of Monadic FLTL and Closure Operators for Security
10th International ACM SIGPLAN Conference on Principles and Practice of Declarative Programming, ACM, Jul 2008, Valencia, Spain. pp.8-19, ⟨10.1145/1389449.1389452⟩
hal-00192051v1  Journal articles
Thomas ColcombetChristof Löding. Transforming structures by set interpretations
Logical Methods in Computer Science, Logical Methods in Computer Science Association, 2007, 3 (2), paper 4. ⟨10.2168/LMCS-3(2:4)2007⟩
hal-02998767v1  Journal articles
Mathilde BouvelValentin FerayMichael Albert. Two first-order logics of permutations
Journal of Combinatorial Theory, Series A, Elsevier, 2020, 171, pp.105-158. ⟨10.1016/j.jcta.2019.105158⟩
hal-01342849v1  Conference papers
Pierre Halmagrand. Soundly Proving B Method Formulae Using Typed Sequent Calculus
13th International Colloquium on Theoretical Aspects of Computing (ICTAC), Oct 2016, Taipei, Taiwan. pp 196-213, ⟨10.1007/978-3-319-46750-4_12⟩
hal-01242509v1  Conference papers
Andrew ReynoldsJasmin Christian BlanchetteCesare Tinelli. Model Finding for Recursive Functions in SMT
SMT Workshop 2015 - 13th International Workshop on on Satisfiability Modulo Theories, Jul 2015, San Francisco, United States
tel-02406821v1  Theses
Marco Voigt. Decidable Fragments of First-Order Logic and of First-Order Linear Arithmetic with Uninterpreted Predicates
Logic in Computer Science [cs.LO]. Universität des Saarlandes, 2019. English
tel-01592497v1  Theses
Daniel Wand. Superposition: Types and Induction
Computer Science [cs]. Saarland University, 2017. English
inria-00074344v1  Reports
Stéphane GrumbachChristophe Tollu. On the Expressive Power of Counting
[Research Report] RR-2330, INRIA. 1992, pp.38
lirmm-00410129v1  Conference papers
Marie-Laure Mugnier. Conceptual Graph Rules and Equivalent Rules: A Synthesis
ICCS: International Conference on Conceptual Structures, Jul 2009, Moscow, Russia. pp.23-31, ⟨10.1007/978-3-642-03079-6_3⟩
hal-02882118v1  Conference papers
Julien Grange. Successor-Invariant First-Order Logic on Classes of Bounded Degree
LICS 2020 - Thirty-Fifth Annual ACM/IEEE Symposium on Logic in Computer Science, Jul 2020, Saarbrücken / Virtual, Germany. ⟨10.1145/3373718.3394767⟩
hal-02310749v2  Conference papers
Julien GrangeLuc Segoufin. Order-Invariant First-Order Logic over Hollow Trees
CSL 2020 - 28th annual conference of the European Association for Computer Science Logic, Jan 2020, Barcelona, Spain. pp.1-23, ⟨10.4230/LIPIcs.CSL.2020.23⟩
tel-02947853v1  Theses
Julien Grange. On the Expressive Power of Invariant Logics over Sparse Classes of Structures
Logic in Computer Science [cs.LO]. ENS Paris, 2020. English
lirmm-00535780v1  Conference papers
Jean-François BagetMichel LeclèreMarie-Laure Mugnier. Walking the Decidability Line for Rules with Existential Variables
KR: Principles of Knowledge Representation and Reasoning, May 2010, Toronto, Canada. pp.466-476
lirmm-00410130v1  Conference papers
Jean-François BagetMichel LeclèreMarie-Laure MugnierEric Salvat. Extending Decidable Cases for Rules with Existential Variables
IJCAI: International Joint Conference on Artificial Intelligence, Jul 2009, Pasadena, CA, United States. pp.677-682
hal-01322328v1  Conference papers
Stephan MerzHernán Vanzetto. Encoding TLA+ into Many-Sorted First-Order Logic
Abstract State Machines, Alloy, B, TLA, VDM, and Z - 5th International Conference, ABZ 2016, 2016, Linz, Austria. pp.54-69, ⟨10.1007/978-3-319-33600-8_3⟩
hal-00919759v1  Conference papers
Guillaume BurelSimon Cruanes. Detection of First Order Axiomatic Theories
FroCoS - 9th International Symposium on Frontiers of Combining Systems - 2013, Sep 2013, Nancy, France. pp.229-244, ⟨10.1007/978-3-642-40885-4_16⟩
hal-01937141v1  Conference papers
Anders SchlichtkrullJasmin Christian BlanchetteDmitriy Traytel. A Verified Prover Based on Ordered Resolution
CPP 2019 - The 8th ACM SIGPLAN International Conference on Certified Programs and Proofs, Jan 2019, Cascais, Portugal. ⟨10.1145/3293880.3294100⟩
hal-02386942v1  Conference papers
Willem HeijltjesDominic HughesLutz Straßburger. Proof Nets for First-Order Additive Linear Logic
FSCD 2019 - 4th International Conference on Formal Structures for Computation and Deduction, Jun 2019, Dortmund, Germany. pp.22:1-22:22, ⟨10.4230/LIPIcs.FSCD.2019.22⟩