An Implementation of OSI Management Q3 Agent Platform for Subscriber Networks. - Toshio Tonouchi; Takashi Fukushima; Asuka Manki; Shin Nakajima 001 (ICC (2), 1997)

An Object-Oriented Modeling Method for Algebraic Specifications in CafeOBJ. - Shin Nakajima 001; Kokichi Futatsugi (ICSE, 1997)

Using Algebraic Specification Techniques in Development of Object-Oriented Frameworks. - Shin Nakajima 001 (World Congress on Formal Methods, 1999)

A Directory Server for Mobile Agents Interoperability. - Yasuyuki Beppu; Shin Nakajima 001; Fumihiro Kumeno; Kenta Cho 001; Tetsuo Hasegawa; Akihiko Ohsuga (EDOC, 2000)

Behavioural Analysis of the Enterprise JavaBeansTM Component Architecture. - Shin Nakajima 001; Tetsuo Tamai (SPIN, 2001)

Behavioural Analysis of Component Framework with Multi-Valued Transition System. - Shin Nakajima 001 (APSEC, 2002)

Verification of Web Service Flows with Model-Checking Techniques. - Shin Nakajima 001 (CW, 2002)

Interoperability for mobile agents by incarnation agents. - Tetsuo Hasegawa; Kenta Cho 001; Fumihiro Kumeno; Shin Nakajima 001; Akihiko Ohsuga; Shinichi Honiden (AAMAS, 2003)

Model-Checking of Safety and Security Aspects in Web Service Flows. - Shin Nakajima 001 (ICWE, 2004)

Project Report: High-Reliable Object-Oriented Embedded Software Design. - Tomoji Kishi; Toshiaki Aoki; Shin Nakajima 001; Natsuko Noda; Takuya Katayama (WSTFEUS, 2004)

Model-Checking Behavioral Specification of BPEL Applications. - Shin Nakajima 001 (WLFM@FM, 2005)

Highly Reliable Embedded Software Development Using Advanced Software Technologies. - Takuya Katayama; Tatsuo Nakajima; Taiichi Yuasa; Tomoji Kishi; Shin Nakajima 001; Shuichi Oikawa; Masahiro Yasugi; Toshiaki Aoki; Mitsutaka Okazaki; Seiji Umatani (IEICE Trans. Inf. Syst., 2005)

Formal specification and analysis of JAAS framework. - Shin Nakajima 001; Tetsuo Tamai (SESS@ICSE, 2006)

Aspect-oriented software design with a variant of UML/STD. - Shin Nakajima 001; Tetsuo Tamai (SCESM, 2006)

Context-aware feature-oriented modeling with an aspect extension of VDM. - Naoyasu Ubayashi; Shin Nakajima 001 (SAC, 2007)

Aspect-Oriented Programming for Web Controller Layer. - Keiji Hokamura; Naoyasu Ubayashi; Shin Nakajima 001; Akihito Iwai (APSEC, 2008)

Modular Checking of C Programs Using SAT-Based Bounded Model Checker. - Yuusuke Hashimoto; Shin Nakajima 001 (APSEC, 2009)

Runtime monitoring of cross-cutting policy. - Shin Nakajima 001; Naoyasu Ubayashi; Keiji Hokamura (EA@ICSE, 2009)

AOWP: Web-Specific AOP Framework for PHP. - Keiji Hokamura; Ryoto Naruse; Masaru Shiozuka; Naoyasu Ubayashi; Shin Nakajima 001; Akihito Iwai (ASE, 2009)

Integration of formal specification, review, and testing for software component quality assurance. - Shaoying Liu; Tetsuo Tamai; Shin Nakajima 001 (SAC, 2009)

Constructing FODA Feature Diagrams with a GUI-based Tool. - Shin Nakajima 001 (SEKE, 2009)

Modular Checking with Model Checking. - Yuusuke Hashimoto; Shin Nakajima 001 (SSV, 2009)

Aspect-Oriented Development of PHP-Based Web Applications. - Shin Nakajima 001; Keiji Hokamura; Naoyasu Ubayashi (COMPSAC Workshops, 2010)

Semi-automated diagnosis of FODA feature diagram. - Shin Nakajima 001 (SAC, 2010)

Structured Counterexamples for the Temporal Description Logic ALCCTL. - Franz Weitl; Shin Nakajima 001; Burkhard Freitag (SEFM, 2010)

Rewriting Logic Approach to Modeling and Analysis of Client Behavior in Open Systems. - Shin Nakajima 001; Masaki Ishiguro; Kazuyuki Tanaka (SEUS, 2010)

Automatic Transformation from Formal Specifications to Functional Scenario Forms for Automatic Test Case Generation. - Shaoying Liu; Toshinori Hayashi; Kazuhiro Takahashi; Koichiro Kimura; Toshihiro Nakayama; Shin Nakajima 001 (SoMeT, 2010)

Non-clausal Encoding of Feature Diagram for Automated Diagnosis. - Shin Nakajima 001 (SPLC, 2010)

