Skip to Main content Skip to Navigation

hal-00685504v1  Conference papers
Omar ChebaroNikolai KosmatovNicky WilliamsBernard BotellaMuriel Roger. A lesson on structural testing with
6th International Conference on Tests & Proofs, May 2012, Prague, Czech Republic. pp.0-0
hal-01093719v1  Journal articles
Didier RémyBoris Yakobowski. A Church-Style Intermediate Language for MLF
Theoretical Computer Science, Elsevier, 2012, 435, pp.77--105. ⟨10.1016/j.tcs.2012.02.026⟩
hal-01935591v1  Conference papers
François BobotStéphane Graham-LengrandBruno MarreGuillaume Bury. Centralizing equality reasoning in MCSAT
16th International Workshop on Satisfiability Modulo Theories (SMT 2018), Jul 2018, Oxford, United Kingdom
hal-01673518v2  Theses
Frédéric Gilbert. Extending higher-order logic with predicate subtyping
Logic in Computer Science [cs.LO]. Université Sorbonne Paris Cité; Université Paris Diderot, 2018. English
hal-01645016v1  Conference papers
Roberto BlancoZakaria ChihaniDale Miller. Translating Between Implicit and Explicit Versions of Proof
CADE 26 - 26th International Conference on Automated Deduction, Aug 2017, Gothenburg, Sweden
hal-01549931v1  Conference papers
Silvia BonomiAntonella del PozzoMaria Potop-ButucaruSébastien Tixeuil. Optimal Storage under Unsynchronized Mobile Byzantine Faults
36th IEEE Symposium on Reliable Distributed Systems (SRDS 2017), Sep 2017, Hong Kong, China
hal-01673517v1  Conference papers
Frédéric Gilbert. Proof certificates in PVS
ITP 2017 - 8th International Conference on Interactive Theorem Proving, Sep 2017, Brasilia, Brazil. pp.262-268, ⟨10.1007/978-3-319-66107-0_17⟩
hal-01091947v1  Conference papers
Pascal CuoqJulien SignolesDamien Doligez. Lightweight Typed Customizable Unmarshaling
ACM SIGPLAN Workshop on ML, Sep 2011, Tokyo, Japan
hal-01245021v1  Conference papers
Frédéric Gilbert. A Lightweight Double-negation Translation
LPAR-20. 20th International Conference on Logic for Programming, Artificial Intelligence and Reasoning, Nov 2015, Suva, Fiji
hal-01503081v1  Conference papers
Richard BonichonPierre Weis. Format Unraveled
28ièmes Journées Francophones des Langages Applicatifs, Jan 2017, Gourette, France
hal-01658653v1  Conference papers
Gergö BaranyJulien Signoles. Hybrid Information Flow Analysis for Real-World C Code
TAP 2017 - 11th International Conference on Tests & Proofs, Jul 2017, Marburg, Germany. pp.23-40, ⟨10.1007/978-3-319-61467-0_2⟩
hal-00909293v1  Conference papers
Mounir AssafJulien SignolesFrédéric TronelEric Totel. Moniteur hybride de flux d'information pour un langage supportant des pointeurs
SARSSI - 8ème Conférence sur la Sécurité des Architectures Réseaux et des Systèmes d'Information, Sep 2013, Mont de Marsan, France
hal-01648681v1  Conference papers
Hugo IllousMatthieu LemerreXavier Rival. A Relational Shape Abstract Domain
NFM 2017 - 9th NASA Formal Methods Symposium, Apr 2017, Moffett Field, United States. pp.212-229, ⟨10.1007/978-3-319-57288-8_15⟩
cea-03218896v1  Journal articles
Hugo IllousMatthieu LemerreXavier Rival. A relational shape abstract domain
Formal Methods in System Design, Springer Verlag, 2020, ⟨10.1007/s10703-021-00366-4⟩
hal-00967132v1  Journal articles
François BobotJean-Christophe FilliâtreClaude MarchéAndrei Paskevich. Let's Verify This with Why3
International Journal on Software Tools for Technology Transfer, Springer Verlag, 2015, 17 (6), pp.709-727. ⟨10.1007/s10009-014-0314-5⟩
hal-01334604v1  Conference papers
Mounir AssafJulien SignolesEric TotelFrédéric Tronel. The Cardinal Abstraction for Quantitative Information Flow
Workshop on Foundations of Computer Security 2016 (FCS 2016), Jun 2016, Lisbon, Portugal
hal-00724508v1  Conference papers
Omar ChebaroMickaël DelahayeNikolai Kosmatov. Testing Inexecutable Conditions on Input Pointers in C Programs with SANTE
ICSSEA 2012 - 24th International Conference on Software & Systems Engineering and their Applications, Oct 2012, Paris, France. pp.1-7
hal-01228995v1  Conference papers
Richard GenestierAlain GiorgettiGuillaume Petiot. Sequential generation of structured arrays and its deductive verification
TAP 2015, 9th Int. Conf. of Tests and Proofs, 2015, L'Aquila, Italy. pp.109--128
hal-00563308v1  Conference papers
Omar ChebaroNikolai KosmatovAlain GiorgettiJacques Julliand. Combining Static Analysis and Test Generation for {C} Program Debugging
TAP'10, 4th Int. Conf. on Tests and Proofs, 2010, Spain. pp.94--100
hal-00875395v1  Conference papers
François BobotJean-Christophe FilliâtreClaude MarchéGuillaume MelquiondAndrei Paskevich. Preserving User Proofs Across Specification Changes
Fifth Working Conference on Verified Software: Theories, Tools and Experiments, May 2013, Atherton, United States. pp.191-201
hal-01344110v1  Conference papers
Nikolai KosmatovClaude MarchéYannick MoyJulien Signoles. Static versus Dynamic Verification in Why3, Frama-C and SPARK 2014
7th International Symposium on Leveraging Applications, Oct 2016, Corfu, Greece. pp.461--478
tel-00789543v1  Theses
Paolo Herms. Certification of a Tool Chain for Deductive Program Verification
Other [cs.OH]. Université Paris Sud - Paris XI, 2013. English. ⟨NNT : 2013PA112006⟩
hal-02317078v1  Conference papers
Allan BlanchardNikolai KosmatovFrédéric Loulergue. A Lesson on Verification of IoT Software with Frama-C
2018 International Conference on High Performance Computing & Simulation (HPCS), Jul 2018, Orleans, France. pp.21-30, ⟨10.1109/HPCS.2018.00018⟩
hal-02317143v1  Documents associated with scientific events
Allan BlanchardNikolai KosmatovFrédéric Loulergue. La logique contre les fantômes: comparaison de deux approches pour la preuve d'un module de listes chaînées *
18e journées Approches Formelles dans l'Assistance au Développement de Logic (AFADL), Jun 2019, Toulouse, France