Line 66: | Line 66: | ||
== Testimonials == | == Testimonials == | ||
* [https://prologyear.logicprogramming.org/ColmerauerPrize.html Winner of the first Alain Colmerauer Prize, celebrating the 50th anniversary of Prolog]<i>"The winner of the first edition of the Prize was announced at the Prolog Day Symposium, on November 10, 2022: | * [https://prologyear.logicprogramming.org/ColmerauerPrize.html Winner of the first Alain Colmerauer Prize, celebrating the 50th anniversary of Prolog]<i>"The winner of the first edition of the Prize was announced at the Prolog Day Symposium, on November 10, 2022: ProB: Harnessing the Power of Prolog to Bring Formal Models and Mathematics to Life. Michael Leuschel and STUPS Group."</i> | ||
ProB: Harnessing the Power of Prolog to Bring Formal Models and Mathematics to Life. Michael Leuschel and STUPS Group."</i> | |||
* [https://link.springer.com/chapter/10.1007/978-3-031-67114-2_13 Proving B with Atelier B]<i>" In the early 2000’s, formal data validation started to become more wide-spread in the railways [10]. In particular, the ProB model-checker was first demonstrated during the EU project DEPLOY [13]. After some optimisations, ProB was able to fully handle large size metro data and validation rules, resulting in the generation of one B machine per validation rule and instantiated with the data related to this rule. To date, the biggest B machine generated for data validation and analysed by ProB contains 10 Mloc. With Atelier B 4.3, ProB was added as an interactive command [12]. Its behaviour is similar to the predicate prover: it does not modify the goal, only trying to demonstrate it. It comes with a time limit (maximum duration) and the possibility to reduce the number of hypotheses by selecting those having one symbol in common with the goal. PRoB allows better handling of arithmetic goals and case-based proofs on reduced domains."</i> | * [https://link.springer.com/chapter/10.1007/978-3-031-67114-2_13 Proving B with Atelier B]<i>" In the early 2000’s, formal data validation started to become more wide-spread in the railways [10]. In particular, the ProB model-checker was first demonstrated during the EU project DEPLOY [13]. After some optimisations, ProB was able to fully handle large size metro data and validation rules, resulting in the generation of one B machine per validation rule and instantiated with the data related to this rule. To date, the biggest B machine generated for data validation and analysed by ProB contains 10 Mloc. With Atelier B 4.3, ProB was added as an interactive command [12]. Its behaviour is similar to the predicate prover: it does not modify the goal, only trying to demonstrate it. It comes with a time limit (maximum duration) and the possibility to reduce the number of hypotheses by selecting those having one symbol in common with the goal. PRoB allows better handling of arithmetic goals and case-based proofs on reduced domains."</i> | ||
*[https://link.springer.com/chapter/10.1007/978-3-031-05814-1_11 The 4SECURail Formal Methods Demonstrator, Franco Mazzanti and Dimitri Belli] <i>""The second framework that has been chosen to support the formal analysis of the system is ProB [16]. Indeed, according to several surveys (see, e.g., [17,18,19]) B/EventB appears to be one of the most adopted formal methods in railways. Moreover, ProB has a very user-friendly interface requiring a small effort to be learnt and powerful verification methods. Last but not least, it is freely available as an open-source product."</i> | *[https://link.springer.com/chapter/10.1007/978-3-031-05814-1_11 The 4SECURail Formal Methods Demonstrator, Franco Mazzanti and Dimitri Belli] <i>""The second framework that has been chosen to support the formal analysis of the system is ProB [16]. Indeed, according to several surveys (see, e.g., [17,18,19]) B/EventB appears to be one of the most adopted formal methods in railways. Moreover, ProB has a very user-friendly interface requiring a small effort to be learnt and powerful verification methods. Last but not least, it is freely available as an open-source product."</i> |