Context-Dependent Product Line Practice for Constructing Reliable Embedded Systems. - Naoyasu Ubayashi; Shin Nakajima 001; Masayuki Hirayama (SPLC, 2010)

A Decompositional Approach to Automatic Test Case Generation Based on Formal Specifications. - Shaoying Liu; Shin Nakajima 001 (SSIRI, 2010)

Incremental Construction of Counterexamples in Model Checking Web Documents. - Franz Weitl; Shin Nakajima 001 (WWV, 2010)

From Counterexamples to Incremental Interactive Tracing of Errors (Schrittweise Fehleranalyse auf der Grundlage von Model-Checking). - Franz Weitl; Shin Nakajima 001; Burkhard Freitag (it Inf. Technol., 2010)

A "Vibration" Method for Automatically Generating Test Cases Based on Formal Specifications. - Shaoying Liu; Shin Nakajima 001 (APSEC, 2011)

An Architecture of Dynamically Adaptive PHP-based Web Applications. - Shin Nakajima 001 (APSEC, 2011)

A framework for automatic functional testing based on formal specifications. - Shaoying Liu; Shin Nakajima 001 (AST, 2011)

Utilizing Model Checking for Automatic Test Case Generation from Conjunctions of Predicates. - Cong Tian; Shaoying Liu; Shin Nakajima 001 (ICST Workshops, 2011)

Translation Pattern of BPEL Process into Promela Code. - Ryosuke Nakashiro; Yasutaka Kamei; Naoyasu Ubayashi; Shin Nakajima 001; Akihito Iwai (IWSM/Mensura, 2011)

Integrated Model Checking of Static Structure and Dynamic Behavior using Temporal Description Logics. - Franz Weitl; Shin Nakajima 001 (Electron. Commun. Eur. Assoc. Softw. Sci. Technol., 2011)

A Framework for Integrating Formal Specification, Review, and Testing to Enhance Software Reliability. - Shaoying Liu; Tetsuo Tamai; Shin Nakajima 001 (Int. J. Softw. Eng. Knowl. Eng., 2011)

Importance Sampling of Runtime Interference. - Shin Nakajima 001 (APSEC, 2012)

Co-analysis of SysML and Simulink Models for Cyber-Physical Systems Design. - Shin Nakajima 001; Satoru Furukawa; Yoshikazu Ueda (RTCSA, 2012)

Applying "Functional Scenario-Based" Test Case Generation Method in Unit Testing and Integration Testing. - Cencen Li; Mo Li 003; Shaoying Liu; Shin Nakajima 001 (SOFL, 2012)

A formal approach to testing programs in practice. - Shaoying Liu; Wuwei Shen; Shin Nakajima 001 (Comput. Sci. Inf. Syst., 2012)

Safe Substitution of Components in Self-Adaptive Web Applications. - Shin Nakajima 001 (APSEC (1), 2013)

Inductive Verification of Hybrid Automata with Strongest Postcondition Calculus. - Daisuke Ishii; Guillaume Melquiond; Shin Nakajima 001 (IFM, 2013)

Safe substitution for service-based applications. - Shin Nakajima 001 (QASBA@ISSTA, 2013)

Model-based Power Consumption Analysis of Smartphone Applications. - Shin Nakajima 001 (ACES-MB@MoDELS, 2013)

Combining Specification-Based Testing, Correctness Proof, and Inspection for Program Verification in Practice. - Shaoying Liu; Shin Nakajima 001 (SOFL+MSVL, 2013)

Modeling and debugging numerical constraints of cyber-physical systems design. - Thanh Nguyen Tien; Shin Nakajima 001; Huynh Quyet Thang (SoICT, 2013)

Efficient online analysis of accidental fault localization for dynamic systems using hidden Markov model. - Ning Ge 002; Shin Nakajima 001; Marc Pantel (SpringSim (TMS-DEVS), 2013)

Context-dependent product line engineering with lightweight formal approaches. - Naoyasu Ubayashi; Shin Nakajima 001; Masayuki Hirayama (Sci. Comput. Program., 2013)

Everlasting Challenges with the OBJ Language Family. - Shin Nakajima 001 (Specification, Algebra, and Software, 2014)

Model Checking of Energy Consumption Behavior. - Shin Nakajima 001 (CSDM Asia, 2014)

A Formula-Based Approach for Automatic Fault Localization of Imperative Programs. - Si-Mohamed Lamraoui; Shin Nakajima 001 (ICFEM, 2014)

Using Alloy in Introductory Courses of Formal Methods. - Shin Nakajima 001 (SOFL+MSVL, 2014)

Analyzing Lifecycle Behavior of Android Application Components. - Shin Nakajima 001 (COMPSAC Workshops, 2015)

Formal Analysis of Android Application Behavior with Real-Time Maude. - Shin Nakajima 001 (CPSNA, 2015)

Fault Localization of Energy Consumption Behavior Using Maximum Satisfiability. - Shin Nakajima 001; Si-Mohamed Lamraoui (CyPhy, 2015)

Using Real-Time Maude to Model Check Energy Consumption Behavior. - Shin Nakajima 001 (FM, 2015)

