[TYPES/announce] Fun With Formal Methods: 2nd CFP and deadline extension (till April 27, 2013)

Николай Шилов shilov at iis.nsk.su
Thu Apr 18 02:56:25 EDT 2013

Fun With Formal Methods FWFM*2013 (http://www.iis.nsk.su/fwfm2013)
One day workshop Saturday, July 13, 2013, Saint Petersburg, Russia

Affiliated with the 25th International Conference on Computer Aided
Verification  (http://cav2013.forsyte.at/)

45 years have passed since Robert W. Floyd published the first research that
explicitly discussed formally how to assign meaning to programs. More than a
decade has passed already since David A. Schmidt published an appeal  On the
Need for a Popular Formal Semantics.  But recently David L.  Parnas have
called Really Rethinking “Formal Methods”, to question the assumptions
underlying the well-known current formal software development methods to see
why they have not been widely adopted  and what should be changed.  So,
things are right where they started decades ago? 
Not at all, since industrial applications of Formal Methods are not the
unique measure of success. Another dimension where we can discuss utility of
Formal Methods could be better education.  A very popular (in Russia)
aphorism of Mikhail Lomonosov  (the first  Russian academician) says:
“Mathematics should be learned just because it disciplines and bring up the
mind”. We do believe that Formal Methods discipline and bring up minds in
Computer Science. We would not like to say that educators should not care
about industrial applications of Formal Methods (quite opposite, we must
care!). At the same time Formal Methods education helps to bridge a
“cultural gap” (E.W.Dijkstra) between Mathematics and Computer Science. 

The problem is how to overcome a stable allergy to Formal Methods: many
people think Formal Methods are too pure in theory but too poor in practice.
We do believe that the basic reason behind this allergy is the absence of
primary, elementary level. It is not wise to start teaching arithmetic from
Peano axiomatic, but it is a common sense to start from elementary problems
about numbers of apples, pencils, etc.  For example, nobody  teaches primary
school  children  to prove  in Peano axiomatic ((x  + y) + z) = (x  + (y  +
z)) for all x, y and z,  but everyone  teaches to solve elementary problems
like the following one: I gave 5 apples to Peter, and then he gave 2 apples
to John; how many apples does Peter have after that? (If you think that he
has 3 apples, you are not right, since he has 3 at least.)

In our vision, a part of the reason of student’s and engineer’s poor
attitude to Formal Methods, is very simple:  FM-experts do not care about
primary education in this field at   the early stage of higher education. In
particular, many courses on Formal Semantics start with fearful terms like
state machine, logic inference, denotational semantics, etc., without
elementary explanations of the basic notions. 

Workshop Topics and Scope
The workshop is designed for
1.	enjoying the art and beauty of Formal Methods,
2.	discussing experience how to make Formal Methods easy, 
3.	presenting application of Formal Methods to puzzles, to games, etc.,
4.	non-standard problem solving outside programming and Computer
5.	everything else about Fun and Joy of Formal Methods.

Inivited Speakers:
1.	Yuri Karpov (Saint-Petersburg State Polytechnic University, Russia)
2.	John Rushby (SRI International, California, USA)

Program Committee
•	Paul Curzon (Queen Mary, University of London),
•	Vladimir Itsykson (Saint-Petersburg State Polytechnic University,
•	Victor Kuliamin (Institute for System Programming, Russia),
•	Dominique Mery (LORIA & Universit? de Lorraine, France),
•	Nikolay Nepejvoda (Program Systems Institute, Russia),
•	Nikolay Shilov (chair, Institute of Informatics Systems, Russia),
•	Rostislav Yavorsky (“Skolkovo”, Russia).

Submission and Proceedings 
•	Original and published papers on topics related to FWFM are
•	There is no any strict limit for page number or style, but it is
recommended to be in range 4-16 pages (single column, single interval, font
not less than 12 for review convenience).
•	All submissions must be made electronically in PDF format via
EasyChair conference management system
•	We plan to publish informal proceedings before the workshop and
disseminate them among participants at the workshop on USB-sticks.  
•	Publication of the post-workshop proceedings will be discussed at
the workshop. 

Important Dates
•	Saturday, April 27th, 2013: Paper submission deadline (Extended but
•	Saturday, May 11th, 2013: Author notification
•	Saturday, May 26th, 2013: Camera ready version for preliminary
•	Saturday, July 13th, 2013: Workshop
•	Saturday, July 13th – Friday, July 19th, 2013: CAV Conference

Registration and Fees
Workshop registration fees will be collected together with CAV registration
fees. From these registration fees CAV provides workshop participants with:
registration, meeting facilities, lunches, coffee breaks, and proceedings on
USB sticks.

As usual for CAV, the workshop registration fee will be uniform and it will
depend only on the number of workshop days people take part in, i.e., one
day (1D) or two days (2D). Each participant registering for a workshop has
the right to attend the other workshops on the same day.

Visa Information
The majority of foreign participants will need visas to enter Russia, this
is a two step process: First, one has to obtain a visa invitation letter;
Then, having the letter, one applies for a visa through the local Russian
The deadline for visa invitation letters through CAV is March 20, 2013 for
non¬EU citizens and April 10, 2013. After the deadline the participants will
have to apply for a tourist visa invitation through the hotel.
We kindly ask submission authors and potential participants to apply for a
visa invitation letter as soon as possible (even if their trip/participation
plans may change later). For further details please check:

Contact Nikolay Shilov (e-mail: shilov at iis.nsk.su, homepage:

More information about the Types-announce mailing list