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:
The project is co-located between CRIStAL at Lille, LIRIS at Lyon and and LRI at Orsay.