08:40: Welcome

08:50: Session 1

  • 08.50-09.15: Epistemic Model Checking of Distributed Commit Protocols with  Byzantine faultsOmar 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 UtilizationDmitry Ivanov and Sibylle Schupp. Hamburg University of Technology (Germany)
  • 10.05-10.30: Clock Reduction in Timed Automata while Preserving Design ParametersBeyazit 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 MethodsDr. 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 NetworksHoang-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 ChalmersUniversity 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 AlgorithmsMilad 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 HOLAndreas Lööw and Magnus O. Myreen. Chalmers University of Technology (Sweden)
  • 17.05-17.30: On the Formalization of Importance Measures using HOL Theorem ProvingWaqar 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