Selected publications by Jean Goubault-Larrecq
Books
- GM97
-
J. Goubault-Larrecq and I. Mackie. Proof Theory and Automated Deduction, Applied Logic Series 6. Kluwer Academic Publishers, 1997. ( BibTeX )
Chapters in Books
- Gou06a
-
J. Goubault-Larrecq. 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. ( 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
- BGGP12
-
O. Bouissou, É. Goubault, J. Goubault-Larrecq and S. Putot. A Generalization of P-boxes to Affine Arithmetic, and Applications to
Static Analysis of Programs. Computing, 2012. To appear. ( PDF | BibTeX + Abstract )
- FG12
-
A. Finkel and J. Goubault-Larrecq. Forward Analysis for WSTS, Part II: Complete WSTS. Logical Methods in Computer Science, 2012. To appear. ( BibTeX + Abstract )
- Gou12
-
J. Goubault-Larrecq. QRB-Domains and the Probabilistic Powerdomain. Logical Methods in Computer Science, 2012. To appear. ( BibTeX + Abstract )
- GK11
-
J. Goubault-Larrecq and K. Keimel. Choquet-Kendall-Matheron Theorems for Non-Hausdorff Spaces. Mathematical Structures in Computer Science 21(3), pages 511-561, 2011. ( PDF | BibTeX + Abstract )
- Gou11a
-
J. Goubault-Larrecq. Musings Around the Geometry of Interaction, and Coherence. Theoretical Computer Science 412(20), pages 1998-2014, 2011. ( PDF | BibTeX + Abstract )
- Gou10a
-
J. Goubault-Larrecq. Finite Models for Formal Security Proofs. Journal of Computer Security 18(6), pages 1247-1299, 2010. ( PDF | BibTeX + Abstract )
- Gou10b
-
J. Goubault-Larrecq. De Groot Duality and Models of Choice: Angels, Demons, and Nature. Mathematical Structures in Computer Science 20(2), pages 169-237, 2010. ( PDF | BibTeX + Abstract )
- GLN08
-
J. Goubault-Larrecq, S. Lasota and D. Nowak. Logical Relations for Monadic Types. Mathematical Structures in Computer Science 18(6), pages 1169-1217, 2008. 81 pages. ( PDF | BibTeX + Abstract )
- VG07
-
K. N. Verma and J. Goubault-Larrecq. Alternating Two-Way AC-Tree Automata. Information and Computation 205(6), pages 817-869, 2007. ( PDF | PS | PS.GZ | BibTeX + Abstract )
- VG05
-
K. N. Verma and J. Goubault-Larrecq. 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
-
J. Goubault-Larrecq. Deciding H1 by Resolution. Information Processing Letters 95(3), pages 401-408, 2005. ( PDF | BibTeX + Abstract )
- GRV05
-
J. Goubault-Larrecq, M. Roger and K. N. Verma. 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
-
J. Goubault-Larrecq. Extensions of Valuations. Mathematical Structures in Computer Science 15(2), pages 271-297, 2005. ( PS | PS.GZ | BibTeX )
- GG03
-
J. Goubault-Larrecq and É. Goubault. On the Geometry of Intuitionistic S4 Proofs. Homology, Homotopy and Applications 5(2), pages 137-209, 2003. ( PS | PS.GZ | BibTeX )
- Gou02c
-
J. Goubault-Larrecq. Sécurité, modélisation et analyse de protocoles
cryptographiques. Phœbus, la revue de la sûreté de fonctionnement 20, 2002. ( DOC | BibTeX )
- GG00
-
H. Goguen and J. Goubault-Larrecq. 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
- GV11
-
J. Goubault-Larrecq and D. Varacca. Continuous Random Variables. In LICS'11, pages 97-106. IEEE Computer Society Press, 2011. ( PDF | BibTeX + Abstract )
- Gou10c
-
J. Goubault-Larrecq. Noetherian Spaces in Verification. In ICALP'10, LNCS 6199, pages 2-21. Springer, 2010. ( PDF | BibTeX + Abstract )
- Gou10d
-
J. Goubault-Larrecq. ωQRB-Domains and the
Probabilistic Powerdomain. In LICS'10, pages 352-361. IEEE Computer Society Press, 2010. ( PDF | BibTeX + Abstract )
- Gou09a
-
J. Goubault-Larrecq. "Logic Wins!". In ASIAN'09, LNCS 5913, pages 1-16. Springer, 2009. ( PDF | BibTeX + Abstract )
- FG09a
-
A. Finkel and J. Goubault-Larrecq. Forward Analysis for WSTS, Part II: Complete WSTS. In ICALP'09, LNCS 5556, pages 188-199. Springer, 2009. ( PDF | BibTeX + Abstract )
- FG09b
-
A. Finkel and J. Goubault-Larrecq. 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
-
J. Goubault-Larrecq. Towards Producing Formally Checkable Security Proofs, Automatically. In CSF'08, pages 224-238. IEEE Computer Society Press, 2008. ( PDF | BibTeX + Abstract )
- Gou08b
-
J. Goubault-Larrecq. Simulation Hemi-Metrics Between Infinite-State Stochastic Games. In FoSSaCS'08, LNCS 4962, pages 50-65. Springer, 2008. ( PDF (long version) | BibTeX + Abstract )
- Gou08c
-
J. Goubault-Larrecq. Prevision Domains and Convex Powercones. In FoSSaCS'08, LNCS 4962, pages 318-333. Springer, 2008. ( PDF (long version) | BibTeX + Abstract )
- GO08
-
J. Goubault-Larrecq and J. Olivain. A Smell of Orchids. In RV'08, LNCS 5289, pages 1-20. Springer, 2008. ( PDF | BibTeX + Abstract )
- BG07
-
E. Bursztein and J. Goubault-Larrecq. 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
-
J. Goubault-Larrecq, C. Palamidessi and A. Troina. A Probabilistic Applied Pi-Calculus. In APLAS'07, LNCS 4807, pages 175-290. Springer, 2007. ( PDF | BibTeX + Abstract )
- Gou07a
-
J. Goubault-Larrecq. Continuous Previsions. In CSL'07, LNCS 4646, pages 542-557. Springer, 2007. ( PDF | PDF (long version) | BibTeX + Abstract )
- Gou07b
-
J. Goubault-Larrecq. Continuous Capacities on Continuous State Spaces. In ICALP'07, LNCS 4596, pages 764-776. Springer, 2007. ( PDF | BibTeX + Abstract )
- Gou07c
-
J. Goubault-Larrecq. On Noetherian Spaces. In LICS'07, pages 453-462. IEEE Computer Society Press, 2007. ( PDF | PDF (long version) | BibTeX + Abstract )
- OG05
-
J. Olivain and J. Goubault-Larrecq. The Orchids Intrusion Detection Tool. In CAV'05, LNCS 3576, pages 286-290. Springer, 2005. ( PDF | BibTeX )
- GP05
-
J. Goubault-Larrecq and F. Parrennes. Cryptographic Protocol Analysis on Real C Code. In VMCAI'05, LNCS 3385, pages 363-379. Springer, 2005. ( PDF | PDF (long version) | BibTeX + Abstract )
- GLNZ04
-
J. Goubault-Larrecq, S. Lasota, D. Nowak and Y. Zhang. Complete Lax Logical Relations for Cryptographic Lambda-Calculi. In CSL'04, LNCS 3210, pages 400-414. Springer, 2004. ( PS | PS.GZ | BibTeX )
- Gou02d
-
J. Goubault-Larrecq. Higher-Order Positive Set Constraints. In CSL'02, LNCS 2471, pages 473-489. Springer, 2002. ( PS | PS.GZ | BibTeX )
- GLN02
-
J. Goubault-Larrecq, S. Lasota and D. Nowak. Logical Relations for Monadic Types. In CSL'02, LNCS 2471, pages 553-568. Springer, 2002. ( PS | PS.GZ | BibTeX )
- Gou01a
-
J. Goubault-Larrecq. Well-Founded Recursive Relations. In CSL'01, LNCS 2142, pages 484-497. Springer, 2001. ( PS | PS.GZ | BibTeX )
- RG01a
-
X. Rival and J. Goubault-Larrecq. Experiments with Finite Tree Automata in Coq. In TPHOLs'01, LNCS 2152, pages 362-377. Springer, 2001. ( PS | PS.GZ | BibTeX )
- RG01b
-
M. Roger and J. Goubault-Larrecq. Log Auditing through Model Checking. In CSFW'01, pages 220-236. IEEE Computer Society Press, 2001. ( PS | PS.GZ | BibTeX )
- VGPA00
-
K. N. Verma, J. Goubault-Larrecq, S. Prasad and S. Arun-Kumar. Reflecting BDDs in Coq. In ASIAN 2000, LNCS 1961, pages 162-181. Springer, 2000. ( PS | PS.GZ | BibTeX )
- Gou00
-
J. Goubault-Larrecq. 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
-
J. Goubault-Larrecq. Conjunctive Types and SKInT. In TYPES'98, LNCS 1657, pages 106-120. Springer, 1999. ( PS | PS.GZ | BibTeX )
- Gou99b
-
J. Goubault-Larrecq. A Simple Sequent System for First-Order Logic with Free Constructors. In TABLEAUX'99, LNAI 1617, pages 202-216. Springer, 1999. ( BibTeX )
- Gou98a
-
J. Goubault-Larrecq. A Proof of Weak Termination of Typed λ-σ-Calculi. In TYPES'96, LNCS 1512, pages 134-151. Springer, 1998. ( PS | PS.GZ | BibTeX )
- Gou97a
-
J. Goubault-Larrecq. Ramified Higher-Order Unification. In LICS'97, pages 410-421. IEEE Computer Society Press, 1997. ( PS | PS.GZ | BibTeX )
- SG97
-
P. H. Schmitt and J. Goubault-Larrecq. A Tableau System for Linear-TIME Temporal Logic. In TACAS'97, LNCS 1217, pages 130-144. Springer, 1997. ( PS | PS.GZ | BibTeX )
Theses
- Gou97b
-
J. Goubault-Larrecq. 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
- OGB+11
-
J. Olivain, J. Goubault-Larrecq, H. Benzina, B. Gourdin and R. Ben Younès. ORCHIDS, 2011. ( Web page | BibTeX + Abstract )
- Gou11b
-
J. Goubault-Larrecq. A Few Pearls in the Theory of Quasi-Metric Spaces, Invited talk, Fifth International Conference on Topology, Algebra,
and Categories in Logic (TACL'11), Marseilles, France, July 2011, 2011. ( BibTeX )
- BG10
-
H. Benzina and J. Goubault-Larrecq. Some Ideas on Virtualized Systems Security, and Monitors. In DPM/SETOP'10, LNCS 6514, pages 244-258. Springer, 2010. ( PDF | BibTeX + Abstract )
- BGGP10
-
O. Bouissou, É. Goubault, J. Goubault-Larrecq and S. Putot. A Generalization of P-boxes to Affine Arithmetic, and Applications to
Static Analysis of Programs. In SCAN'10. 2010. ( BibTeX )
- Gou09b
-
J. Goubault-Larrecq. 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
-
J. Goubault-Larrecq. HimML: HimML is a
map-oriented ML, 2008. ( Web page | BibTeX )
- Gou08e
-
J. Goubault-Larrecq. 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 )
- Gou08f
-
J. Goubault-Larrecq. The h1 Tool Suite, 2008. ( Web page | BibTeX )
- Gou07d
-
J. Goubault-Larrecq. 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
-
J. Goubault-Larrecq. 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
-
J. Olivain and J. Goubault-Larrecq. 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
-
J. Goubault-Larrecq. 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 )
- GP04
-
J. Goubault-Larrecq and F. Parrennes. Csur: Static Analysis of C Code, 2004. ( Web page | BibTeX )
- Gou04a
-
J. Goubault-Larrecq. 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
-
J. Goubault-Larrecq. 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
-
J. Goubault-Larrecq. 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
-
J. Goubault-Larrecq. 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 [Gou08]) (3454 lines). ( Web page | BibTeX )
- Gou02f
-
J. Goubault-Larrecq. 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 )
- Gou02g
-
J. Goubault-Larrecq. Vérification de protocoles cryptographiques: la logique à la
rescousse! In SECI'02, pages 119-152. INRIA, 2002. Invited paper. ( PS | PS.GZ | BibTeX )
- GV02
-
J. Goubault-Larrecq and K. N. Verma. 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 )
- Gou02h
-
J. Goubault-Larrecq. SKInT Labels. Research Report LSV-02-7, Laboratoire Spécification et Vérification, ENS Cachan,
France, July 2002. 15 pages. ( PS | PS.GZ | BibTeX )
- Gou02i
-
J. Goubault-Larrecq. 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
-
J. Goubault-Larrecq. 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
-
J. Goubault-Larrecq and É. Goubault. Order-Theoretic, Geometric and Combinatorial Models of Intuitionistic
S4 Proofs. In IMLA'99. 1999. ( PS | PS.GZ | BibTeX )
- Gou99c
-
J. Goubault-Larrecq. 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
-
J. Goubault-Larrecq. A Few Remarks on SKInT. Research Report RR-3475, INRIA Rocquencourt, France, August 1998. ( PS | PS.GZ | BibTeX )
- Gou97c
-
J. Goubault-Larrecq. 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 )