The Coq mailing list

[Nguyen Quang-Huy <quang-huy.nguyen AT trusted-labs.com>]

Hi all,

We from Trusted Labs are using Coq for certifying critical SW and HW 
components.
Most of EAL7 certification projects done in Trusted Labs (and also Gemalto) 
have been done in Coq (although we are not bounded to this tool).
In addition to the references provided by Pierre, I gave recently some talks 
about our use of Coq in an industrial project:
http://pat.sce.ntu.edu.sg/esss14/keynote.html or
"Formal Verification for Certifying Security IC in EAL7 Level", keynote at 
the 8th ECSI Forum on specification & Design Languages, September 2013

The team still looking for skillful guy that is interested in applying formal 
tools like Coq to security industry.
However, we don't have plan to work on an open-source project now.

BR,
Huy

-----Original Message-----
From: Pierre NERON 
[mailto:pierre.neron AT gmail.com]
 On Behalf Of Pierre Neron
Sent: vendredi 23 mai 2014 18:46
To: 
coq-club AT inria.fr
Subject: Re: [Coq-Club] professional advice for a young Coq developer

Hi everyone

I did an internship few years ago at Gemalto. They use coq for formal 
verification, particularly around the JavaCard platform, and they even 
publish a few things.
You can have a look at the publications of:
Quang-Huy Nguyen : 
http://www.informatik.uni-trier.de/~ley/pers/hd/n/Nguyen_0002:Quang_Huy.html
Boutheina Chetali : 
http://www.informatik.uni-trier.de/~ley/pers/hd/c/Chetali:Boutheina.html

We also published a paper on a formal model of a smart card web server in Coq 
(http://www.lix.polytechnique.fr/~neron/Publi/SCWS/scws_cardis.pdf).

I think people at Prove&Run also use Coq.

Another application is the use of Coq to verify the B tool used by Siemens, 
see Melanie Jacquel work 
(http://www.informatik.uni-trier.de/~ley/pers/hd/j/Jacquel:M=eacute=lanie.html).

Pierre.

On 23 mai 2014, at 17:16, Jonathan 
<jonikelee AT gmail.com>
 wrote:

> I'd be interested in finding out if there are any funded open-source 
> projects to use Coq that are looking for help.  The open-source ones 
> couldn't hide how seriously they employ Coq.
>
> I might be headed in the direction of starting such a project myself - but 
> I'd certainly want to know about others first.
>
> -- Jonathan
>
> On 05/23/2014 11:06 AM, Adam Chlipala wrote:
>> I think the risk here is that some companies will hint at more
>> serious Coq use than they actually employ in real product-oriented
>> activity, as a trick to pull in the best developers. ;)
>>
>> On 05/23/2014 11:01 AM, David MENTRE wrote:
>>> Le 23/05/2014 16:43, Adam Chlipala a écrit :
>>>> And how is a random person meant to learn more about the details?
>>>
>>> It is difficult. It is not usual habit for companies to talk about their 
>>> practices (and nowadays everything is "confidential" in a company).
>>>
>>>> If I
>>>> spent a little time poking around their web sites, would I get a
>>>> good sense?
>>>
>>> Probably not, for above reasons.
>>>
>>> Most of the time I found those kind of information through direct 
>>> discussion or through a few lines in a slide.
>>>
>>> For Trusted Labs, you'll find some basic information by googling "trusted 
>>> labs coq" or "trusted logic coq". But probably not detailed enough for an 
>>> advanced user like you.
>>>
>>> Sincerely yours,
>>> david
>>>
>>
>

________________________________
 This message and any attachments are intended solely for the addressees and 
may contain confidential information. Any unauthorized use or disclosure, 
either whole or partial, is prohibited.
E-mails are susceptible to alteration. Our company shall not be liable for 
the message if altered, changed or falsified. If you are not the intended 
recipient of this message, please delete it and notify the sender.
Although all reasonable efforts have been made to keep this transmission free 
from viruses, the sender will not be liable for damages caused by a 
transmitted virus.