Saturday, December 14, 2013
In this episode of Verification Corner, Jean-Raymond Abrial and Rustan Leino show how to do a design starting from a model that is gradually refined toward executable code. They use the Rodin tool, which supports the Event-B formalism.
Using an extended example that flattens and reconstructs trees, Sophia Drossopoulou and Rustan Leino show how to write inductive proofs of functional programs. The verification tool checks the correctness of the proofs. Proofs can be given in full detail, as they might be when a person first writes the proof or when the proof is intended for human understanding. Alternatively, proofs can be written with less detail, akin to the way a confident mathematician elides some details. In either case, the verification tool is satisfied only if it can fill in the missing pieces of the proof.
Jason Koenig and Rustan Leino show a verification problem that makes use of functions, ghost variables, and lemmas.
In this episode, Rosemary Monahan and Rustan Leino use problems specified using comprehension expressions to demonstrate how a problem can be solved using partial solutions
Conférence de Jean-Raymond Abrial, docteur d'honneur en sciences 2008 à l'UdeS
12 septembre 2008
Professeur invité à l'École polytechnique fédérale de Zurich en Suisse depuis 2004, Jean-Raymond Abrial présente une conférence publique qui s'intitule « Mais si, on peut développer des systèmes informatiques sans fautes! ». Cette présentation se veut en lien direct avec ses grands projets de recherche dans lesquels il s'est investi tout au long de sa carrière exceptionnelle. À l'Agora du Carrefour de l'information, le vendredi 12 septembre 2008, à midi. Jean-Raymond Abrial est venu à Sherbrooke recevoir le 13 septembre le tout premier doctorat honoris causa en sciences dans le domaine de l'informatique de l'Université de Sherbrooke.
Call for Papers: FormaliSE 2014
2nd FME Workshop on Formal Methods in Software Engineeringheld in conjunction with ICSE 2014 (May 31th–June 7th)
IThe software industry has a long-standing and well-earned reputation for
failing to deliver on its promises and it is clear that still nowadays, the
success of software projects with the current technologies cannot be assured.For large complex projects ad hoc approaches have proven inadequate to assure
ey places makes software engineering overly sensitive to the weaknesses thatthe correct behavior of the delivered software. The lack of formalization in
k are inevitable in the complex activities behind software creation. Aids to precision in each phase of software development and crosschecking are
both thinking and documenting the preliminary stage of the softwa
ore creation process. When done well, this can aid all aspects of software creation: user requirement formulation, implementation, verification/testing, and the creation
ed by practitioners, and the integration of such tools with
s are far from the unrealistic assumptions that characterized some earlier research in formal methods. After decades of research, and despite significant advancement, formal methods
needs, and its specific role in the software
process. At the same time, from
g a software engineering perspective, there could be a number of fundamental principles that might help to guide the design of formal methods in order to make them more easily applicable in the development of software applications.
EST include but are not limited to:
- integration of FMs in the software
Rdevelopment life cycle - ability of formal methods to handle real-world problems - prescriptive/objective guidance in the use of FMs - Formal methods in a certification context - “lightweight” or usable FMs - application experiences - scalability of FM applications - experimental validation
e Proceedings Format. They
will be published as part of the (electronic) pro
cceedings of ICSE 2013. All papers submitted to the workshop must be unpublished original work and should not be under review or submitted elsewhere while being under consideration. All submissions must be in English and in PDF format through online upload to the workshop submission website at the following URL:
https://www.easychair.org/conferences/?conf=formalise2014. Three or four PC
members will review all submissions. Papers will be judged on the basis oftheir clarity, relevance, originality, and contribution to the field.
24 February 2
r014: notification of acceptance/rejection to authors
*** Exact date *** 2014: FormaliSE workshop held in H
pyderabad, India OC/PC CHAIRS are Stefania Gnesi (ISTI-CNR, Italy) and Nico Plat (West
vices, India). The OC/PC Chairs can be reached via e-mail:Consulting BV, The Netherlands). Local organizer is Ravindra Metta (Tata Consultancy Se
firstname.lastname@example.org. If you intend to submit a paper you are invited to inform usin advance.
OMMITTEE consists of Andreas Bollin (Klagenfurt University,
Cnar Broch Johnsen (Oslo University, Norway), Manfred Broy
rk University, UK),
Nancy Day (University of Waterloo, Canada), Cindy Eisner (
oIBM Haifa Research Laboratory, Israel) , Alessandro Fantechi (University of Florence, Italy), Jaco
echnology, The Netherlands), Arie Gurfinkel (Carnegie
TUSA), Mike Hinchey (Lero, Ireland), Randolph Johnson (independent consultant, USA), Axel van Lamsweerde (University of Louvain.
France), Yves Ledru
(IMAG, France), Axel Legay (INRIA Rennes, France),
Antónia Lopes (University of Lisbon, Portugal), István Majzik (Budapest University of Technology and Economics, Hungary), Tiziana Margaria (Potsdam University, Germany), Ravindra
Finland) , Sebastián Uchitel (Imperial College and
Universidad de Buenos Aires,
UK and Argentina), Hironori Washizaki (Waseda
France).University, Japan), and Fatiha Zaïdi (LRI/CNRS,