Books | |
| [GM97] | . Proof Theory and Automated Deduction, Applied Logic Series 6. Kluwer Academic Publishers, 1997. ( BibTeX ) |
Chapters in Books | |
| [Gou06a] | . Preuve et vérification pour la sécurité et la sûreté. In Encyclopédie de l'informatique et des systèmes d'information, chapter I.6, pages 683-703. Vuibert, 2006. ( Web page | BibTeX + Abstract ) |
Edited Books | |
| [Gou03] | J. Goubault-Larrecq (ed.). Proceedings of the 1st Workshop on Logical Aspects of Cryptographic Protocol Verification (LACPV 2001), Paris, France, July 2001, ENTCS 55(1). Elsevier Science Publishers, 2003. ( Web page | BibTeX ) |
| [Gou02a] | J. Goubault-Larrecq (ed.). Special Issue on Models and Methods for Cryptographic Protocol Verification. Journal of Telecommunications and Information Technology 4/2002, 2002. ( Web page | BibTeX ) |
| [Gou02b] | J. Goubault-Larrecq (ed.). Actes du 1er Workshop International sur la Sécurité des Communications sur Internet (SECI'02), Tunis, Tunisia, September 2002. INRIA. ( Web page | BibTeX ) |
Journals | |
| [Gou10a] | . De Groot Duality and Models of Choice: Angels, Demons, and Nature. Mathematical Structures in Computer Science, 2010. To appear. ( PDF | BibTeX + Abstract ) |
| [Gou10b] | . Musings Around the Geometry of Interaction, and Coherence. Theoretical Computer Science, 2010. To appear. ( PDF | BibTeX + Abstract ) |
| [Gou09a] | . Finite Models for Formal Security Proofs. Journal of Computer Security, 2009. To appear. ( BibTeX ) |
| [GLN08] | . Logical Relations for Monadic Types. Mathematical Structures in Computer Science 18(6), pages 1169-1217, 2008. 81 pages. ( PDF | BibTeX + Abstract ) |
| [VG07] | . Alternating Two-Way AC-Tree Automata. Information and Computation 205(6), pages 817-869, 2007. ( PDF | PS | PS.GZ | BibTeX + Abstract ) |
| [VG05] | . Karp-Miller Trees for a Branching Extension of VASS. Discrete Mathematics & Theoretical Computer Science 7(1), pages 217-230, 2005. ( PDF | PS | PS.GZ | BibTeX + Abstract ) |
| [Gou05a] | . Deciding H1 by Resolution. Information Processing Letters 95(3), pages 401-408, 2005. ( PDF | BibTeX + Abstract ) |
| [GRV05] | . Abstraction and Resolution Modulo AC: How to Verify Diffie-Hellman-like Protocols Automatically. Journal of Logic and Algebraic Programming 64(2), pages 219-251, 2005. ( PS | PS.GZ | BibTeX ) |
| [Gou05b] | . Extensions of Valuations. Mathematical Structures in Computer Science 15(2), pages 271-297, 2005. ( PS | PS.GZ | BibTeX ) |
| [GG03] | . On the Geometry of Intuitionistic S4 Proofs. Homology, Homotopy and Applications 5(2), pages 137-209, 2003. ( PS | PS.GZ | BibTeX ) |
| [Gou02c] | . Sécurité, modélisation et analyse de protocoles cryptographiques. Phœbus, la revue de la sûreté de fonctionnement 20, 2002. ( DOC | BibTeX ) |
| [GG00] | . Sequent Combinators: A Hilbert System for the Lambda Calculus. Mathematical Structures in Computer Science 10(1), pages 1-79, 2000. ( PS | PS.GZ | BibTeX ) |
Conferences | |
| [Gou09b] | . "Logic Wins!". In ASIAN'09, LNCS 5913, pages 1-16. Springer, 2009. ( PDF | BibTeX + Abstract ) |
| [FG09a] | . Forward Analysis for WSTS, Part II: Complete WSTS. In ICALP'09, LNCS 5556, pages 188-199. Springer, 2009. ( PDF | BibTeX + Abstract ) |
| [FG09b] | . Forward Analysis for WSTS, Part I: Completions. In STACS'09, Leibniz International Proceedings in Informatics 3, pages 433-444. Leibniz-Zentrum für Informatik, 2009. ( PDF | BibTeX + Abstract ) |
| [Gou08a] | . Towards Producing Formally Checkable Security Proofs, Automatically. In CSF'08, pages 224-238. IEEE Computer Society Press, 2008. ( PDF | BibTeX + Abstract ) |
| [Gou08b] | . Simulation Hemi-Metrics Between Infinite-State Stochastic Games. In FoSSaCS'08, LNCS 4962, pages 50-65. Springer, 2008. ( PDF (long version) | BibTeX + Abstract ) |
| [Gou08c] | . Prevision Domains and Convex Powercones. In FoSSaCS'08, LNCS 4962, pages 318-333. Springer, 2008. ( PDF (long version) | BibTeX + Abstract ) |
| [GO08] | . A Smell of Orchids. In RV'08, LNCS 5289, pages 1-20. Springer, 2008. ( PDF | BibTeX + Abstract ) |
| [BG07] | . A Logical Framework for Evaluating Network Resilience Against Faults and Attacks. In ASIAN'07, LNCS 4846, pages 212-227. Springer, 2007. ( PDF | BibTeX + Abstract ) |
| [GPT07] | . A Probabilistic Applied Pi-Calculus. In APLAS'07, LNCS 4807, pages 175-290. Springer, 2007. ( PDF | BibTeX + Abstract ) |
| [Gou07a] | . Continuous Previsions. In CSL'07, LNCS 4646, pages 542-557. Springer, 2007. ( PDF | PDF (long version) | BibTeX + Abstract ) |
| [Gou07b] | . Continuous Capacities on Continuous State Spaces. In ICALP'07, LNCS 4596, pages 764-776. Springer, 2007. ( PDF | BibTeX + Abstract ) |
| [Gou07c] | . On Noetherian Spaces. In LICS'07, pages 453-462. IEEE Computer Society Press, 2007. ( PDF | PDF (long version) | BibTeX + Abstract ) |
| [OG05] | . The Orchids Intrusion Detection Tool. In CAV'05, LNCS 3576, pages 286-290. Springer, 2005. ( PDF | BibTeX ) |
| [GP05] | . Cryptographic Protocol Analysis on Real C Code. In VMCAI'05, LNCS 3385, pages 363-379. Springer, 2005. ( PDF | PDF (long version) | BibTeX + Abstract ) |
| [GLNZ04] | . Complete Lax Logical Relations for Cryptographic Lambda-Calculi. In CSL'04, LNCS 3210, pages 400-414. Springer, 2004. ( PS | PS.GZ | BibTeX ) |
| [Gou02d] | . Higher-Order Positive Set Constraints. In CSL'02, LNCS 2471, pages 473-489. Springer, 2002. ( PS | PS.GZ | BibTeX ) |
| [GLN02] | . Logical Relations for Monadic Types. In CSL'02, LNCS 2471, pages 553-568. Springer, 2002. ( PS | PS.GZ | BibTeX ) |
| [Gou01a] | . Well-Founded Recursive Relations. In CSL'01, LNCS 2142, pages 484-497. Springer, 2001. ( PS | PS.GZ | BibTeX ) |
| [RG01a] | . Experiments with Finite Tree Automata in Coq. In TPHOLs'01, LNCS 2152, pages 362-377. Springer, 2001. ( PS | PS.GZ | BibTeX ) |
| [RG01b] | . Log Auditing through Model Checking. In CSFW'01, pages 220-236. IEEE Computer Society Press, 2001. ( PS | PS.GZ | BibTeX ) |
| [VGPA00] | . Reflecting BDDs in Coq. In ASIAN 2000, LNCS 1961, pages 162-181. Springer, 2000. ( PS | PS.GZ | BibTeX ) |
| [Gou00] | . A Method for Automatic Cryptographic Protocol Verification (Extended Abstract). In Proceedings of the Workshops of the 15th International Parallel and Distributed Processing Symposium, Cancun, Mexico, May 2000, LNCS 1800, pages 977-984. Springer, 2000. ( PS | PS.GZ | BibTeX ) |
| [Gou99a] | . Conjunctive Types and SKInT. In TYPES'98, LNCS 1657, pages 106-120. Springer, 1999. ( PS | PS.GZ | BibTeX ) |
| [Gou99b] | . A Simple Sequent System for First-Order Logic with Free Constructors. In TABLEAUX'99, LNAI 1617, pages 202-216. Springer, 1999. ( BibTeX ) |
| [Gou98a] | . A Proof of Weak Termination of Typed λ-σ-Calculi. In TYPES'96, LNCS 1512, pages 134-151. Springer, 1998. ( PS | PS.GZ | BibTeX ) |
| [Gou97a] | . Ramified Higher-Order Unification. In LICS'97, pages 410-421. IEEE Computer Society Press, 1997. ( PS | PS.GZ | BibTeX ) |
| [SG97] | . A Tableau System for Linear-TIME Temporal Logic. In TACAS'97, LNCS 1217, pages 130-144. Springer, 1997. ( PS | PS.GZ | BibTeX ) |
Theses | |
| [Gou97b] | . Logique, complexité, démonstration automatique et thèmes connexes. Mémoire d'habilitation, Université Paris 9 (Dauphine), Paris, France, September 1997. ( PS | PS.GZ | BibTeX ) |
Other Publications | |
| [Gou09c] | . On a Generalization of a Result by Valk and Jantzen. Research Report LSV-09-09, Laboratoire Spécification et Vérification, ENS Cachan, France, May 2009. 18 pages. ( PDF | BibTeX + Abstract ) |
| [Gou08d] | . A Cone-Theoretic Krein-Milman Theorem. Research Report LSV-08-18, Laboratoire Spécification et Vérification, ENS Cachan, France, June 2008. 8 pages. ( PDF | BibTeX + Abstract ) |
| [Gou07d] | . Believe It Or Not, GOI is a Model of Classical Linear Logic. Research Report LSV-07-03, Laboratoire Spécification et Vérification, ENS Cachan, France, January 2007. 18 pages. ( PDF | BibTeX + Abstract ) |
| [Gou06b] | . The ORCHIDS Intrusion Prevention System, Invited talk, Annual Adaptive and Resilient Computing Systems Workshop (AARCS'06), Santa Fe, New Mexico, USA, 2006. ( Web page | BibTeX ) |
| [OG06] | . Detecting Subverted Cryptographic Protocols by Entropy Checking. Research Report LSV-06-13, Laboratoire Spécification et Vérification, ENS Cachan, France, June 2006. 19 pages. ( PDF | BibTeX + Abstract ) |
| [Gou05c] | . A Biased Survey of Models and Methods for Verifying Cryptographic Protocols, Invited talk, Workshop on Classical and Quantum Information Security, Pasadena, California, USA, 2005. ( Web page | Slides | BibTeX ) |
| [Gou04a] | . On Computational Interpretations of the Modal Logic S4, Invited talk, 2nd Workshop on the Logic for Pragmatics (WoLP'04), Créteil, France, 2004. ( BibTeX ) |
| [Gou04b] | . On Cryptographic Protocols, Regular Tree Languages, and Automated Deduction, Invited talk, Workshop on Security of Systems: Formalism and Tools (SASYFT'04), Orleans, France, 2004. ( Web page | Slides | BibTeX ) |
| [Gou04c] | . Une fois qu'on n'a pas trouvé de preuve, comment le faire comprendre à un assistant de preuve ? In JFLA'04, pages 1-40. INRIA, 2004. Invited paper. ( PS | PS.GZ | BibTeX ) |
| [Gou02e] | . The EVA Parser and Translator, Available at http://www.lsv.ens-cachan.fr/˜goubault/EVA.html, 2002. Started 2001. Written in C (1327 lines), OCaml (361 lines), HimML (see [Gou02]) (3454 lines). ( Web page | BibTeX ) |
| [Gou02f] | . HimML: HimML is a map-oriented ML, An extension of core Standard ML, available at http://www.lsv.ens-cachan.fr/˜goubault/himml-dwnld.html, 2002. Version 1.0 alpha 17. Written in C (108948 lines), Emacs-Lisp (1850 lines). Documentation: 91 pages. ( Web page | BibTeX ) |
| [Gou02g] | . Csur: Static Analysis of C Code, Available at http://www.lsv.ens-cachan.fr/csur/, 2002. Written in OCaml (12648 lines). ( Web page | BibTeX ) |
| [Gou02h] | . Un algorithme pour l'analyse de logs. Research Report LSV-02-18, Laboratoire Spécification et Vérification, ENS Cachan, France, November 2002. 33 pages. ( PS | PS.GZ | BibTeX ) |
| [Gou02i] | . Vérification de protocoles cryptographiques: la logique à la rescousse! In SECI'02, pages 119-152. INRIA, 2002. Invited paper. ( PS | PS.GZ | BibTeX ) |
| [GV02] | . Alternating Two-Way AC-Tree Automata. Research Report LSV-02-11, Laboratoire Spécification et Vérification, ENS Cachan, France, September 2002. 21 pages. ( PS | PS.GZ | BibTeX ) |
| [Gou02j] | . SKInT Labels. Research Report LSV-02-7, Laboratoire Spécification et Vérification, ENS Cachan, France, July 2002. 15 pages. ( PS | PS.GZ | BibTeX ) |
| [Gou02k] | . A Note on the Completeness of Certain Refinements of Resolution. Research Report LSV-02-8, Laboratoire Spécification et Vérification, ENS Cachan, France, July 2002. 16 pages. ( PS | PS.GZ | BibTeX ) |
| [Gou01b] | . Higher-Order Automata, Pushdown Systems, and Set Constraints. Research Report LSV-01-9, Laboratoire Spécification et Vérification, ENS Cachan, France, November 2001. 15 pages. ( PS | PS.GZ | BibTeX ) |
| [GG99] | . Order-Theoretic, Geometric and Combinatorial Models of Intuitionistic S4 Proofs. In IMLA'99. 1999. ( PS | PS.GZ | BibTeX ) |
| [Gou99c] | . A Simple Deduction System for First-Order Logic with Equality, Free Constructors and Induction. Research Report RR-3653, INRIA Rocquencourt, France, March 1999. ( PS | PS.GZ | BibTeX ) |
| [Gou98b] | . A Few Remarks on SKInT. Research Report RR-3475, INRIA Rocquencourt, France, August 1998. ( PS | PS.GZ | BibTeX ) |
| [Gou97c] | . On Computational Interpretations of the Modal Logic S4 - IIIb. Confluence, Termination of the λevQH-Calculus. Research Report RR-3164, INRIA Rocquencourt, France, May 1997. ( PS | PS.GZ | BibTeX ) |