Sign in
Robby
Publication Activity (10 Years)
Years Active: 2000-2023
Publications (10 Years): 13
Top Topics
Systems Engineering
Code Generation
Flow Analysis
Programming Language
Top Venues
ISoLA
ISoLA (1)
HILT
Innov. Syst. Softw. Eng.
</>
Publications
</>
John Hatcliff
,
Jason Belt
,
Robby
,
Jacob Legg
,
Danielle Stewart
,
Todd Carpenter
Automated Property-Based Testing from AADL Component Contracts.
FMICS
(2023)
Jason Belt
,
John Hatcliff
,
Robby
,
John Shackleton
,
Jim Carciofini
,
Todd Carpenter
,
Eric Mercer
,
Isaac Amundson
,
Junaid Babar
,
Darren D. Cofer
,
David S. Hardin
,
Karl Hoech
,
Konrad Slind
,
Ihor Kuz
,
Kent McLeod
Model-driven development for the seL4 microkernel using the HAMR framework.
J. Syst. Archit.
134 (2023)
Darren D. Cofer
,
Isaac Amundson
,
Junaid Babar
,
David S. Hardin
,
Konrad Slind
,
Perry Alexander
,
John Hatcliff
,
Robby
,
Gerwin Klein
,
Corey Lewis
,
Eric Mercer
,
John Shackleton
Cyberassured Systems Engineering at Scale.
IEEE Secur. Priv.
20 (3) (2022)
Hariharan Thiagarajan
,
John Hatcliff
,
Robby
Awas: AADL information flow and error propagation analysis framework.
Innov. Syst. Softw. Eng.
18 (4) (2022)
John Hatcliff
,
Jason Belt
,
Robby
,
Todd Carpenter
HAMR: An AADL Multi-platform Code Generation Toolset.
ISoLA
(2021)
Robby
,
John Hatcliff
Slang: The Sireum Programming Language.
ISoLA
(2021)
Hariharan Thiagarajan
,
John Hatcliff
,
Robby
Awas: AADL Information Flow and Error Propagation Analysis Framework.
ECSA Companion
(2020)
Fengguo Wei
,
Sankardas Roy
,
Xinming Ou
,
Robby
Amandroid: A Precise and General Inter-component Data Flow Analysis Framework for Security Vetting of Android Apps.
ACM Trans. Priv. Secur.
21 (3) (2018)
John Hatcliff
,
Brian R. Larson
,
Jason Belt
,
Robby
,
Yi Zhang
A Unified Approach for Modeling, Developing, and Assuring Critical Systems.
ISoLA (1)
(2018)
Robby
,
John Hatcliff
,
Jason Belt
Model-Based Development for High-Assurance Embedded Systems.
ISoLA (1)
(2018)
Zhi Zhang
,
Robby
,
John Hatcliff
,
Yannick Moy
,
Pierre Courtieu
Focused Certification of an Industrial Compilation and Static Verification Toolchain.
SEFM
(2017)
Venkatesh-Prasad Ranganath
,
Yu Jin Kim
,
John Hatcliff
,
Robby
Communication patterns for interconnecting and composing medical systems.
EMBC
(2015)
Yu Jin Kim
,
Sam Procter
,
John Hatcliff
,
Venkatesh-Prasad Ranganath
,
Robby
Ecosphere Principles for Medical Application Platforms.
ICHI
(2015)
Fengguo Wei
,
Sankardas Roy
,
Xinming Ou
,
Robby
Amandroid: A Precise and General Inter-component Data Flow Analysis Framework for Security Vetting of Android Apps.
CCS
(2014)
Sam Procter
,
John Hatcliff
,
Robby
Towards an AADL-Based Definition of App Architecture for Medical Application Platforms.
FHIES/SEHC
(2014)
Pierre Courtieu
,
Maria-Virginia Aponte
,
Tristan Crolard
,
Zhi Zhang
,
Robby
,
Jason Belt
,
John Hatcliff
,
Jérôme Guitton
,
Trevor Jennings
Towards the formalization of SPARK 2014 semantics with explicit run-time checks using coq.
HILT
(2013)
Jooyong Yi
,
Robby
,
Xianghua Deng
,
Abhik Roychoudhury
Past expression: encapsulating pre-states at post-conditions by means of AOP.
AOSD
(2013)
John Hatcliff
,
Robby
,
Patrice Chalin
,
Jason Belt
Explicating symbolic execution (xSymExe): an evidence-based verification framework.
ICSE
(2013)
Xianghua Deng
,
Jooyong Lee
,
Robby
Efficient and formal generalized symbolic execution.
Autom. Softw. Eng.
19 (3) (2012)
Hariharan Thiagarajan
,
John Hatcliff
,
Jason Belt
,
Robby
Bakar Alir: Supporting Developers in Construction of Information Flow Contracts in SPARK.
SCAM
(2012)
Jason Belt
,
Patrice Chalin
,
John Hatcliff
,
Robby
Leading-edge Ada verification technologies: highly automated Ada contract checking using bakar kiasan.
HILT
(2012)
Jason Belt
,
Robby
,
Patrice Chalin
,
John Hatcliff
,
Xianghua Deng
Efficient Symbolic Execution of Value-Based Data Structures for Critical Systems.
NASA Formal Methods
(2012)
Jason Belt
,
John Hatcliff
,
Robby
,
Patrice Chalin
,
David S. Hardin
,
Xianghua Deng
Bakar Kiasan: Flexible Contract Checking for Critical Systems Using Symbolic Execution.
NASA Formal Methods
(2011)
Jason Belt
,
John Hatcliff
,
Robby
,
Patrice Chalin
,
David S. Hardin
,
Xianghua Deng
Enhancing spark's contract checking facilities using symbolic execution.
SIGAda
(2011)
Patrice Chalin
,
Robby
,
Perry R. James
,
Jooyong Lee
,
George Karabotsos
Towards an industrial grade IVE for Java and next generation research platform for JML.
Int. J. Softw. Tools Technol. Transf.
12 (6) (2010)
Scott J. Harmon
,
Scott A. DeLoach
,
Robby
From abstract qualities to concrete specification using guidance policies.
AAMAS (2)
(2009)
Scott J. Harmon
,
Scott A. DeLoach
,
Robby
Abstract Requirement Analysis in Multiagent System Design.
IAT
(2009)
Juan C. García-Ojeda
,
Scott A. DeLoach
,
Robby
agentTool III: from process definition to code generation.
AAMAS (2)
(2009)
Juan C. García-Ojeda
,
Scott A. DeLoach
,
Robby
agentTool process editor: supporting the design of tailored agent-based processes.
SAC
(2009)
Robby
,
Patrice Chalin
Preliminary design of a unified JML representation and software infrastructure.
FTfJP@ECOOP
(2009)
Jason Belt
,
Robby
,
Xianghua Deng
Sireum/Topi LDP: a lightweight semi-decision procedure for optimizing symbolic execution-based analyses.
ESEC/SIGSOFT FSE
(2009)
Torben Amtoft
,
John Hatcliff
,
Edwin Rodríguez
,
Robby
,
Jonathan Hoag
,
David A. Greve
Specification and Checking of Software Contracts for Conditional Information Flow.
FM
(2008)
Scott J. Harmon
,
Scott A. DeLoach
,
Robby
,
Doina Caragea
Leveraging Organizational Guidance Policies with Learning to Self-Tune Multiagent Systems.
SASO
(2008)
Juan C. García-Ojeda
,
Scott A. DeLoach
,
Robby
,
Walamitien H. Oyenan
,
Jorge L. Valenzuela
O-MaSE: A Customizable Approach to Developing Multiagent Development Processes.
AOSE
(2007)
Xianghua Deng
,
Robby
,
John Hatcliff
Towards A Case-Optimal Symbolic Execution Algorithm for Analyzing Strong Properties of Object-Oriented Programs.
SEFM
(2007)
Scott J. Harmon
,
Scott A. DeLoach
,
Robby
Trace-Based Specification of Law and Guidance Policies for Multi-Agent Systems.
ESAW
(2007)
Matthew B. Dwyer
,
John Hatcliff
,
Robby
,
Corina S. Pasareanu
,
Willem Visser
Formal Software Analysis Emerging Trends in Software Model Checking.
FOSE
(2007)
Robby
,
Edwin Rodríguez
,
Matthew B. Dwyer
,
John Hatcliff
Checking JML specifications using an extensible software model checking framework.
Int. J. Softw. Tools Technol. Transf.
8 (3) (2006)
Xianghua Deng
,
Robby
,
John Hatcliff
Kiasan: A Verification and Test-Case Generation Framework for Java Based on Symbolic Execution.
ISoLA
(2006)
Matthew B. Dwyer
,
John Hatcliff
,
Matthew Hoosier
,
Venkatesh Prasad Ranganath
,
Robby
,
Todd Wallentine
Evaluating the Effectiveness of Slicing for Model Reduction of Concurrent Object-Oriented Programs.
TACAS
(2006)
Robby
,
Matthew B. Dwyer
,
John Hatcliff
Domain-specific Model Checking Using The Bogor Framework.
ASE
(2006)
Robby
,
Scott A. DeLoach
,
Valeriy A. Kolesnikov
Using Design Metrics for Predicting System Flexibility.
FASE
(2006)
Robby
,
Matthew B. Dwyer
,
John Hatcliff
Bogor: A Flexible Framework for Creating Software Model Checkers.
TAIC PART
(2006)
Xianghua Deng
,
Jooyong Lee
,
Robby
Bogor/Kiasan: A k-bounded Symbolic Execution for Checking Strong Heap Properties of Open Systems.
ASE
(2006)
Edwin Rodríguez
,
Matthew B. Dwyer
,
Cormac Flanagan
,
John Hatcliff
,
Gary T. Leavens
,
Robby
Extending JML for Modular Specification and Verification of Multi-threaded Programs.
ECOOP
(2005)
Matthew B. Dwyer
,
John Hatcliff
,
Matthew Hoosier
,
Robby
Building Your Own Software Model Checker Using the Bogor Extensible Model Checking Framework.
CAV
(2005)
Matthew Hoosier
,
Matthew B. Dwyer
,
Robby
,
John Hatcliff
A Case Study in Domain-Customized Model Checking for Real-Time Component Software.
ISoLA
(2004)
Edwin Rodríguez
,
Matthew B. Dwyer
,
John Hatcliff
,
Robby
A Flexible Framework for the Estimation of Coverage Metrics in Explicit State Software Model Checking.
CASSIS
(2004)
John Hatcliff
,
Robby
,
Matthew B. Dwyer
Verifying Atomicity Specifications for Concurrent Object-Oriented Software Using Model-Checking.
VMCAI
(2004)
Robby
,
Edwin Rodríguez
,
Matthew B. Dwyer
,
John Hatcliff
Checking Strong Specifications Using an Extensible Software Model Checking Framework.
TACAS
(2004)
Matthew Hoosier
,
John Hatcliff
,
Robby
,
Matthew B. Dwyer
A Case Study in Domain-customized Model Checking for Real-time Component Software.
ISoLA (Preliminary proceedings)
(2004)
Matthew B. Dwyer
,
Robby
,
Oksana Tkachuk
,
Willem Visser
Analyzing Interaction Orderings with Model Checking.
ASE
(2004)
Matthew B. Dwyer
,
John Hatcliff
,
Robby
,
Venkatesh Prasad Ranganath
Exploiting Object Escape and Locking Information in Partial-Order Reductions for Concurrent Object-Oriented Programs.
Formal Methods Syst. Des.
25 (2-3) (2004)
Matthew B. Dwyer
,
Robby
,
Xianghua Deng
,
John Hatcliff
Space Reductions for Model Checking Quasi-Cyclic Systems.
EMSOFT
(2003)
John Hatcliff
,
William Deng
,
Matthew B. Dwyer
,
Georg Jung
,
Venkatesh Prasad Ranganath
,
Robby
Slicing and partial evaluation of CORBA component model designs for avionics system.
PEPM
(2003)
Robby
,
Matthew B. Dwyer
,
John Hatcliff
Bogor: an extensible and highly-modular software model checking framework.
ESEC / SIGSOFT FSE
(2003)
Robby
,
Matthew B. Dwyer
,
John Hatcliff
,
Radu Iosif
Space-Reduction Strategies for Model Checking Dynamic Software.
Electron. Notes Theor. Comput. Sci.
89 (3) (2003)
John Hatcliff
,
Matthew B. Dwyer
,
Corina S. Pasareanu
,
Robby
Foundations of the Bandera Abstraction Tools.
The Essence of Computation
(2002)
James C. Corbett
,
Matthew B. Dwyer
,
John Hatcliff
,
Robby
Expressing checkable properties of dynamic systems: the Bandera Specification Language.
Int. J. Softw. Tools Technol. Transf.
4 (1) (2002)
Xianghua Deng
,
Matthew B. Dwyer
,
John Hatcliff
,
Georg Jung
,
Robby
,
Gurdip Singh
Model-Checking Middleware-Based Event-Driven Real-Time Embedded Software.
FMCO
(2002)
Matthew B. Dwyer
,
John Hatcliff
,
Roby Joehanes
,
Shawn Laubach
,
Corina S. Pasareanu
,
Robby
,
Hongjun Zheng
,
Willem Visser
Tool-Supported Program Abstraction for Finite-State Verification.
ICSE
(2001)
James C. Corbett
,
Matthew B. Dwyer
,
John Hatcliff
,
Robby
A Language Framework for Expressing Checkable Properties of Dynamic Software.
SPIN
(2000)
James C. Corbett
,
Matthew B. Dwyer
,
John Hatcliff
,
Robby
Bandera: a source-level interface for model checking Java programs.
ICSE
(2000)
James C. Corbett
,
Matthew B. Dwyer
,
John Hatcliff
,
Shawn Laubach
,
Corina S. Pasareanu
,
Robby
,
Hongjun Zheng
Bandera: extracting finite-state models from Java source code.
ICSE
(2000)