Modelling and Verifying Dynamic Properties of Biological Neural Networks in Coq

Formal verification involves with proving properties about a system to make sure that the system is not free of bugs. There are two main methods for verification which are called model checking and theorem proving. Most current approaches to systems biology rely on model checking. Model checking is more automatic but not as general and often must rely on special values and cases. Theorem provers can verify models for arbitrary size, input, and time. In our approach, we use Coq proof assistant to create and verify a model of neural networks. Verifying biological system is a new field of research. A biological system can be from a single cell to whole body of a live creature. Most research in this field focuses on a particular organ. Our research is based on providing a general verified model for human neural networks using Coq proof assistant. TO BE CONT’D

Faculty Supervisor:

Amy Felty

Student:

Partner:

Université Nice Sophia Antipolis

Discipline:

Computer science

Sector:

Education

University:

University of Ottawa

Program: