The aim is to certify and verify, as well, data intensive systems with the Coq proof assistant . The project is divided into three main lines:
In many areas of computing, techniques ranging from testing, formal modeling to full-blown verification have been successfully used to help programmers create reliable systems. For example, in processor development, automated theorem proving uncovers deep bugs in designs before they become costly errors in silicon; avionics developers use program analysis to verify critical safety properties of the embedded software running on airplanes; and operating system vendors have successfully used model checking to eliminate entire classes of bugs in device drivers. More recently, program verification and mechanization, based on proof assistants such as Coq or Isabelle have been intensively studied yielding very impressive results and highly reliable software that do exactly conform to their formal specification.
Surprisingly, until recently, data intensive management systems and applications and more generally, the data realm, have largely resisted analysis using formal techniques. Such a situation is quite astonishing as, with the advent of internet, data intensive applications are being used in various sensitive domains in which data integration and exchange preserving privacy and/or data reliability are critical.
Datacert interacts with
the DeepSpec Expedition project.
The aim is to certify and verify, as well, data intensive systems
with the Coq proof assistant .
The project is divided into three main lines:
We are seeking for students, (master, doctoral and post-doctoral) with an interest in (data-centric) programming languages and formal methods to work with us. Applicants should have, according to the position they apply for, a good, strong or very strong background in Coq. Contact us: datacert@lri.fr
The work will be pursued within the VALS research group of LRI lab in Paris Sud (batiment 650). The VALS group is a world-wide recognised research team in the area of Verification and Validation of Algorithms, Languages and Systems, right in the heart of the scientific field called "Formal Methods". The applicant will be co-advised by Dr., Th. Balabonski, Prof., V. Benzaken and Dr., E. Contejean.
