As part of the symposium, Lero hosted a "Formal Methods Limerick" competition.  A Limerick, named after the city of Limerick, is a popular form of poem, usually whimsical and sometimes risque', using an a-a-b-b-a rhyming scheme.

A prize was offered to the best Limerick on the topic of formal methods. The following was the winning entry:-

Ken Pierce, Newcastle University

In addition, a special prize was given to a Limerick that was both on the topic of formal methods and began with the line "There once was a man from Nantucket". The winning entry was:-

There once was a man from Nantucket
Who thought Z could help him to duck it
But suck it and C,
Just try it in B.
If informal he knew he would muck it.

Jonathan P. Bowen, Museophile Limited , UK

David Gries - An argument, in limerick form, calculated to change the teaching of logic

THANKS TO ALL FOR ENTERING !

Here's a late one since it's lunch time: There was a young man from Vancouver He thought he was really a mover He made an advance To a girl at the dance But she called him a French theorem prover! Ken Pierce et al

There once was a formal expert from Baghdad asserting that he was a postgrad mathematically commanding beyond your understanding solving problems you didn’t knew you had. Claus B. Nielsen

There once was a man from Nantucket who wanted to prove there was no hole in his bucket. A bit of water proved ample to find a counterexample to the property of the imperviousity of the bucket. Kristin Y. Rozier

I once found a beautiful lady Who would enjoy time with FM geeks greatly She had huge "eyes" And the perfect size Of 1920x1080 [of nineteen twenty | by a thousand | and eighty] Pawel Gancarski

We learned about fuzzy autofocus And lots more fun hocus pocus. "Come, Let's Play" Said Harel today. He surely is no diplodocus. Jonathan Bowen

There once were three Irish wise Michaels Who continued in infinite cycles. At FM here, phew, We only have two, With no Micheal mac an Airch an Airch an Airch an Airch an Airch an Airch an Airch an Airch an Airch an Airch an Airch an Airch an Airch ... Jonathan Bowen

There once was a man from Nantucket Who thought Z could help him to duck it. But suck it and C, Just try it in B. If informal he knew he would muck it. Jonathan Bowen

There once was a Butler who could B And everyone thought that he would B. When asked to be chair, He just scratched his hair, But everyone thought that he should B. Jonathan Bowen

There once was a chairman from Lero Who could not play fiddle like Nero. So he organized FM With only some FN And everyone thought him a hero. Jonathan Bowen

There once was a smart man from Cork. I forget if he said Cork or not Cork. Not not Cork would do Since not false is true, So Boole came from Cork and not not Cork. Jonathan Bowen

There once was a girl from Torbay Who was struck by a young man's display She said, "Overture?" He said, "Oh, for sure!" And the rest I really can't say. Ken Pierce, Newcastle University, UK and Sune Wolff, Kenneth Lausdahl, and Claus Nielsen, Aarhus School of Engineering, Denmark

This one has a few maths symbols in and needs to be read in the right way. PDF and image uploaded here: http://www.metaq.org/limerick/limerick1.png http://www.metaq.org/limerick/limerick1.pdf This should be read as: A guy met a girl in a shop He eyed her bottom and top For all of his flaws A quick chat-up clause And inter bed they did hop LaTeX source: \documentclass{minimal} \begin{document} \setlength{\parindent}{2em} \noindent A guy met a girl in a shop \He eyed her $\bot$ $\wedge$ $\top$ \\indent $\forall$ of his flaws \\indent A quick chat-up clause \And $\cap$ bed they did hop \ \end{document} Ken Pierce, Newcastle University

Once upon a time, Rozier and Vardi were checking LTL satisfiability. They said "oh what the heck, let's re-encode this spec," and improved their time exponentially. Kristin Y. Rozier

There once was a man from Nantucket, Whose proof method was see-it-and-suck-it, His coding was vigorous, But not very rigorous; When contradiction appeared, he'd duck it.  Michael Banks & Jeremy Jacob

There once was a man from Nantucket Who an error through checking, he'd snuck it It led to disaster He tried "bandage and plaster" But his system, it still kicked the bucket Steve Reeves

There once was a man from Nantucket vainly dating his girlfriend named Astrid. Charmed by the KeY system she never had kissed him "if you truely love me then prove it" Peter H. Schmitt, KIT

A process 'P' of CCS loved the CSP process princess. He lay in bed wishin' for their composition but alas: he'd the wrong SOS. Colm Bhandal

There once was a man from Nantucket Who set off on a cool little junket He searched far and wide For a method that provides Verification and validation in one bucket Rosalynne Strickland

There once was a man from Nantucket, Who, despising FM said: Oh f**k it! Just lash up the code, And then sell a great load. Complaints can go in the spam bucket. Richard Banach

There once was a man from Nantucket Who kept a Petri net in his pocket. One never knows, he said With some luck and God’s aid Big fish may turn up in my basket! Sacha Krakowiak

There once was a man from Nantucket Whose code from the air he would pluck it Once he was asked if he Would stand by its quality He said back: "Oh no! We'll just luck it!" Steve Reeves

There once was a man from Nantucket Who kept all his code in a bucket When asked for assurance He'd built for endurance He said "Good point, but I'll just duck it" Steve Reeves