The Coq mailing list

[Larry Lee <llee454 AT gmail.com>]

Hi Abhishek,

While working at SiFive, I developed some partially verified models of
memory devices and a UART using Kami, a DSL embedded within Coq. You
can find these models in the ProcKami/Devices directory of the
RiscvSpecFormal project (https://github.com/sifive/RiscvSpecFormal).

Feel free to message me if you have any questions about the code.

- Larry Lee 

On Mon, 2020-05-11 at 21:05 +0000, Fernandez, Matthew wrote:
> There’s a partial model of the GIC in the seL4 proofs [0]. It only
> contains the bare minimum that was necessary for their proofs, but
> maybe this is a good jumping off point.
>  
>  [0]: https://github.com/seL4/l4v
>  
> From: 
> coq-club-request AT inria.fr
>  
> <coq-club-request AT inria.fr>
>  On Behalf
> Of Abhishek Anand
> Sent: Monday, May 11, 2020 13:27
> To: coq-club 
> <coq-club AT inria.fr>;
>  
> cl-isabelle-users AT lists.cam.ac.uk
> Subject: [Coq-Club] formal models of peripheral devices like GIC, NIC
>  
> Has someone built formal models of peripheral devices like Arm's
> Generic Interrupt Controller (GIC), network interface cards that
> could be suitable for proving correctness properties of software
> driving them (e.g. OS, network driver)?
> I'd be grateful for pointers to such work. The models need not be in
> Coq/Isabelle, as long as there is a plausible way to convert them to
> Coq/Isabelle models that describe the behavior of such devices.
>  
> Thanks,
> -- Abhishek
> http://www.cs.cornell.edu/~aa755/