The 7th Conference on Formal Methods in Software Engineering, FormaliSE 2019, was organized as a one-day event in Montréal, Canada on 27 May. The event was attended by roughly 45 researchers, including people from industry as well as academia in the area of Formal Verification from around the globe. A detailed report can be found here.
Proceedings
The proceedings of the conference were published as part of the ICSE 2019 Workshop Proceedings in the ACM and IEEE Digital Libraries.
Keynote by Dr. Jeff Joyce
Title of the keynote: The Benefits of (having doubts about) Formal Methods
To believe with certainty we must begin with doubting - Stanisław Leszczyński (1677 – 1766)
Abstract: A variety of industry standards for critical systems, such as RTCA DO-178C and ISO 26262, refer to the possibility of using formal methods to produce verification results for the purpose of certification. However, satisfying the expectations of a certification authority using verification results obtained by means of formal methods can be a formidable challenge. Dr. Joyce will describe some reasonable doubts that might be raised by a certification authority about a plan to use formal methods as a source of verification results in place of test-based results. He will explain how such doubts influenced guidance developed by the aerospace industry for use of formal methods in the certification of airborne software. Anticipating these doubts can be the basis of an effective strategy to use formal methods as part of the certification of a critical system.
Dr. Jeffrey Joyce is the co-founder and managing director of a Vancouver-based engineering consultancy, Critical System Labs Inc., (CSL) that provides clients with expertise in the specification, analysis and certification of software-intensive critical systems. Jeff has more than 30 years of experience across a variety of technical domains including aerospace, automotive, defence, energy, medical devices and rail signalling systems. He has served on international working groups that have developed industry standards such as RTCA DO-178C (airborne software), RTCA DO-333 (formal methods) and ISO 26262 (automotive). In 1990, Jeff earned a doctorate from Cambridge University following earlier degrees from the University of Calgary and the University of Waterloo. His doctoral research under the supervision of Prof. Michael Gordon was among early work on the use of formal methods to verify digital hardware. More recently, Jeff and his CSL colleagues have used formal methods to verify aspects of critical software systems for clients in aerospace, automotive and high-energy physics.
You can watch a video of his keynote here.
Programme
08:40: Welcome
08:50: Session 1
- 08.50-09.15: Epistemic Model Checking of Distributed Commit Protocols with Byzantine faults. Omar Bataineh and Mark Reynolds. NTU (SIngapore) and The Univeristy of Western Australia (Australia)
- 09.15-09.40: Rigorous Design and Deployment of IoT Applications. Ajay Krishna, Michel Le Pallec, Radu Mateescu, Ludovic Noirie and Gwen Salaün. INRIA (France), Nokia Bell Labs (France) and University of Grenoble Alpes (France)
- 09.40-10.05: Static Analysis for Worst-Case Battery Utilization. Dmitry Ivanov and Sibylle Schupp. Hamburg University of Technology (Germany)
- 10.05-10.30: Clock Reduction in Timed Automata while Preserving Design Parameters. Beyazit Yalcinkaya and Ebru Aydin Gol. Middle East Technical University (Turkey)
10:30: Coffee break
11:00: Session 2
- 11:00-12:05: Keynote presentation: The Benefits of (having doubts about) Formal Methods. Dr. Jeffrey Joyce. Critical System Labs Inc. (Canada)
- 12.05-12.30: FASTEN: An Open Extensible Framework to Experiment with Formal Specification Approaches - Using Language Engineering to Develop a Multi-Paradigm Specification Environment for NuSMV. Daniel Ratiu, Marco Gario and Hannes Schoenhaar. Siemens Corporate Technology (Germany and USA)
12:30: Lunch
14:00: Session 3
- 14.00-14.25: Parallelizable Reachability Analysis Algorithms for Feed-Forward Neural Networks. Hoang-Dung Tran, Patrick Musau, Diego Manzanas Lopez, Xiao Dong Yang, Luan Nguyen, Weiming Xiang and Taylor Johnson. Vanderbilt University (USA) and University of Pennsylvania (USA)
- 14:25-14.40: Towards Sampling and Simulation-Based Analysis of Featured Weighted Automata (short Paper). Maxime Cordy, Axel Legay, Sami Lazreg and Philippe Collet. University of Luxembourg (Belgium), UCLouvain (Belgium), University Cote d'Azur (France)
- 14:40-15:05: Verifying Channel Communication Correctness for a Multi-Core Cooperatively Scheduled Runtime Using CSP. Jan Pedersen and Kevin Chalmers. University of Nevada at Las Vegas (USA) and Edinburgh Napier University (UK)
- 15:05-15.30: A Generalized Program Verification Workflow Based on Loop Elimination and SA Form. Cláudio Belo Lourenço, Maria João Frade and Jorge Sousa Pinto. LRI, Université Paris-Sud & INRIA Saclay (France) and HASLab/INESC TEC & Universidade do Minho (Portugal)
15:30: Tea break
16:00: Session 4
- 16.00-16.25: Modular Synthesis of Verified Verifiers of Computation with STV Algorithms. Milad K. Ghale, Dirk Pattinson and Michael Norrish. The Australian National University (Australia)
- 16.25-16.40: A Vision for Helping Developers Use APIs by Leveraging Temporal Patterns (short Paper). Erick Raelijohn, Michalis Famelis and Houari Sahraoui. University of Montréal (Canada)
- 16.40-17.05: A Proof-Producing Translator for Verilog Development in HOL. Andreas Lööw and Magnus O. Myreen. Chalmers University of Technology (Sweden)
- 17.05-17.30: On the Formalization of Importance Measures using HOL Theorem Proving. Waqar Ahmad, Shahid Murtaza, Osman Hasan and Sofiene Tahar. Concordia University (canada) and National University of Sciences and Technology (Pakistan)
- 17.30-18.00: Discussion/closing
18:00: End of FormaliSE 2019
PC Chairs
PC Chairs for FormaliSE 2019 were:
- Nancy Day, (Canada)
- Matteo Rossi (Italy)
Social Media Chair:
- Eunsuk Kang (USA)
Communications Chair:
- Stéphanie Challita (France)
Programme Committee
- Marcello Bersani (Politecnico di Milano)
- Dirk Beyer (Ludwig-Maximilians-Universität München, Germany)
- Domenico Bianculli (University of Luxembourg, Luxembourg)
- Simon Bliudze (INRIA Lille, France)
- Andreas Bollin (Alpen-Adria-Universität Klagenfurt, Austria)
- Einar Broch Johnsen (Oslo University, Norway)
- Ana Cavalcanti (University of York, UK)
- Marsha Chechik (University of Toronto, Canada)
- Juergen Dingel (Queen's University, Canada)
- Amy Felty (University of Ottawa, Canada)
- Marc Frappier (Université de Sherbrooke, Canada)
- Carlo Alberto Furia (Università della Svizzera Italiana, Switzerland)
- Peter Gorm Larsen (Aarhus University, Denmark)
- Arie Gurfinkel (University of Waterloo, Canada)
- Marieke Huisman (University of Twente, The Netherlands)
- Eunsuk Kang (Carnegie Mellon University)
- Mark Lawford (McMaster University, Canada)
- Robyn Lutz (Iowa State University, USA)
- Paolo Masci (National Institute of Aerospace, USA)
- Richard Paige (University of York, UK)
- Corina Pasareanu (NASA, USA)
- Patrizio Pelliccione (University of Gothenburg | Chalmers University of Technology, Sweden)
- Gerardo Schneider (Chalmers, Sweden)
- Paola Spoletini (Kennesaw State University, USA)
- Jun Sun (Singapore University of Technology and Design, Singapore)
- Maurice ter Beek (ISTI-CNR, Italy)
- Stefano Tonetta (Fondazione Bruno Kessler, Italy)
- Michael Whalen (University of Minnesota, USA)
- Kirsten Winter (University of Queensland, Australia)
Organizing Committee
Organizing Committee members for FormaliSE 2019:
- Stefania Gnesi (ISTI-CNR, Italy)
- Nico Plat (Thanos, The Netherlands