Modelling and Verifying Properties of Biological Neural Networks (Invited Talk)

Author Amy Felty

Thumbnail PDF


  • Filesize: 416 kB
  • 2 pages

Document Identifiers

Author Details

Amy Felty
  • School of Electrical Engineering and Computer Science, University of Ottawa, Canada

Cite AsGet BibTex

Amy Felty. Modelling and Verifying Properties of Biological Neural Networks (Invited Talk). In 13th International Conference on Interactive Theorem Proving (ITP 2022). Leibniz International Proceedings in Informatics (LIPIcs), Volume 237, pp. 1:1-1:2, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2022)


In this talk, I present a formal model of biological neural networks and discuss the use of model checking and interactive theorem proving to verify some of their properties. Having a formal model can increase our understanding of the behavior and properties of such networks, as well as provide insight into their response to external factors such as disease, medicine, and environmental changes. We focus on neuronal micro-networks, considering properties of single neurons as well as properties of slightly larger ones called archetypes, which represent specific computational functions. Archetypes, in turn, represent the building blocks of larger more complicated neuronal circuits. I first present work by colleagues on a model checking approach, and then present our joint work on a newer theorem proving approach. Using interactive theorem proving allows us to generalize the kinds of properties that we can prove. This work is joint with Abdorrahim Bahrami and Elisabetta De Maria.

Subject Classification

ACM Subject Classification
  • Theory of computation → Logic and verification
  • Applied computing → Systems biology
  • Neuronal networks
  • Model checking
  • Theorem proving
  • Coq


  • Access Statistics
  • Total Accesses (updated on a weekly basis)
    PDF Downloads


  1. Abdorrahim Bahrami, Elisabetta De Maria, and Amy Felty. Modelling and verifying dynamic properties of biological neural networks in Coq. In Ninth International Conference on Computational Systems-Biology and Bioinformatics (CSBio), pages 12:1-12:11, 2018. Google Scholar
  2. Yves Bertot and Pierre Castéran. Interactive Theorem Proving and Program Development-Coq'Art: The Calculus of Inductive Constructions. Springer, 2004. Google Scholar
  3. Wulfram Gerstner and Werner M. Kistler. Spiking Neuron Models: Single Neurons, Populations, Plasticity. Cambridge University Press, 2002. Google Scholar
  4. George Hagen and Cesare Tinelli. Scaling up the formal verification of Lustre programs with SMT-based techniques. In 2008 Formal Methods in Computer-Aided Design (FMCAD), pages 1-9, 2008. Google Scholar
  5. Elisabetta De Maria, Abdorrahim Bahrami, Thibaud L'Yvonnet, Amy Felty, Daniel Gaffé, Annie Ressouche, and Franck Grammont. On the use of formal methods to model and verify neuronal archetypes. Frontiers of Computer Science, 16(3), 2022. Article No: 163404. Google Scholar
  6. Elisabetta De Maria, Joëlle Despeyroux, Amy Felty, Pietro Lió, Carlos Olarte, and Abdorrahim Bahrami. Computational logic for biomedicine and neurosciences. To appear as a chapter in an ISTE-Wiley book, 2020. Google Scholar
  7. Elisabetta De Maria, Thibaud L'Yvonnet, Daniel Gaffé, Annie Ressouche, and Franck Grammont. Modelling and formal verification of neuronal archetypes coupling. In Eighth International Conference on Computational Systems-Biology and Bioinformatics (CSBio), pages 3-10, 2017. Google Scholar
  8. Elisabetta De Maria, Alexandre Muzy, Daniel Gaffé, Annie Ressouche, and Franck Grammont. Verification of temporal properties of neuronal archetypes modeled as synchronous reactive systems. In Fifth International Workshop on Hybrid Systems Biology (HSB), pages 97-112, 2016. Google Scholar
Questions / Remarks / Feedback

Feedback for Dagstuhl Publishing

Thanks for your feedback!

Feedback submitted

Could not send message

Please try again later or send an E-mail