Alexandre Kirszenberg

In International Journal on Software Tools for Technology Transfer (STTT)

Abstract We introduce Go2Pins, a tool that takes a program written in Go and links it with two model-checkers: LTSMin and Spot. Go2Pins is an effort to promote the integration of both formal verification and testing inside industrial-size projects. With this goal in mind, we introduce black-box transitions, an efficient and scalable technique for handling the Go runtime. This approach, inspired by hardware verification techniques, allows easy, automatic and efficient abstractions.

Learning grayscale mathematical morphology with smooth morphological layers

By Romain Hermary, Guillaume Tochon, Élodie Puybareau, Alexandre Kirszenberg, Jesús Angulo

2022-04-04

In Journal of Mathematical Imaging and Vision

Abstract The integration of mathematical morphology operations within convolutional neural network architectures has received an increasing attention lately. However, replacing standard convolution layers by morphological layers performing erosions or dilations is particularly challenging because the min and max operations are not differentiable. P-convolution layers were proposed as a possible solution to this issue since they can act as smooth differentiable approximation of min and max operations, yielding pseudo-dilation or pseudo-erosion layers.

VerSe: A vertebrae labelling and segmentation benchmark for multi-detector CT images

By Anjany Sekuboyina, Malek E. Husseini, Amirhossein Bayat, Maximilian Löffler, Hans Liebl, Hongwei Li, Giles Tetteh, Jan Kukačka, Christian Payer, Darko Stern, Martin Urschler, Maodong Chen, Dalong Cheng, Nikolas Lessmann, Yujin Hu, Tianfu Wang, Dong Yang, Daguang Xu, and Felix Ambellan, Tamaz Amiranashvili, Moritz Ehlke, Hans Lamecker, Sebastian Lehnert, Marilia Lirio, Nicolás Pérez de Olaguer, Heiko Ramm, Manish Sahu, Alexander Tack, Stefan Zachow, Tao Jiang, Xinjun Ma, Christoph Angerman, Xin Wang, Kevin Brown, Matthias Wolf, Alexandre Kirszenberg, Élodie Puybareau, Di Chen, Yiwei Bai, Brandon H. Rapazzo, Timyoas Yeah, Amber Zhang, Shangliang Xu, Feng Houa, Zhiqiang He, Chan Zeng, Zheng Xiangshang, Xu Liming, Tucker J. Netherton, Raymond P. Mumme, Laurence E. Court, Zixun Huang, Chenhang He, Li-Wen Wang, Sai Ho Ling, Lê Duy Huỳnh, Nicolas Boutry, Roman Jakubicek, Jiri Chmelik, Supriti Mulay, Mohanasankar Sivaprakasam, Johannes C. Paetzold, Suprosanna Shit, Ivan Ezhov, Benedikt Wiestler, Ben Glocker, Alexander Valentinitsch, Markus Rempfler, Björn H. Menze, Jan S. Kirschke

2021-07-22

In Medical Image Analysis

Abstract Vertebral labelling and segmentation are two fundamental tasks in an automated spine processing pipeline. Reliable and accurate processing of spine images is expected to benefit clinical decision support systems for diagnosis, surgery planning, and population-based analysis of spine and bone health. However, designing automated algorithms for spine processing is challenging predominantly due to considerable variations in anatomy and acquisition protocols and due to a severe shortage of publicly available data.

Go2Pins: A framework for the LTL verification of Go programs

By Alexandre Kirszenberg, Antoine Martin, Hugo Moreau, Étienne Renault

2021-06-08

In Proceedings of the 27th international SPIN symposium on model checking of software (SPIN’21)

Abstract We introduce Go2Pins, a tool that takes a program written in Go and links it with two model-checkers: LTSMin [19] and Spot [7]. Go2Pins is an effort to promote the integration of both formal verifica- tion and testing inside industrial-size projects. With this goal in mind, we introduce black-box transitions, an efficient and scalable technique for handling the Go runtime. This approach, inspired by hardware ver- ification techniques, allows easy, automatic and efficient abstractions.

Going beyond p-convolutions to learn grayscale morphological operators

By Alexandre Kirszenberg, Guillaume Tochon, Élodie Puybareau, Jesus Angulo

2021-02-16

In Proceedings of the IAPR international conference on discrete geometry and mathematical morphology (DGMM)

Abstract Integrating mathematical morphology operations within deep neural networks has been subject to increasing attention lately. However, replacing standard convolution layers with erosions or dilations is particularly challenging because the min and max operations are not differentiable. Relying on the asymptotic behavior of the counter-harmonic mean, p-convolutional layers were proposed as a possible workaround to this issue since they can perform pseudo-dilation or pseudo-erosion operations (depending on the value of their inner parameter p), and very promising results were reported.

Go2Pins: A framework for the LTL verification of Go programs (extended version)

Learning grayscale mathematical morphology with smooth morphological layers

VerSe: A vertebrae labelling and segmentation benchmark for multi-detector CT images

Go2Pins: A framework for the LTL verification of Go programs

Going beyond p-convolutions to learn grayscale morphological operators

Search

Tags