coq-club AT inria.fr

Subject: The Coq mailing list

List archive

[Coq-Club] formal models of peripheral devices like GIC, NIC

From: Abhishek Anand <abhishek.anand.iitg AT gmail.com>
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
Date: Mon, 11 May 2020 13:27:09 -0700
Authentication-results: mail3-smtp-sop.national.inria.fr; spf=None smtp.pra=abhishek.anand.iitg AT gmail.com; spf=Pass smtp.mailfrom=abhishek.anand.iitg AT gmail.com; spf=None smtp.helo=postmaster AT mail-il1-f171.google.com
Ironport-phdr: 9a23:ZeLJcBwmCCU3OJfXCy+O+j09IxM/srCxBDY+r6Qd2ukUIJqq85mqBkHD//Il1AaPAdyGraMcwLOK6ujJYi8p2d65qncMcZhBBVcuqP49uEgeOvODElDxN/XwbiY3T4xoXV5h+GynYwAOQJ6tL1LdrWev4jEMBx7xKRR6JvjvGo7Vks+7y/2+94fcbglVhDexe7d/IAm5oQnMucQanJZpJ7osxBfOvnZGYfldy3lyJVKUkRb858Ow84Bm/i9Npf8v9NNOXLvjcaggQrNWEDopM2Yu5M32rhbDVheA5mEdUmoNjBVFBRXO4QzgUZfwtiv6sfd92DWfMMbrQ704RSiu4qF2QxLulSwJNSM28HvPh8N/jKxVrhGvqQFhzYHIe4yaLuZyc7nHcN8GWWZMXMBcXDFBDIOmaIsPCvIMMPpDoIn9plsOthu+ChevBOjy1jJIgGX53asn3O88FgzJxhcvH9IPsHTPrNX6KqQSXfqvw6nO1zrDae5Z1S386IjJbhAhruqBXb11ccXLyEkvExnJgUmXqYzgJj6Y0PkGvGeH4eR6T+2vl3InpB9rojip3sohlInHi5wIx13L+it03Zg5KNOmREN4fdOpHpteuz+VOoZyQM4uXmNltTs6x7MGu5O2fyoHxIg5yxLBaPGKcIaF7xT+X+ifJjd4gWhqeLO5hxuq7Uegzff8Vs+q31ZOqipJiMfDuW0Q1xHV98OJSeN981+/1TqT0w3f8OJJLEAumabGKpMsw6Q8mocRvEjeGCL9hV/4g7WMdko+/+il8+Tnbavipp+bL4J0jxvxMqUqmsCmAOQ4NhUCU3GV+eih1rDv4Ff1QLpNjv0xnanZtI7VKd4Hqa6+Bg9Zyocj6xChADe6yNkUg2ULIVZfdB+Ej4XlIUzCLfH5APulnlihkipny+jDPrL7A5XNKnbDkK3mfbZ480NT0hE8zdBe55JPCrEOPvHzVlXru9zeFBA5NRG7z/zmCNV8yoMeVnmCAqCcMKzIsF+I4vgjLPWLZI8QoDr9MeQq5+byjX8lnl8QZbWm3ZwOaHyhAvtmJ1iZbmH3j9caEWYKuxI+Q/bwhF2DVz5TfXeyULgm6jE1EoL1RbvEE4uqmfmK2DqxVsldYXkDAVSRG1/pcZ+FUrECcnTWasRl1z0fXLKsT4sskAy1uRXh475mNfbPvCYRsNTq355o5L79jxY3oBV+D8WG02yOB0hyl2UED2s/1qB+ukxwyRGK16F+j7pZFMBcz/xMWwY+c5XbyropWJjJRgvdc4LRGx6dSdK8DGRpF4Nj85o1e094Xu6aoFXG1iuuDaUSkuXSVpMx+6PYmXP2IpQkkiuU5Owal1AjB/B3Gyimi6p4rVaBAofIlwCYk//ve/1DhWjC82CMyWfIt0ZdAlYpDff1GEsHb06TluzXo1vYRub3W7siOwpFj8WFL/kSZw==

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/

[Coq-Club] formal models of peripheral devices like GIC, NIC, Abhishek Anand, 05/11/2020
- RE: [Coq-Club] formal models of peripheral devices like GIC, NIC, Fernandez, Matthew, 05/11/2020
  - Re: [Coq-Club] formal models of peripheral devices like GIC, NIC, Larry Lee, 05/11/2020
- Re: [Coq-Club] [isabelle] formal models of peripheral devices like GIC, NIC, Hira Taqdees Syeda, 05/12/2020