Demo Data from SIGIR 2026 / reviewers in the wild / expert
Michael McDougall
dblp:17/6749
· DBLP profile ↗
5ranked-venue papers
1as first author
1since 2021 · last 2023
—ORCID · unresolved
Domains — the database's venue-derived domains; a paper can count in several
Systems, architecture and hardware · 2 · 1 since 2021Software engineering, systems software and programming languages · 2Theory of computation · 2Artificial intelligence and machine learning · 1 · 1 since 2021Applied, interdisciplinary, general and emerging computing · 1 · 1 first-author
Expertise — from the expertise taxonomy: the topics of the expert's papers under the CCF categories. A weight counts papers with recency: 1 for a paper about the topic, 0.3 when the topic is its context, halved every five years.
| Software engineering, system software, and programming languages
2 papers |
Program verification · 100% | |
| Theoretical computer science
2 papers |
Automated reasoning and model checking · 70% Automata and formal languages · 30% |
Topics — the 6 heaviest of 6, each with the papers that count most for it
| Topic | Weight | Papers | Last | Evidence papers |
|---|---|---|---|---|
Program verification › model checking
state space reduction |
0.0 | 1 | 2002 | Exploiting Behavioral Hierarchy for Efficient Model Checking · CAV 2002 |
Automated reasoning and model checking
model checking |
0.0 | 1 | 2002 | Exploiting Behavioral Hierarchy for Efficient Model Checking · CAV 2002 |
Program verification
model checking |
0.0 | 1 | 2000 | Efficient Reachability Analysis of Hierarchical Reactive Machines · CAV 2000 |
Program verification › model checking
state space exploration |
0.0 | 1 | 2000 | Efficient Reachability Analysis of Hierarchical Reactive Machines · CAV 2000 |
Automata and formal languages › finite automata
hierarchical state machines |
0.0 | 1 | 2000 | Efficient Reachability Analysis of Hierarchical Reactive Machines · CAV 2000 |
Automated reasoning and model checking
reachability |
0.0 | 1 | 2000 | Efficient Reachability Analysis of Hierarchical Reactive Machines · CAV 2000 |
Methods — techniques the papers use, named apart from their topics
symbolic model checking · 0.1
| Year | Publication | Venue | Position |
|---|---|---|---|
| 2023 | Multi-Gait Locomotion Planning and Tracking for Tendon-Actuated Terrestrial Soft Robot (TerreSoRo)abstractThe adaptability of soft robots makes them ideal candidates to maneuver through unstructured environments. However, locomotion challenges arise due to complexities in modeling the body mechanics, actuation, and robot-environment dynamics. These factors contribute to the gap between their potential and actual autonomous field deployment. A closed-loop path planning framework for soft robot locomotion is critical to close the real-world realization gap. This paper presents a generic path planning framework applied to TerreSoRo (Tetra-Limb Terrestrial Soft Robot) with pose feedback. It employs a gait-based, lattice trajectory planner to facilitate navigation in the presence of obstacles. The locomotion gaits are synthesized using a data-driven optimization approach that allows for learning from the environment. The trajectory planner employs a greedy breadth-first search strategy to obtain a collision-free trajectory. The synthesized trajectory is a sequence of rotate-then-translate gait pairs. The control architecture integrates high-level and low-level controllers with real-time localization (using an overhead webcam). Terre-SoRo successfully navigates environments with obstacles where path re-planning is performed. To best of our knowledge, this is the first instance of real-time, closed-loop path planning of a non-pneumatic soft robot. Arun Niddish Mahendran, Caitlin Freeman, Alexander H. Chang, Michael McDougall, Patricio A. Vela, Vishesh Vikas |
IROS | 4 |
| 2004 | A model-based approach to integrating security policies for embedded devicesabstractEmbedded devices like smartcards can now run multiple interacting applications. A particular challenge in this domain is to dynamically integrate diverse security policies. In this paper we show how a framework based on a concise formal model lets us securely customize a payment card equipped with a programmable chip. We present policy automata, a formal model of computations that grant or deny access to a resource. This model combines defeasible logic with state machines, representing complex policies as combinations of simpler modular policies. We use the model in a framework for specifying, merging and analyzing modular policies. This framework is implemented as Polaris, a tool which analyzes policy automata to reveal potential conflicts or redundancies, and compiles automata into Java Card applets. Michael McDougall, Rajeev Alur, Carl A. Gunter |
EMSOFT | 1 |
| 2002 | Predictable programs in barcodesabstractWe explore the challenges for making the programming interfaces for embedded devices open and safe, and present a prototype architecture for delivering verified programs using barcodes. In particular, we consider programs for microwave ovens, which provide a basic open API for controlling cooking times. In our architecture, recipes are written in Java, and their safety properties are formally verified using the model checker Spin. We use off-the-shelf utilities for compressing the byte code, and use two-dimensional barcodes for program delivery. We report on experiments that demonstrate the feasibility of the proposed architecture for predictability and delivery. Alwyn Goodloe, Michael McDougall, Carl A. Gunter, Rajeev Alur |
CASES | 2 |
| 2002 | Exploiting Behavioral Hierarchy for Efficient Model Checking
Rajeev Alur, Michael McDougall, Zijiang Yang 0006 |
CAV | 2 |
| 2000 | Efficient Reachability Analysis of Hierarchical Reactive Machines
Rajeev Alur, Radu Grosu, Michael McDougall |
CAV | 3 |