Hardened Flow-Sensitive Trace Formula for Fault Localization. - Si-Mohamed Lamraoui; Shin Nakajima 001; Hiroshi Hosobe (ICECCS, 2015)

Verifying eventuality properties of imprecise system requirements using event-B. - Hong Anh Le; Ninh-Thuan Truong; Shin Nakajima 001 (SAC, 2015)

Refinement and Proof Based Development of Systems Characterized by Continuous Functions. - Guillaume Babin; Yamine Aït Ameur; Shin Nakajima 001; Marc Pantel (SETTA, 2015)

Fault Localization of Timed Automata Using Maximum Satisfiability. - Shin Nakajima 001; Si-Mohamed Lamraoui (SOFL+MSVL, 2015)

Studying Verification Conditions for Imperative Programs. - Cláudio Belo Lourenço; Si-Mohamed Lamraoui; Shin Nakajima 001; Jorge Sousa Pinto (Electron. Commun. Eur. Assoc. Softw. Sci. Technol., 2015)

Online diagnosis of accidental faults for real-time embedded systems using a hidden Markov model. - Ning Ge 001; Shin Nakajima 001; Marc Pantel (Simul., 2015)

Dataset Coverage for Testing Machine Learning Computer Programs. - Shin Nakajima 001; Hai Ngoc Bui (APSEC, 2016)

A Formula-based Approach for Automatic Fault Localization of Multi-fault Programs. - Si-Mohamed Lamraoui; Shin Nakajima 001 (J. Inf. Process., 2016)

Implicit and explicit semantics integration in proof based developments of discrete systems (NII Shonan Meeting 2016-16). - Yamine Aït Ameur; Shin Nakajima 001; Dominique Méry (NII Shonan Meet. Rep., 2016)

Architecture-Centric Modeling, Analysis, and Veri cation of Cyber-Physical Systems (NII Shonan Meeting 2016-5). - Shin Nakajima 001; Jean-Pierre Talpin; Masumi Toyoshima; Huafeng Yu (NII Shonan Meet. Rep., 2016)

Equivalence Checking of Java Methods: Toward Ensuring IoT Dependability. - Kozo Okano; Satoshi Harauchi; Toshifusa Sekizawa; Shinpei Ogata; Shin Nakajima 001 (ICCCN, 2017)

Generalized Oracle for Testing Machine Learning Computer Programs. - Shin Nakajima 001 (SEFM Workshops, 2017)

A Generalized Approach to Verification Condition Generation. - Cláudio Belo Lourenço; Maria João Frade; Shin Nakajima 001; Jorge Sousa Pinto (COMPSAC (1), 2018)

A Net-Based Formal Framework for Causal Loop Diagrams. - Guillermina Cledou; Shin Nakajima 001 (CSDM Asia, 2018)

[Invited] Quality Assurance of Machine Learning Software. - Shin Nakajima 001 (GCCE, 2018)

Dataset Diversity for Metamorphic Testing of Machine Learning Software. - Shin Nakajima 001 (SOFL+MSVL, 2018)

A Map of Asynchronous Communication Models. - Florent Chevrou; Aurélie Hurault; Shin Nakajima 001; Philippe Quéinnec (FM Workshops (2), 2019)

Generating Biased Dataset for Metamorphic Testing of Machine Learning Programs. - Shin Nakajima 001; Tsong Yueh Chen (ICTSS, 2019)

Distortion and Faults in Machine Learning Software. - Shin Nakajima 001 (SOFL+MSVL, 2019)

Quality Evaluation Assurance Levels for Deep Neural Networks Software. - Shin Nakajima 001 (TAAI, 2019)

Consistency Checking between Java Equals and hashCode Methods Using Software Analysis Workbench. - Kozo Okano; Satoshi Harauchi; Toshifusa Sekizawa; Shinpei Ogata; Shin Nakajima 001 (IEICE Trans. Inf. Syst., 2019)

Causal Reasoning in Systems (NII Shonan Meeting 139). - Gregor Gössler; Stefan Leue; Shin Nakajima 001 (NII Shonan Meet. Rep., 2019)

Software Testing with Statistical Partial Oracles - Application to Neural Networks Software -. - Shin Nakajima 001 (SOFL+MSVL, 2020)

AI Extension of SQuaRE Data Quality Model. - Shin Nakajima 001; Takako Nakatani (QRS Companion, 2021)

Automatic Test Case and Test Oracle Generation Based on Functional Scenarios in Formal Specifications for Conformance Testing. - Shaoying Liu; Shin Nakajima 001 (IEEE Trans. Software Eng., 2022)

Fault Localization with DNN-based Test Case Learning and Ablated Execution Traces. - Takuma Ikeda; Kozo Okano; Shinpei Ogata; Shin Nakajima 001 (ISE@APSEC, 2023)

DSPOL: A High-Level Language for Defining Data Policies in Data Spaces. - Shunya Taniguchi; Shin Nakajima 001; Takashi Michikata; Hirotsugu Seike; Noboru Koshizuka (IEEE Big Data, 2024)