| 2025 | MODELSWARD | LLFSMs to TLA+: A Model-to-Text Transformation of Executable Models Enabling Specification and Verification of Multi-Threaded and Concurrent Systems. | Vladimir Estivill-Castro, Miguel Carrillo, David A. Rosenblueth |
| 2025 | MODELSWARD | Efficient Modelling with Logic-Labelled Finite-State Machines of IEC 61499 Function Blocks: Simulation, Execution and Verification. | Vladimir Estivill-Castro, Miguel Carrillo, David A. Rosenblueth |
| 2020 | MODELSWARD | Model-to-Model Transformations for Efficient Time-domain Verification of Concurrent Models by NuSMV Modules. | Miguel Carrillo, Vladimir Estivill-Castro, David A. Rosenblueth |
| 2020 | MODELSWARD | Verification and Simulation of Time-Domain Properties for Models of Behaviour. | Miguel Carrillo, Vladimir Estivill-Castro, David A. Rosenblueth |
| 2016 | CONCUR | Decentralized Asynchronous Crash-Resilient Runtime Verification. | Borzoo Bonakdarpour, Pierre Fraigniaud, Sergio Rajsbaum, David A. Rosenblueth, Corentin Travers |
| 2015 | ATVA | Marimba: A Tool for Verifying Properties of Hidden Markov Models. | No Hernndez, Kerstin Eder, Evgeni Magid, Jess Savage, David A. Rosenblueth |
| 2013 | CEC | The dynamically extended mind. | Tom Froese, Carlos Gershenson, David A. Rosenblueth |
| 2012 | APSEC | Efficient Modelling of Embedded Software Systems and their Formal Verification. | Vladimir Estivill-Castro, Ren Hexel, David A. Rosenblueth |
| 2011 | ATVA | Nondeterministic Update of CTL Models by Preserving Satisfaction through Protections. | Miguel Carrillo, David A. Rosenblueth |
| 2005 | IJCAI | Incorporating a folding rule into inductive logic programming. | David A. Rosenblueth |
| 2003 | ICLP | A Distinct-Head Folding Rule. | David A. Rosenblueth |
| 2001 | PPDP | Development Reuse and the Logic Program Derivation of Two String-Matching Algorithms. | Manuel Hernndez, David A. Rosenblueth |
| 1998 | LOPSTR | An Exhaustive-Search Method Using Layered Streams Obtained Through a Meta-Interpreter for Chain Programs. | David A. Rosenblueth |