In the last two decades, formal verification and analysis of engineering systems have been widely considered in academia and industry. This results in the availability of more sophisticated proof assistants (e.g., HOL Light, Coq, Isabelle/HOL and Mizar) and large formalization of mathematical theories (e.g., multivariate analysis, linear algebra, etc.). Recently, significant amount of work has been reported describing the prospects of using artificial intelligence (AI) and machine learning techniques to provide better management of large formalized theories and powerful proof automation. In this workshop, we aim at discussing two main research directions: 1) motivation and state-of-the-art related to the formalization of Physics (particularly Optics). 2) Applying already developed AI techniques to the formalization of Physics.

Workshop Program

DATE | Time	Description
25 August 2014
14:00-14:15	Introduction to Hardware Verification Group (HVG) Research (Prof. Sofiene Tahar)
14:15-14:30	Introduction to Formal Math and Interest in Formal Physics (Dr. Josef Urban)
14:30-14:45	Formalization of Ray Optics (Umair Siddique)
14:45-15:00	Formalization of Electromagnetic Optics (Sanaz Khan-Afshar)
15:00-15:30	Interactive Proofs, Computer Algebra, Automation and Presentation (Dr. Cezary Kaliszyk)
15:30-16:00	Tea/Coffee Break
16:00-18:00	Discussions
26 August 2014
14:00-14:15	Formalization of Quantum Optics (Umair Siddique)
14:15-14:30	Linking HOL Light and Mathematica using OpenMath (Ons Seddiki)
14:30-15:00	Automating and Presenting Formal Proofs and Formal Physics (Dr. Josef Urban)
15:30-16:00	Discussions and Brainstorming
16:00-16:30	Tea/Coffee Break
16:30-18:00	Discussions
18:00-21:00	Code/Tool Demonstration
28 August 2014
10:00-11:30	Brunch with Prof. Tahar
11:30-13:00	Collobration and Concrete Future Directions

Workshop Organizers

Sanaz Khan-Afshar
Umair Siddique

Pictures