10 citations · 12 across the 7 of their papers we have counts for
8 papers
FASR: Automated Identification of Unsafe Control Actions in STPA
Ian Dardik, Yining She, Sam Procter +3
The System-Theoretic Process Analysis (STPA) is a well-established hazard analysis technique that has been applied to a wide range of safety-critical systems. Despite its popularit…
Compositional Inductive Invariant Inference via Assume-Guarantee Reasoning
Ian Dardik, Eunsuk Kang
A common technique for verifying the safety of complex systems is the inductive invariant method. Inductive invariants are inductive formulas that overapproximate the reachable sta…
Constrained LTL Specification Learning from Examples
Changjian Zhang, Parv Kapoor, Ian Dardik +4
Temporal logic specifications play an important role in a wide range of software analysis tasks, such as model checking, automated synthesis, program comprehension, and runtime mon…
Recomposition: A New Technique for Efficient Compositional Verification
Ian Dardik, April Porter, Eunsuk Kang
Compositional verification algorithms are well-studied in the context of model checking. Properly selecting components for verification is important for efficiency, yet has receive…
Safe Environmental Envelopes of Discrete Systems
Rômulo Meira-Góes, Ian Dardik, Eunsuk Kang +2
A safety verification task involves verifying a system against a desired safety property under certain assumptions about the environment. However, these environmental assumptions m…
Plain and Simple Inductive Invariant Inference for Distributed Protocols in TLA+
William Schultz, Ian Dardik, Stavros Tripakis
We present a new technique for automatically inferring inductive invariants of parameterized distributed protocols specified in TLA+. Ours is the first such invariant inference tec…
Formal Verification of a Distributed Dynamic Reconfiguration Protocol
William Schultz, Ian Dardik, Stavros Tripakis
We present a formal, machine checked TLA+ safety proof of MongoRaftReconfig, a distributed dynamic reconfiguration protocol. MongoRaftReconfig was designed for and implemented in M…
Design and Analysis of a Logless Dynamic Reconfiguration Protocol
William Schultz, Siyuan Zhou, Ian Dardik +1
Distributed replication systems based on the replicated state machine model have become ubiquitous as the foundation of modern database systems. To ensure availability in the prese…