[isabelle] 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/



This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.