Skip to Main content Skip to Navigation

hal-01989726v1  Journal articles
Jasmin Christian BlanchetteLorenzo GheriAndrei PopescuDmitriy Traytel. Bindings as Bounded Natural Functors
Proceedings of the ACM on Programming Languages, ACM, 2019, 3 (POPL), pp.1-34. ⟨10.1145/3290335⟩
hal-01643157v1  Journal articles
Jasmin Christian BlanchetteAndrei PopescuDmitriy Traytel. Soundness and Completeness Proofs by Coinductive Methods
Journal of Automated Reasoning, Springer Verlag, 2017, 58 (1), pp.149 - 179. ⟨10.1007/s10817-016-9391-3⟩
hal-02296014v1  Journal articles
Alexander BentkampJasmin BlanchetteDietrich Klakow. A Formal Proof of the Expressiveness of Deep Learning
Journal of Automated Reasoning, Springer Verlag, 2019, 63 (2), pp.347-368. ⟨10.1007/s10817-018-9481-5⟩
hal-02395177v1  Journal articles
Jasmin BlanchetteStephan Merz. Selected Extended Papers of ITP 2016: Preface
Journal of Automated Reasoning, Springer Verlag, 2019, 62 (2), pp.169-170. ⟨10.1007/s10817-018-9470-8⟩
hal-00760398v1  Conference papers
Arnaud FietzkeEvgeny KruglovChristoph Weidenbach. Automatic Generation of Invariants for Circular Derivations in SUP(LA)
18th International Conference on Logic for Programming, Artificial Intelligence and Reasoning, Mar 2012, Mérida, Venezuela. pp.197-211
hal-00760579v1  Conference papers
Stephan MerzHernán Vanzetto. Harnessing SMT Solvers for TLA+ Proofs
12th International Workshop on Automated Verification of Critical Systems (AVoCS 2012), Sep 2012, Bamberg, Germany
hal-00768812v1  Conference papers
Tianxiang LuStephan MerzChristoph Weidenbach. Formal Verification Of Pastry Using TLA+
International Workshop on the TLA+ Method and Tools, Aug 2012, Paris, France
hal-00760392v1  Conference papers
Jasmin BlanchetteAndrei PopescuDaniel WandChristoph Weidenbach. More SPASS with Isabelle -- Superposition with Hard Sorts and Configurable Simplification
Interactive Theorem Proving (ITP 2012), Aug 2012, Princeton, New Jersey, United States. pp.345-360
hal-00763092v1  Conference papers
Manamiary Bruno AndriamiarinaHayat DaoudMostefa BelarbiDominique MéryCamel Tanougast. Formal Verification of Fault Tolerant NoC-based Architecture
First International Workshop on Mathematics and Computer Science (IWMCS2012), Mostefa BELARBI - University of Tiaret - Algeria, Dec 2012, Tiaret, Algeria
hal-03141064v1  Conference papers
Patrick KoopmannWarren Del-PintoSophie TourretRenate Schmidt. Signature-Based Abduction for Expressive Description Logics
17th International Conference on Principles of Knowledge Representation and Reasoning , Sep 2020, Rhodes, France. pp.592-602, ⟨10.24963/kr.2020/59⟩
hal-00931919v1  Conference papers
Peter BaumgartnerUwe Waldmann. Hierarchic Superposition With Weak Abstraction
24th International Conference on Automated Deduction (CADE-24), Jun 2013, Lake Placid, NY, United States. pp.39-57, ⟨10.1007/978-3-642-38574-2_3⟩
inria-00540811v1  Conference papers
Tianxiang LuStephan MerzChristoph Weidenbach. Model Checking the Pastry Routing Protocol
10th International Workshop Automated Verification of Critical Systems, Sep 2010, Düsseldorf, Germany. pp.19-21
hal-01084232v1  Journal articles
Gerald LüttgenStephan Merz. Editorial: Special Issue of Automated Verification of Critical Systems
Science of Computer Programming, Elsevier, 2014, Special Issue: Automated Verification of Critical Systems, 96 (3), pp.277-278
tel-02963301v1  Theses
Mathias Fleury. Formalization of Logical Calculi in Isabelle/HOL
Logic in Computer Science [cs.LO]. Universität des Saarlandes Saarbrücken, 2020. English
hal-01933975v1  Directions of work or proceedings
El Hassan AbdelwahedLadjel BellatrecheDjamal BenslimaneMatteo GolfarelliStéphane Jean et al.  New Trends in Model and Data Engineering
MEDI 2018 - International Workshops, DETECT, MEDI4SG, IWCFS, REMEDY, Oct 2018, Marrakesh, Morocco. Communications in Computer and Information Science, Communications in Computer and Information Science (929), Springer, 2018, 978-3-030-02851-0. ⟨10.1007/978-3-030-02852-7⟩
hal-01590918v1  Conference papers
Haniel BarbosaPascal FontaineAndrew Reynolds. Congruence Closure with Free Variables
Tools and Algorithms for Construction and Analysis of Systems (TACAS), 2017, Uppsala, Sweden. pp.220 - 230, ⟨10.1007/10721959_17⟩
hal-01590922v1  Conference papers
Haniel BarbosaJasmin BlanchettePascal Fontaine. Scalable Fine-Grained Proofs for Formula Processing
Proc. Conference on Automated Deduction (CADE), 2017, Gotenburg, Sweden. pp.398 - 412, ⟨10.1007/978-3-642-02959-2_10⟩
hal-01199160v1  Journal articles
Gaurav SharmaFrédéric JurieCordelia Schmid. Expanded Parts Model for Semantic Description of Humans in Still Images
IEEE Transactions on Pattern Analysis and Machine Intelligence, Institute of Electrical and Electronics Engineers, 2017, 39 (1), pp.87-101. ⟨10.1109/TPAMI.2016.2537325⟩
hal-01180164v1  Conference papers
Olivier DevillersStefan MeiserMonique Teillaud. Fully dynamic Delaunay triangulation in logarithmic expected time per operation
Workshop Algorithms and Data Structures, 1991, Ottawa, Canada. pp.42-53
hal-01180157v1  Conference papers
Olivier DevillersStefan MeiserMonique Teillaud. The space of spheres, a geometric tool to unify duality results on Voronoi diagrams
Canadian Conference on Computational Geometry, 1992, St. John's, Canada. pp.263-268
hal-02997277v1  Conference papers
Horatiu CirsteaAlexis GrallDominique Méry. Generating Distributed Programs from Event-B Models
International Workshop on Verification and Program Transformation, Apr 2020, Dublin, Ireland. pp.110-124, ⟨10.4204/EPTCS.320.8⟩
hal-00643987v1  Conference papers
Sanjoy BaruahVincenzo BonifaciGianlorenzo d'AngeloAlberto Marchetti-SpaccamelaSuzanne Ster et al.  Mixed-Criticality Scheduling of Sporadic Task Systems
19th Annual European Symposium on Algorithms (ESA 2011), Sep 2011, Saarbruecken, Germany. pp.555-566, ⟨10.1007/978-3-642-23719-5_47⟩
hal-00795285v1  Conference papers
Nikolaos FountoulakisBruce Reed. A general critical condition for the emergence of a giant component in random graphs with given degrees
European Conference on Combinatorics, Graph Theory and Applications (Eurocomb 2009), 2009, Bordeaux, France. pp.639―645