Benedikt Becker

The promise of formal software verification is unique: becoming unconditionally sure about the functioning of software, by translating programs into logic and logically proving the properties of the program. But this surety comes to a price: the verification typically multiplies the effort needed for the implementation. And there are many ways an engineer can get lost on her way. Counterexamples, i.e. program input that trigger contradictions of the program to the specifications, are a common way to help understanding proof failures. In the Why3 framework for deductive program verification (and also in Ada/SPARK), I worked on the automatic classification of counterexample to explain proof failures.

Talks

• Explaining Proof Failures with Giant-Step Runtime Assertion Checking. (F-IDE 2021, slides)
• Ghost Code in Action: Automated Verification of a Symbolic Interpreter Using Why3. (Inria Gallium seminar, 2019, slides)

An important hurdle in the implementation of observational studies and decision making in pharmacoepidemiology lies in the heterogeneity of the data sources: Relevant information may be written in prose by researchers in publications or physicians in medical records, or it may be coded (using more-or-less formalised coding systems) in medical databases. The aim in my PhD was to accelerate the compilation of relevant information about vaccines from heterogeneous data source, which involved extracting information from prose for further automatic processing using natural language processing technologies, and linking heterogeneously coded data and making it available to researchers.

More about my PhD is available here.

Talks

• Vaccine Semantics – Automatic Methods for Recognizing, Representing, and Reasoning about Vaccine-related Information. (PhD defence, 2019, slides)

Web technology is interesting from two points of view: First, there are the underlying technological challenges. A web application runs in different tiers (the browser client, the server program, the database backends, …) in very different technical contexts and requirements, but to create a coherent application these tiers have to be integrated closely. On the other side, web development is one of the most useful programming technologies available, because it everybody uses it: to find information and to run software. I've been working between the two sides by contributing to the Eliom web framework, among others, a simplified interaction between client and server code, and by implementing a number of web applications.

---

Here is my CV.

• CoLiS language: Target language for the verification of Shell scripts by symbolic execution
• CodeMapper: Semi-automatic coding of medical case definitions
• VaccO: An ontology of vaccine descriptions with an application to code alignment
• Brighton ABC tool: Automatic classification of vaccine adverse events
• EasyOCaml: More descriptive error messages for OCaml by constraint-based type checking
• see also https://github.com/benozol

• Explaining Counterexamples with Giant-Step Assertion Checking. (link)
  Benedikt Becker, Cláudio Belo Lourenço, Claude Marché.
  F-IDE, 2021.
• Analysing installation scenarios of Debian packages. (link)
  Benedikt Becker, Nicolas Jeannerod, Claude Marché, Yann Régis-Gianas, Mihaela Sighireanu and Ralf Treinen.
  TACAS, 2020.
• Ghost Code in Action: Automated Verification of a Symbolic Interpreter. (link)
  Benedikt Becker, Claude Marché.
  VSTTE, 2019.
• Quantifying outcome misclassification in multi-database studies: The case study of pertussis in the ADVANCE project. (link)
  Rosa Ginia, Caitlin Dodd, Kaatje Bollaerts, Claudia Bartolini, Giuseppe Roberto, Consuelo Huerta-Alvarez, Elisa Martín-Merino, Talita Duarte-Salles, Gino Picelli, Lara Tramontan, Giorgia Danieli, Ana Correa, Chris McGee, Benedikt Becker, Charlotte Switzer, Sonja Gandhi-Banga, Jorgen Bauwens, Nicoline van der Maas, Gianfranco Spiteri, Emmanouela Sdona, Daniel Weibel, Miriam Sturkenboom.
  Vaccine, 2019.
• Masking by vaccines in pediatric drug safety signal detection in the EudraVigilance database. (link)
  C Dodd, A Pacurariu, O Osokogu, D Weibel, C Ferrajolo, D Vo, B Becker, J Kors, M Sturkenboom.
  Pharmacoepidemiology and drug safety, 2019.
• Alignment of vaccine codes using an ontology of vaccine descriptions. (link)
  Benedikt Becker, Jan Kors, Erik Mulligen, Miriam Sturkenboom.
  Journal of Biomedical Semantics, 2022.
• Identification and normalization of vaccine descriptions in scientific literature.
  Benedikt Becker, Miriam Sturkenboom, Jan Kors.
  Submitted, 2018.
• CodeMapper: semiautomatic coding of medical case definitions. (link)
  Benedikt Becker, Paul Avillach, Silvana Romio, Erik Mulligen, Daniel Weibel, Miriam Sturkenboom, Jan Kors.
  Pharmacoepidemiology and drug safety, 2017.
• Extraction of chemical-induced diseases using prior knowledge and textual information. (link)
  Ewoud Pons + Benedikt Becker, Saber Akhondi, Zubair Afzal, Erik Van Mulligen, Jan Kors.
  Database, 2016.
• Evaluation of a multinational, multilingual vaccine debate on Twitter. (link)
  Benedikt Becker, Heidi Larson, Jan Bonhoeffer, Erik Van Mulligen, Jan Kors, Miriam Sturkenboom.
  Vaccine, 2016.
• Evaluating social media networks in medicines safety surveillance: two case studies. (link)
  Preciosa Coloma, Benedikt Becker, Miriam Sturkenboom, Erik van Mulligen, Jan Kors.
  Drug safety, 2015.
• Preferences in Cardinal Direction. (link)
  Marco Ragni, Benedikt Becker.
  Proceedings of the Cognitive Science Society, 2010.

Pages are published from Emacs' org-mode with tufte-css.