Skip to Main content Skip to Navigation

tel-01591108v1  Theses
Haniel Barbosa. New techniques for instantiation and proof production in SMT solving
Artificial Intelligence [cs.AI]. Université de Lorraine, 2017. English. ⟨NNT : 2017LORR0091⟩
inria-00100068v1  Conference papers
Gérard MorelDominique MéryJean-Baptiste LégerThierry Lecomte. Proof-Oriented Fault-Tolerant Systems Engineering : Rationales, Experiments and Open Issues
7th IFAC Symposium on Cost Oriented Automation - COA'2004, 2004, Gatineau, Québec, Canada
hal-02422273v1  Conference papers
Thomas LetanYann Régis-Gianas. FreeSpec: Specifying, Verifying and Executing Impure Computations in Coq
CPP 2020 - 9th ACM SIGPLAN International Conference on Certified Programs and Proofs, Jan 2020, Nouvelle-Orléans, United States. pp.1-15, ⟨10.1145/3372885.3373812⟩
hal-01671994v1  Conference papers
Théo ZimmermannHugo Herbelin. Coq's Prolog and application to defining semi-automatic tactics
Type Theory Based Tools, Jan 2017, Paris, France
tel-02333396v2  Theses
Damien Rouhling. Formalisation tools for classical analysis : a case study in control theory
Logic in Computer Science [cs.LO]. Université Côte d'Azur, 2019. English. ⟨NNT : 2019AZUR4058⟩
hal-01672703v1  Conference papers
Niklas GrimmKenji MaillardCédric FournetCătălin HriţcuMatteo Maffei et al.  A Monadic Framework for Relational Verification
7th ACM SIGPLAN International Conference on Certified Programs and Proofs (CPP), Jan 2018, Los Angeles, United States. pp.130--145, ⟨10.1145/3167090⟩