Partner Event: Deductive Verification of State Machine Specifications with Why3 About the event Join Huawei for this Coffee House Tech talk, taking place on 7th of March. Abstract State machines are the foremost mechanism used to specify distributed algorithms and protocols. Formal verification of these algorithms has essentially been done using model checking tools, which are very useful for finding bugs but less effective in providing correctness guarantees. When such guarantees are sought, an approach based on deductive verification must be used. In the case of sequential software, significant advances in logics, techniques, and tools have contributed to make deductive verification effective in practice. More recently deductive approaches have also been proposed for verifying distributed algorithms, either supported by dedicated tools (TLAPS and Ivy), or based on interactive theorem provers like Coq or Isabelle/HOL. In this talk they argue that the power of automated reasoning can be brought to the verification of distributed systems through the use of a general-purpose verifier. They employ the Why3 deductive verifier, a tool acclaimed for its modeling language (WhyML), library of logic theories, support for many external proof tools, and an extraction mechanism capable of automatically producing correct-by-construction OCaml code. They show how Why3 can be used to reason about state machine specifications, and give examples demonstrating that distributed algorithms can be formalized in WhyML in a natural way, and their safety properties proved with a high degree of automation. Finally they consider the use of refinement, a useful technique that allows for hierarchical development and verification of state machine specifications. They give a simple Why3 theory of refinement, and show examples of nontrivial distributed lgorithms that they have proved correct by refinement. Speaker Bio Jorge Sousa Pinto is an associate professor with habilitation at the Computer Science Department, Universidade do Minho, and a senior researcher at the High Assurance Software laboratory, HASLab/INESCTEC. He received his PhD in theoretical computer science from École Polytechnique, France, where he worked on Interaction Nets and the Geometry of Interaction under the supervision of Ian Mackie and Radhia Cousot. His research in recent years has focused on deductive program verification. He is one of the authors of the textbook "Rigorous Software Development - An Introduction to Program Verification". Mar 07 2023 11.00 - 12.00 Partner Event: Deductive Verification of State Machine Specifications with Why3 Join Huawei for this Coffee House Tech talk, taking place on 7th of March. Where (Physically) : Coffee House, 4/F, Bayes Centre, 47 Potterrow, Edinburgh EH8 9BT, UK Where (Virtually) : https://meeting.zhumu.me/wc/98895877/join?track_id=&jmf_code=&meeting_result=&tk=&cap=d7cec&prefer=0 Register
Partner Event: Deductive Verification of State Machine Specifications with Why3 About the event Join Huawei for this Coffee House Tech talk, taking place on 7th of March. Abstract State machines are the foremost mechanism used to specify distributed algorithms and protocols. Formal verification of these algorithms has essentially been done using model checking tools, which are very useful for finding bugs but less effective in providing correctness guarantees. When such guarantees are sought, an approach based on deductive verification must be used. In the case of sequential software, significant advances in logics, techniques, and tools have contributed to make deductive verification effective in practice. More recently deductive approaches have also been proposed for verifying distributed algorithms, either supported by dedicated tools (TLAPS and Ivy), or based on interactive theorem provers like Coq or Isabelle/HOL. In this talk they argue that the power of automated reasoning can be brought to the verification of distributed systems through the use of a general-purpose verifier. They employ the Why3 deductive verifier, a tool acclaimed for its modeling language (WhyML), library of logic theories, support for many external proof tools, and an extraction mechanism capable of automatically producing correct-by-construction OCaml code. They show how Why3 can be used to reason about state machine specifications, and give examples demonstrating that distributed algorithms can be formalized in WhyML in a natural way, and their safety properties proved with a high degree of automation. Finally they consider the use of refinement, a useful technique that allows for hierarchical development and verification of state machine specifications. They give a simple Why3 theory of refinement, and show examples of nontrivial distributed lgorithms that they have proved correct by refinement. Speaker Bio Jorge Sousa Pinto is an associate professor with habilitation at the Computer Science Department, Universidade do Minho, and a senior researcher at the High Assurance Software laboratory, HASLab/INESCTEC. He received his PhD in theoretical computer science from École Polytechnique, France, where he worked on Interaction Nets and the Geometry of Interaction under the supervision of Ian Mackie and Radhia Cousot. His research in recent years has focused on deductive program verification. He is one of the authors of the textbook "Rigorous Software Development - An Introduction to Program Verification". Mar 07 2023 11.00 - 12.00 Partner Event: Deductive Verification of State Machine Specifications with Why3 Join Huawei for this Coffee House Tech talk, taking place on 7th of March. Where (Physically) : Coffee House, 4/F, Bayes Centre, 47 Potterrow, Edinburgh EH8 9BT, UK Where (Virtually) : https://meeting.zhumu.me/wc/98895877/join?track_id=&jmf_code=&meeting_result=&tk=&cap=d7cec&prefer=0 Register
Mar 07 2023 11.00 - 12.00 Partner Event: Deductive Verification of State Machine Specifications with Why3 Join Huawei for this Coffee House Tech talk, taking place on 7th of March.
