goto-instrument" is now "goto-inkstrument", "linking" is now "inking", "goto-cc" is now "goto-sea-sea", etc. ``` _________ _______. _ _ .___/ \ / -_ / \ / \ / _ _ | | _ _ \ | \/ | / / \/ \ | | / \ / \| \ / | |.||.| / | |.| |.|| \ / | \_/\_/ / \_ \_/ \_// \ / \ ___ _/ \ _/ \/ \_\_/ / | \_/ ___\| / ..____/_.. /.-_/o\____/.. .. || o\o \~.o. //~ //..|| \\ .. .. |/ .|| \\.. // || ..|| || .. .. //o .o\\ || .. // // .. // || . .. || .. \o \\ //. // .. || || .. .. o// .. \\ ^\// .. // . |/ .\| .. . // .. || /\ .// .. // . \\ .. . |/ .. \| //\| || ../| .. || .. o .. o l o //.. .|\ .. \\ .. .. |/ .. |/ .. \| .. o . o o ______________ ________ / __ | ___ | \/ / __ \ | / \| |_/ | . . | / \/ | | | ___ | |\/| | | | \__/| |_/ | | | | \__/\ \____\____/\_| |_/\____/ ``` Logo information: ================= The octopus on the left is the "model-checking octopus," and the one on the right is the "path exploration octopus". Their lovemaking symbolises the retrofitting of path-exploration functionality to CBMC in diffblue#1641. Rationale: ========== We're hoping to boost CBMC's uptake and retention amongst customers by adding a fun logo. The "mating octopi" logo was crafted during a several-month long rebranding and outreach effort. We found that customers form positive associations with tech brands that [feature](https://en.wikipedia.org/wiki/Tux_(mascot)) [cute](https://en.wikipedia.org/wiki/Docker_(software)) [animals](https://github.com/logos) as opposed to [fruits](https://www.apple.com/) or [rectangles](https://www.microsoft.com/en-gb). Members of the verification community have responded warmly to this proposed logo; below are a selection of quotes: This is a charming logo, I hope to see it when using CBMC to verify my latest sorting algorithm! Just to think, if only I had devised such a magnificent logo for my process calculus in the 80s, it would not have been usurped by Robin's bald-faced ripoff. -- Tony I like the idea, but don't eight-legged animals have a very large footprint? The logo is also off-centre, adding a proper frame would help here. Finally, the octopuses appear to be hopelessly tangled up and ought to be separated. Fortunately, I came up with a neat trick back in 2001 that could help you with all of these problems... -- Peter You're adding a _logo_ to a _verification tool_? Goto hell. -- Edsgar

Commits

Commits on Mar 30, 2018

Make CBMC more fun