85 citations · 354 across the 71 of their papers we have counts for
6 papers · 1 filter
FAR-Cubicle - A new reachability algorithm for Cubicle
Sylvain Conchon, Amit Goel, Sava Krstic +2
We present a fully automatic algorithm for verifying safety properties of parameterized software systems. This algorithm is based on both IC3 and Lazy Annotation. We implemented it…
Verification of Immediate Observation Population Protocols
Javier Esparza, Pierre Ganty, Rupak Majumdar +1
Population protocols (Angluin et al., PODC, 2004) are a formal model of sensor networks consisting of identical mobile devices. Two devices can interact and thereby change their st…
Quadratic Word Equations with Length Constraints, Counter Systems, and Presburger Arithmetic with Divisibility
Anthony W. Lin, Rupak Majumdar
Word equations are a crucial element in the theoretical foundation of constraint solving over strings, which have received a lot of attention in recent years. A word equation relat…
Lazy Abstraction-Based Controller Synthesis
Kyle Hsu, Rupak Majumdar, Kaushik Mallik +1
We present lazy abstraction-based controller synthesis (ABCS) for continuous-time nonlinear dynamical systems against reach-avoid and safety specifications. State-of-the-art multi-…
Lazy Abstraction-Based Control for Safety Specifications
Kyle Hsu, Rupak Majumdar, Kaushik Mallik +1
We present a lazy version of multi-layered abstraction-based controller synthesis (ABCS) for continuous-time nonlinear dynamical systems against safety specifications. State-of-the…
Precise but Natural Specification for Robot Tasks
Ivan Gavran, Brendon Boldt, Eva Darulova +1
We present Flipper, a natural language interface for describing high-level task specifications for robots that are compiled into robot actions. Flipper starts with a formal core la…