This week I revived an old github project and migrated it to codeberg: https://codeberg.org/jepler/ProvenDelights

Long ago I had hoped to write "proofs" for many of the programs in the book Hacker's Delight using cbmc. I only got a few done and archived the project.

cbmc is neat for this because, when it CAN prove a result, it proves it about a C program with full C semantics not just (for instance) abstractly on the integers.

A few days ago a friend nerd-sniped me into writing a certain function and I wanted to make sure it was correct. ProvenDelights had all the infrastructure to help me do that so I dusted it off and added two new proofs. Then I went ahead and migrated it from github pages to grebedoc as well, and transitioned from asciidoc to asciidoctor. tl;dr now the small set of proofs can be read at https://jepler.grebedoc.dev/ProvenDelights/

#codeberg #grebedoc #cbmc

Voor de najaarseditie van Business Contact, een uitgave van CBMC Nederland, maakte ik ook de foto's bij het interview met Piet van Ommeren. Begonnen als metselaar, bouwde hij zijn onderneming uit tot een bloeiend aannemersbedrijf. Een mooi gesprek over stille tijd in de vroege ochtend, wonderen door gebed en ondernemen op de smalle weg.

https://www.raes-media.nl

#interview #fotoshoot #cbmc

Voor de najaarseditie van Business Contact, een uitgave van CBMC Nederland, maakte ik ook de foto's bij het interview met Piet van Ommeren. Begonnen als metselaar, bouwde hij zijn onderneming uit tot een bloeiend aannemersbedrijf. Een mooi gesprek over stille tijd in de vroege ochtend, wonderen door gebed en ondernemen op de smalle weg.

https://www.ralphoto.nl

#interview #fotoshoot #cbmc

Voor de najaarseditie van Business Contact, een uitgave van CBMC Nederland, maakte ik ook de foto's bij het interview met Piet van Ommeren. Begonnen als metselaar, bouwde hij zijn onderneming uit tot een bloeiend aannemersbedrijf. Een mooi gesprek over stille tijd in de vroege ochtend, wonderen door gebed en ondernemen op de smalle weg.

#interview #fotoshoot #cbmc @ralphoto

Voor de najaarseditie van Business Contact, een uitgave van CBMC Nederland, maakte ik ook de foto's bij het interview met Piet van Ommeren. Begonnen als metselaar, bouwde hij zijn onderneming uit tot een bloeiend aannemersbedrijf. Een mooi gesprek over stille tijd in de vroege ochtend, wonderen door gebed en ondernemen op de smalle weg.

#interview #fotoshoot #cbmc

Начали за здравие (нашёл время попробовать CBMC для поиска проблем в коде PUC Rio Lua), а кончили за упокой (оформил два тикета в сам CBMC).

• https://github.com/diffblue/cbmc/issues/8278
• https://github.com/diffblue/cbmc/issues/8276

#CBMC