Skip to Main content Skip to Navigation

inria-00407778v1  Reports
Georges GonthierRoux Stéphane Le. An Ssreflect Tutorial
[Technical Report] RT-0367, INRIA. 2009, pp.33
pastel-00780446v1  Theses
Cyril Cohen. Formalized algebraic numbers: construction and first-order theory.
Logic in Computer Science [cs.LO]. Ecole Polytechnique X, 2012. English
hal-00763495v1  Conference papers
Frédéric BlanquiKim Quyen Ly. Automated verification of termination certificates
15th National Symposium of Selected ICT Problems, Dec 2012, Hanoi, Vietnam
hal-00776876v1  Conference papers
Thomas BraibantAdam Chlipala. Formal Verification of Hardware Synthesis
Computer Aided Verification - 25th International Conference, Jul 2013, Saint Petersburg, Russia. pp.213-228, ⟨10.1007/978-3-642-39799-8_14⟩
inria-00100144v1  Book sections
Yann ZimmermannStefan HallerstedeDominique Cansell. Formal modelling of electronic circuits using event-B, Case Study: SAE J1708 Serial Communication Link
Jean Mermet. UML-B - Specification for Proven Embedded Systems Design, Kluwer Academic Publishers, 2004
hal-01351005v1  Reports
Bernard Paul Serpette. Logical semantics of Esterel with unconstrained local signals
[Research Report] RR-8942, INRIA Sophia Antipolis - Méditerranée. 2016
hal-01226760v3  Reports
Bernard Paul Serpette. Using counters for absence prediction in Esterel
[Research Report] RR-8941, INRIA Sophia Antipolis - Méditerranée. 2016, pp.18
hal-00097561v1  Conference papers
Ninh Thuan TruongJeanine Souquières. Checking Consistency of UML state and sequence diagrams using B
Japan-Vietnam Workshop on Software Engineering 2006 (JVSE'06), 2006, Hanoi, Vietnam
inria-00099920v1  Conference papers
Jacques CalmetVincent Lefèvre. Toward the Integration of Numerical Computations into the OMSCS Framework
7th International Workshop on Computer Algebra in Scientific Computing - CASC'2004, 2004, Saint Petersburg, Russia, pp.71-79
inria-00539899v1  Conference papers
Henri DebratBernadette Charron-BostStephan Merz. Formal Verification of Consensus Algorithms in a Proof Assistant
2010 Grande Region Security and Reliability Day, Mar 2010, Saarbrücken, Germany
pastel-00605836v1  Theses
Arnaud Spiwack. Verified Computing in Homological Algebra
Algebraic Topology [math.AT]. Ecole Polytechnique X, 2011. English
hal-02102015v1  Reports
Sylvie BoldoMarc Daumas. A simple test qualifying the accuracy of Horner's rule for polynomials
[Research Report] LIP RR-2003-01, Laboratoire de l'informatique du parallélisme. 2003, 2+39p
hal-02101979v1  Reports
Sylvie BoldoGuillaume Melquiond. When double rounding is odd
[Research Report] LIP RR-2004-48, Laboratoire de l'informatique du parallélisme. 2004, 2+7p
inria-00001035v1  Conference papers
Julien Narboux. A Decision Procedure for Geometry in Coq
Theorem Proving in Higher Order Logics 2004, Jul 2004, Park City, USA, United States. pp.225-240, ⟨10.1007/b100400⟩
hal-01110666v1  Conference papers
Guillaume Melquiond. Automations for verifying floating-point algorithms
5th Coq Workshop, Jul 2013, Rennes, France
tel-02194683v1  Habilitation à diriger des recherches
Guillaume Melquiond. Formal Verification for Numerical Computations, and the Other Way Around
Computer Arithmetic. Université Paris Sud, 2019
hal-00747305v1  Conference papers
Dominique MéryNeeraj Kumar Singh. Critical systems development methodology using formal techniques
3rd International Symposium on Information and Communication Technology - SoICT 2012, Aug 2012, Ha Long, Vietnam. pp.3-12, ⟨10.1145/2350716.2350720⟩
hal-01630411v1  Conference papers
Florian Faissole. Formalization and closedness of finite dimensional subspaces
SYNASC 2017 - 19th International Symposium on Symbolic and Numeric Algorithms for Scientific Computing, Sep 2017, Timișoara, Romania. pp.1-7
hal-01768758v1  Journal articles
Noran AzmyStephan MerzChristoph Weidenbach. A Machine-Checked Correctness Proof for Pastry
Science of Computer Programming, Elsevier, 2018, 158, pp.64-80. ⟨10.1016/j.scico.2017.08.003⟩
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⟩
tel-00336576v1  Habilitation à diriger des recherches
Sandrine Blazy. Sémantiques formelles
Informatique [cs]. Université d'Evry-Val d'Essonne, 2008