This week I hosted a monthly meetup of Lisp Ireland, where Rafael Sadykov presented his talk "Lisp & Hardware Verification with ACL2".
ACL2 is a theorem prover implemented in a subset of Common Lisp, and the talk discussed how it can be used for formal verification of various systems, and for hardware verification in particular.
The recording was uploaded here: https://www.youtube.com/watch?v=iFEb9p54x_Q
#LispIreland #Meetup #TechTalk #Lisp #CommonLisp #ACL2 #FormalVerification #HardwareVerification #Ireland
Yaroslav Khnygin /
npub1kz…jvaa5
2024-02-17 19:39:53
Author Public Key
npub1kz0muz0cehys8wwxauh99yw8szwtetvd6axawesgenu64y743q0qtjvaa5Published at
2024-02-17 19:39:53Event JSON
{
"id": "9957b520e15af717b81b122de102cf65c71417a8e22d2016a7939e65bbde17bf",
"pubkey": "b09fbe09f8cdc903b9c6ef2e5291c7809cbcad8dd74dd76608ccf9aa93d5881e",
"created_at": 1708198793,
"kind": 1,
"tags": [
[
"t",
"lispireland"
],
[
"t",
"meetup"
],
[
"t",
"techtalk"
],
[
"t",
"lisp"
],
[
"t",
"commonlisp"
],
[
"t",
"acl2"
],
[
"t",
"formalverification"
],
[
"t",
"hardwareverification"
],
[
"t",
"ireland"
],
[
"proxy",
"https://mastodon.ie/users/surabax/statuses/111948516127918372",
"activitypub"
]
],
"content": "This week I hosted a monthly meetup of Lisp Ireland, where Rafael Sadykov presented his talk \"Lisp \u0026 Hardware Verification with ACL2\".\n\nACL2 is a theorem prover implemented in a subset of Common Lisp, and the talk discussed how it can be used for formal verification of various systems, and for hardware verification in particular.\n\nThe recording was uploaded here: https://www.youtube.com/watch?v=iFEb9p54x_Q\n\n#LispIreland #Meetup #TechTalk #Lisp #CommonLisp #ACL2 #FormalVerification #HardwareVerification #Ireland",
"sig": "1707377f21dce61d00b468b991398871c3d7aa219dbd1dc04488ca776ffb9205498ad991e33a5098d0c0c5110e226c28f3c8a79d952d63feb8aaae2c7bc74419"
}