4 papers
Less Manual Work for Safety Engineers: Towards an Automated Safety Reasoning with Safety Patterns
Yuri Gil Dantas, Antoaneta Kondeva, Vivek Nigam
The development of safety-critical systems requires the control of hazards that can potentially cause harm. To this end, safety engineers rely during the development phase on archi…
On the Accuracy of Formal Verification of Selective Defenses for TDoS Attacks
Marcilio O. O. Lemos, Yuri Gil Dantas, Iguatemi E. Fonseca +1
Telephony Denial of Service (TDoS) attacks target telephony services, such as Voice over IP (VoIP), not allowing legitimate users to make calls. There are few defenses that attempt…
Towards the Automated Verification of Cyber-Physical Security Protocols: Bounding the Number of Timed Intruders
Vivek Nigam, Carolyn Talcott, Abraão Aires Urquiza
Timed Intruder Models have been proposed for the verification of Cyber-Physical Security Protocols (CPSP) amending the traditional Dolev-Yao intruder to obey the physical restricti…
Abstract Effects and Proof-Relevant Logical Relations
Nick Benton, Martin Hofmann, Vivek Nigam
We introduce a novel variant of logical relations that maps types not merely to partial equivalence relations on values, as is commonly done, but rather to a proof-relevant general…