The Coq mailing list

["Soegtrop, Michael" <michael.soegtrop AT intel.com>]

Dear David, Anand,

as you mentioned, all links on the first site you mentioned below appear to 
be dead.

The below site from a different university working on CerCo works and also 
links to more papers on this:

http://cerco.cs.unibo.it/

Best regards,

Michael

-----Original Message-----
From: 
coq-club-request AT inria.fr
 
[mailto:coq-club-request AT inria.fr]
 On Behalf Of David MENTRÉ
Sent: Saturday, September 20, 2014 11:28 AM
To: 
coq-club AT inria.fr
Subject: Re: [Coq-Club] microcontroller operational semantics with timing?

Hello,

2014-09-20 05:38, Abhishek Anand:
> Is there a formalization of the operational semantics of a 
> microcontroller (preferably RISC) such that the formalization includes 
> timing behaviour, such as how long (e.g. clock cycles)  programs take 
> to run?

You should have a look at publications and results of project CerCo:

   http://www.pps.univ-paris-diderot.fr/cerco

Especially that paper: http://hal.inria.fr/hal-00702665/en

> It would be great if formalization includes the instructions for 
> interacting with ADCs and digital IO pins.

I don't think that have gone so far.

> If not, does someone have suggestions about a cheap microcontroller 
> that has a simple instruction set with a simple and well documented 
> timing behaviour?

They modeled 8051 processor.

The developments seem to be no longer accessible but the authors would 
probably send it to you.

Best regards,
david