Courses

Formal Proofs of Mathematical Theorems Thaynara Arielly Lima (UFG - Brazil), Mauricio Ayala-Rincón (UnB - Brazil)

Despite the fact that the acceptance of a mathematical truth will always depend on humans, nowadays finding mathematicians working with machines to produce formal proofs is no longer seen as an innovation but as a well-practice of modern mathematical proving. The course will present "deduction" and "proof theory" in the practice to researchers (in any level) using the proof assistant PVS. Participants will "put their hands in the dough" receiving a basic training to understand how to prove mathematical theorems using such powerful tools.

Modeling Cyberphysical Agents in Maude Carolyn Talcott (SRI International - USA)

Cyberphysical agents (CPAs) play many important roles in agriculture, critical infrastructure surveillance, logistics, manufacturing, disaster recovery, ... . CPAs are autonomous to some degree, and operate in unpredictable, possibly hostile, environments. Thus they must be robust and adapt to change and obstacles to progress. In this course we will present the Soft Agent Framework, a formal framework in Maude for exploration of CPA system designs. We will show how the framework can be used to design and execute scenarios, explore effects of faults and obstacles, carry out reachability analysis, and statistical model checking to better understand limits of agents ability to adapt. CPA models are modular and we will show how the Maude representation of the physics can be replaced by a simulator either for execution or statistical model checking.

Modelling and Verifying Cyber-Physical Security Protocols Vivek Nigam (Fortiss - Germany)

Emerging technologies, such as RFID based credit cards, passports, contactless keys, enable users to rapidly access resources without the need for physical contact between devices. These applications have also been target to attacks that may cause financial losses or inflict privacy problems to users. For example, attackers have been able to access vehicles and misuse credit cards without possessing a vehicle key nor the targeted credit card. To mitigate these attacks, cyber-physical security protocols have been developed that when completed establish properties such as authenticity and confidentiality, as in usual security protocols, and additionally establish physical properties, such as bounds on the distance between protocol participants. During this tutorial, we will review some of the challenges in designing cyber-physical security protocols, and how formal methods based on rewriting logic can be used to verify the security of protocol against many known attacks.