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,
Monday, November 11, 2013
"EB2ALL is a set of translator tools that automatically generates efficient target programming language code (C, C++, Java and C#) from Event-B formal specification related to the analysis of the complex problems. The EB2ALL contains four plugin namely EB2C, EB2C++, EB2J and EBC#. The goal of EB2ALL is to be able to generate a verified source code that satisfies behavioral properties of the develop formal system (abstractly). The EB2ALL tool is developed as a set of plugins for RODIN development tool under the Eclipse framework. RODIN is an integrated development environment (IDE) for developing Event-B models. The RODIN tool is written entirely in Java and build on top of the Eclipse platform."
Tuesday, November 5, 2013
First International Workshop on Formal Integrated Development Environments (Satellite event of ETAPS)
Call for Papers - F-IDE 2014 - April 6th, 2014, Grenoble, France Call for Papers First International Workshop on Formal Integrated Development Environments (Satellite event of ETAPS) April 6th, 2014, Grenoble, France http://www.ensta-paristech.fr/~etaps/ WORKSHOP AIM High levels of safety, security and also privacy standards require the use of formal methods to specify and develop compliant software (sub)systems. Any standard comes with an assessment process, which requires a complete documentation of the application in order to ease the justification of design choices, code review and proofs. Ideally, an F-IDE dedicated to such developments should comply with several requirements. The first one is to associate a logical theory with a programming language, in a way that facilitates the tightly coupled handling of specification properties and program constructs. The second one is to offer a language/environment simple enough to be usable by most developers, even if they are not fully acquainted with higher-order logics or set theory, in particular by making development of proofs as easy as possible and as readable as possible. The third one is to offer automated management of application documentation. It may also be expected that developments done with such an F-IDE are reusable and modular. Moreover, tools for testing andstatic analysis may be embedded in this F-IDE, to address most steps of the assessment process. TOPICS We encourage submissions presenting and discussing research efforts as well as experience feedbacks on design, development, use of tools aiming at making formal methods "easier" for non-specialists. In this context, the topics include (but are not limited to): - F-IDE building : design and integration of languages, compilation - How to make high-level logical and programming concepts palatable to industrial developers - Integration of Object-Oriented and modularity features - Integration of static analyzers - Integration of automatic proof tools, theorem provers and testing tools - Documentation tools - Impact of tools on certification - Experience reports of developing F-IDE - Experience reports of using F-IDE - Experience reports of formal methods-based assessments of industrial applications We encourage not only mature research results but also submissions presenting innovative ideas and early results are also of interest. SUBMISSIONS Papers (6-14 pages in length), following EPCTS format are expected. They can be: - Research papers providing new concepts and results - Position papers and research perspectives - Experience reports - Tool presentations Submissions will be done via Easychair: https://www.easychair.org/conferences/?conf=fide2014 PROCEEDINGS Final versions of accepted papers will be published in a volume of the Electronic Proceedings in Theoretical Computer Science (EPTCS). IMPORTANT DATES - Abstract submission : 18 December, 2013 - Paper Submission : 23 December, 2013 - Notification : 27 January, 2014 - Final version : 10 February, 2014 - Workshop date: April 6, 2014 PC CO-CHAIRS - Catherine Dubois, Cédric / ENSIIE,
(dot) (at) ensiie (dot) fr - Dimitra Giannakopoulou, NASA Ames, (dot) (at) nasa (dot) gov - Dominique Mery, LORIA / Université de Lorraine, (dot) (at) loria (dot) fr
11th International Colloquium on Theoretical Aspects of Computing 17-20 September 2014, Bucharest, Romania
CALL FOR PAPERS -- ICTAC 2014 ********************************************************************** 11th International Colloquium on Theoretical Aspects of Computing 17-20 September 2014, Bucharest, Romania http://fmi.unibuc.ro/ictac2014 ********************************************************************** ICTAC 2014 is the 11th International Colloquium on Theoretical Aspects of Computing and will bring together practitioners and researchers from academia, industry and government to present research and to exchange ideas and experience addressing challenges in both theoretical aspects of computing and in the exploitation of theory through methods and tools for system development. Another aim of ICTAC is to bring together researchers working on theoretical aspects of computing in order to present their recent results and to discuss new ideas concerning computer science. THEMES AND TOPICS OF PAPERS ICTAC 2014 calls for regular research papers on theories of computation and programming, foundations of software engineering and on formal techniques in software design and verification, as well as papers about tools that support formal techniques for software modeling, system design and verification. The topical areas of the conference include, but not limited to * Automata theory and formal languages; * Principles and semantics of programming languages; * Theories of concurrency, mobility and reconfiguration; * Logics and their applications; * Software architectures, their models, refinement and verification; * Relationship between software requirements, models and code; * Program static and dynamic analysis and verification; * Software specification, refinement, verification and testing; * Model checking and theorem proving; * Models of object and component systems; * Coordination and feature interaction; * Integration of theories, formal methods and tools for engineering computing systems; * Service-oriented architectures: models and development methods; * Models of concurrency, security, and mobility; * Theory of distributed, grid and cloud computing; * Real-time, embedded, hybrid and cyber-physical systems; * Type and category theory in computer science. PAPER SUBMISSION As for the past editions, the proceedings of ICTAC 2014 will be published by Springer in the series Lecture Notes in Computer Science (LNCS) and will be available at the colloquium. Special issue of few journals with extended version of selected papers from ICTAC 2014 is under negotiation. Submissions to the colloquium must not have been published or be concurrently considered for publication elsewhere. All submissions will be judged on the basis of originality, contribution to the field, technical and presentation quality, as well as their relevance to the conference. Regular Papers should not exceed 18 pages in LNCS format (see http://www.springer.de/comp/lncs/authors.html for details). Papers must be submitted by using www.easychair.org/conferences/?conf=ictac2014. IMPORTANT DATES: Abstract submission: 16 March 2014 Submission deadline: 23 March 2014 Paper notification: 30 May 2014 Revised/final paper: 14 June 2014 GENERAL CHAIRS Gabriel Ciobanu, Romanian Academy, ICS, Iasi Florentin Ipate, University of Bucharest, Romania PC CHAIRS Gabriel Ciobanu, Romanian Academy, ICS, Iasi, Romania Dominique Mery, LORIA, Universite de Lorraine, France PROGRAM COMMITTEE Yamine Ait-Ameur, IRIT, ENSEIHT, France Farhad Arbab, CWI and Leiden University, The Netherlands Michael Butler, University of Southampton, UK Ana Calvacanti, University of York, UK Jeremie Chalopin, CNRS, France Zhenbang Chen, National University of Defense Technology, China Maximiliano Cristia, Faculty of Exact Sciences, Argentina David Deharbe, Universidade Federal do Rio Grande do Norte, Brazil Rocco De Nicola, IMT Lucca, Italy Jose Luiz Fiadeiro, Royal Holloway, University of London, UK John Fitzgerald, Newcastle University, UK Simon Gay, University of Glasgow, UK Dimitra Giannakopoulou, NASA Ames, USA Stefania Gnesi, ISTI-CNR, Italy Lindsay Groves, Victoria University of Wellington, New Zealand Geoff Hamilton, Dublin City University, Ireland Ian J. Hayes, University of Queensland, Australia Rob Hierons, Brunel University, UK Jane Hillston, University of Edinburgh, UK Ross Horne, Romanian Academy, Iasi, Romania Zhenjiang Hu, National Institute of Informatics, Japan Florentin Ipate, University of Bucharest, Romania Tudor Jebelean, Johannes Kepler University, Austria Cliff Jones, Newcastle University, UK Lila Kari, University of Western Ontario, Canada Jetty Kleijn, Leiden University, The Netherlands Maciej Koutny, Newcastle University, UK Yassine Lakhnech, VERIMAG, France Kim G. Larsen, Aalborg University, Denmark Insup Lee, University of Pennsylvania, USA Axel Legay, INRIA, France Martin Leucker, University of Lubeck, Germany Zhiming Liu, UNU-IIST, Macau, China Marius Minea, Politehnica University of Timisoara, Romania Victor Mitrana, University of Bucharest, Romania Rosemary Monahan, National University of Ireland, Ireland Mohammed Mosbah, LABRI, University of Bordeaux, France Tobias Nipkow, Technical University Munich, Germany Manuel Nunez, Universidad Complutense de Madrid, Spain Paritosh Pandya, Tata Institute of Fundamental Research, India Jun Pang, University of Luxembourg, Luxembourg Corina Pasareanu, NASA Ames, USA Shengchao Qin, University of Teesside, UK Antonio Ravara, Universidade Nova de Lisboa, Portugal Grigore Rosu, University of Illinois at Urbana Champaign, USA Augusto Sampaio, Federal University of Pernambuco, Brasil Pierre-Yves Schobbens, Universite de Namur, Belgium Emil Sekerinski, McMaster University, Canada Natarajan Shankar, SRI International, USA Viorica Sofronie-Stokkermans, Max Planck Institute, Germany Gheorghe Stefanescu, University of Bucharest, Romania Andrzej Tarlecki, Warsaw University, Poland Elena Troubitsyna, Abo Akademi University, Finland Emilio Tuosto, University of Leicester, UK Martin Wirsing, Ludwig-Maximilian University of Munich, Germany Burkhart Wolff, Universite de Paris-Sud, France Jim Woodcock, University of York, UK Fatiha Zaidi, Universite de Paris-Sud, France Naijun Zhan, Chinese Academy of Sciences, China Jianjun Zhao, Shanghai Jiao Tong University, China Huibiao Zhu, East China Normal University, China STEERING COMMITTEE Ana Cavalcanti, University of York, United Kingdom John Fitzgerald, Newcastle University, UK Martin Leucker, University of Luebeck, Germany Zhiming Liu, UNU-IIST, Macao, China Tobias Nipkow, Technical University Munich, Germany Augusto Sampaio, Federal University of Pernambuco, Brasil Natarajan Shankar, SRI International, USA ********************************************************************** This call for papers and additional information about the conference can be found on the ICTAC 2014 web page http://fmi.unibuc.ro/ictac2014/. For information regarding the conference and other queries, you can use the conference email address: email@example.com **********************************************************************
Sunday, October 13, 2013
Friday, October 4, 2013
|Research paper and answers to case study submission:||January 14, 2014|
|Workshop proposal submissions:||October 15, 2013|
|Short paper submission:||February 3, 2014|
|Tutorial proposal submissions:||January 30, 2014|
|Papers/abstract/answers to case study notification:||March 1, 2014|
|Workshop proposal notifications:||November 30, 2013|
|Final Version due:||March 20, 2014|
|Tutorial proposal notifications:||Febuary 28, 2014|
|Main ABZ 2012 conference:|
Tuesday, September 17, 2013
Thursday, August 29, 2013
Sunday, April 7, 2013
CALL FOR PARTICIPATION: FormaliSE 2013 FME Workshop on Formal Methods in Software Engineering held in conjunction with ICSE 2013 Saturday 25 May 2013, San Francisco, USA http://www.formalise.org/ WORKSHOP SCOPE The 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 the correct behavior of the delivered software. The lack of formalization in key places makes software engineering overly sensitive to the weaknesses that are inevitable in the complex activities behind software creation. Aids to precision in each phase of software development and crosschecking are essential, and this is precisely one the objectives of formal methods. After decades of research, and despite significant advancement, formal methods are still not widely used in industrial software development. This may be due to the fact that the formal methods community has not enough focused its attention to software engineering needs, and its specific role in the software process. At the same time, from 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. The main goal of the workshop is to foster integration between the formal methods and the software engineering communities with the purpose to examine the link between the two more carefully than is currently the case. PROGRAM Invited keynote: Though this be madness, yet there is method in it? Alan Wassyng (McMaster University, Canada) Session 1: Specification Do You Speak Z? Formal Methods under the Perspective of a Cross-Cultural Adaptation Problem Andreas Bollin (Alpen-Adria Universitat, Austria) Session 2: Verification Functional SMT solving with Z3 and Racket Siddharth Agarwal and Amey Karkare (Indian Institute of Technology Kanpur, India) Trace Based Reachability Verification for Statecharts Kumar Madhukar, Ravindra Metta, Ulka Shrotri and R. Venkatesh (Tata Consultancy Services, India) An Integrated Data Model Verifier with Property Templates Jaideep Nijjar, Ivan Bocic and Tevfik Bultan (University of California at Santa Barbera, USA) Session 3: Application of Formal Methods Towards a Formalism-Based Toolkit for Automotive Applications Rainer Gmehlich, Katrin Grau, Felix Loesch, Alexei Iliasov, Michael Jackson and Manuel Mazzara Recommendations for Improving the Usability of Formal Methods for Product Lines Joanne M. Atlee, Sandy Beidu, Nancy A. Day, Fathiyeh Faghih and Pourya Shaker (University of Waterloo, Canada) Lightweight Formal Models of Software Weaknesses Robin Gandhi, Harvey Siy and Yan Wu (University of Nebraska at Omaha, USA) Session 4: Timed systems Automatic Validation of Infinite Real-Time Systems Thomas Göthel and Sabine Glesner (Technische Universitat Berlin, Germany) A framework for the rigorous design of highly adaptive timed systems Louis-Marie Traonouez, Axel Legay, Maxime Cordy and Pierre-Yves Schobbens (University of Namur, Belgium, and INRIA Rennes, France) Closing: Round table and discussion For more details see www.formalise.org, REGISTRATION for the workshop is open, see http://2013.icse-conferences.org/content/registration (early registration with reduced rates closes on 14 April 2013). For HOTELS and VENUE see http://2013.icse-conferences.org/content/venue OC/PC CHAIRS Stefania Gnesi (ISTI-CNR, Italy) Nico Plat (West Consulting BV, The Netherlands). The OC/PC Chairs can be reached via e-mail: firstname.lastname@example.org. PROGRAM COMMITTEE * Yamine Ait-Ameur (IRIT/ENSEEIHT, France) * Manfred Broy (Technical University München, Germany) * Jürgen Dingel (Queen's University, Canada) * Cindy Eisner (IBM Haifa Research Laboratory, Israel) * Arie Gurfinkel (Carnegie Mellon University, USA) * Patrick Heymans (University of Namur, Belgium, and INRIA, France) * Alessandro Fantechi (Università di Firenze, Italy) * Connie Heitmeyer (Naval Research Laboratory, USA) * Mike Hinchey (Lero, Ireland) * Axel van Lamsweerde (University of Louvain. Belgium) * Peter Gorm Larsen (Aarhus University, Denmark) * Marc Lawford (MacMaster University, Canada) * Thierry Lecomte (ClearSy, France) * Yves Ledru (IMAG, France) * Antónia Lopes (University of Lisbon, Portugal) * Tiziana Margaria (Potsdam University, Germany) * Henry Muccini (Università dellAquila, Italy) * Isabelle Perseil (Inserm, France) * Steve Riddle (University of Newcastle, UK) * Matteo Rossi (Politecnico di Milano, Italy) * Wolfram Schulte (Microsoft, USA) * Elena Troubitsyna (Abo University, Finland) * Sebastián Uchitel (Imperial College and Universidad de Buenos Aires) * Willem Visser (University of Stellenbosch, South Africa) * Fatiha Zaïdi (LRI/CNRS, France) _______________________________________________ events mailing list email@example.com http://fmeurope.hosting.west.nl/mailman/listinfo/events