3 citations · 5 across the 6 of their papers we have counts for
7 papers
FVSpec: Real-World Property-Based Tests as Lean Challenges
Quinn Dougherty, Max von Hippel, Simon Henniger +2
As AI systems generate an ever-growing share of the world's code, formal verification offers a principled way to ensure that code is correct, and AI itself may be able to shoulder…
A Formal Analysis of SCTP: Attack Synthesis and Patch Verification
Jacob Ginesin, Max von Hippel, Evan Defloor +2
SCTP is a transport protocol offering features such as multi-homing, multi-streaming, and message-oriented delivery. Its two main implementations were subjected to conformance test…
Verification of GossipSub in ACL2s
Ankit Kumar, Max von Hippel, Panagiotis Manolios +1
GossipSub is a popular new peer-to-peer network protocol designed to disseminate messages quickly and efficiently by allowing peers to forward the full content of messages only to…
A Case Study in Analytic Protocol Analysis in ACL2
Max von Hippel, Panagiotis Manolios, Kenneth L. McMillan +2
When verifying computer systems we sometimes want to study their asymptotic behaviors, i.e., how they behave in the long run. In such cases, we need real analysis, the area of math…
HoLA Robots: Mitigating Plan-Deviation Attacks in Multi-Robot Systems with Co-Observations and Horizon-Limiting Announcements
Kacper Wardega, Max von Hippel, Roberto Tron +2
Emerging multi-robot systems rely on cooperation between humans and robots, with robots following automatically generated motion plans to service application-level tasks. Given the…
Formal Model-Driven Analysis of Resilience of GossipSub to Attacks from Misbehaving Peers
Ankit Kumar, Max von Hippel, Pete Manolios +1
GossipSub is a new peer-to-peer communication protocol designed to counter attacks from misbehaving peers by controlling what information is sent and to whom, via a score function…
Automated Attacker Synthesis for Distributed Protocols
Max von Hippel, Cole Vick, Stavros Tripakis +1
Distributed protocols should be robust to both benign malfunction (e.g. packet loss or delay) and attacks (e.g. message replay) from internal or external adversaries. In this paper…