Fun With Formal Methods
One day workshop Saturday, July 13, 2013,
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) = (x + (y + 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
Submission and Proceedings
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.
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 Consulate.
The deadline for visa invitation letters through CAV is March 20, 2013 for nonEU 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: http://cav2013.forsyte.at/visa/.