Travelled to:1 × Australia
1 × Austria
1 × Finland
1 × France
2 × United Kingdom
Collaborated with:∅ S.Conchon M.Iguernelala R.Rieu-Helft D.Ishii S.Nakajima F.d.Dinechin C.Q.Lauter C.Roux K.Ji C.Fumex F.Bobot E.Contejean A.Mahboubi A.Mebsout
Talks about:verif (3) point (3) float (3) algorithm (2) function (2) smt (2) postcondit (1) elementari (1) treatment (1) strongest (1)
Person: Guillaume Melquiond
DBLP: Melquiond:Guillaume
Contributed to:
2014
2013
201220122008
2006
20172018Wrote 8 papers:
- SMT-2014-Melquiond #algorithm #automation #float #verification
- Automating the Verification of Floating-Point Algorithms (GM), p. 63.
- IFM-2013-IshiiMN #automaton #calculus #hybrid #induction #verification
- Inductive Verification of Hybrid Automata with Strongest Postcondition Calculus (DI, GM, SN), pp. 139–153.
- IJCAR-2012-BobotCCIMMM #integer #linear
- A Simplex-Based Extension of Fourier-Motzkin for Solving Linear Integer Arithmetic (FB, SC, EC, MI, AM, AM, GM), pp. 67–81.
- SMT-2012-ConchonMRI #axiom #float #smt
- Built-in Treatment of an Axiomatic Floating-Point Theory for SMT Solvers (SC, GM, CR, MI), pp. 12–21.
- IJCAR-2008-Melquiond #bound #proving
- Proving Bounds on Real-Valued Functions with Computations (GM), pp. 2–17.
- SAC-2006-DinechinLM #using #verification
- Assisted verification of elementary functions using Gappa (FdD, CQL, GM), pp. 1318–1322.
- CAV-2017-ConchonIJMF #float #reasoning #smt
- A Three-Tier Strategy for Reasoning About Floating-Point Numbers in SMT (SC, MI, KJ, GM, CF), pp. 419–435.
- IJCAR-2018-MelquiondR #algorithm #framework #proving #why
- A Why3 Framework for Reflection Proofs and Its Application to GMP's Algorithms (GM, RRH), pp. 178–193.