Specification of user-interfaces using CRUISE/OBSERV. - Aviv Cohen; Shmuel S. Tyszberowicz; Amiram Yehudai (COMPSAC, 1991)

OBSERV - A Prototyping Language and Environment. - Shmuel S. Tyszberowicz; Amiram Yehudai (ACM Trans. Softw. Eng. Methodol., 1992)

How to Implement a Safe Real-Time System: The OBSERV Implementation of the Production Cell Case Study. - Shmuel S. Tyszberowicz (Real Time Syst., 1998)

Behavioral Consistency Validation of UML Diagrams. - Boris Litvak; Shmuel S. Tyszberowicz; Amiram Yehudai (SEFM, 2003)

Reactive and Real-Time Systems Course: How to Get the Most Out of it. - Tal Lev-Ami; Shmuel S. Tyszberowicz (Real Time Syst., 2003)

Enforcing Interaction Properties in AOSD-Enabled Systems. - Constantin Serban; Shmuel S. Tyszberowicz (ICSEA, 2006)

Jose: Aspects for Design by Contract80-89. - Yishai A. Feldman; Ohad Barzilay; Shmuel S. Tyszberowicz (SEFM, 2006)

Refactoring with Contracts. - Yishai A. Feldman; Maayan Goldstein; Shmuel S. Tyszberowicz (WRT, 2007)

Locating Regression Bugs. - Dor Nir; Shmuel S. Tyszberowicz; Amiram Yehudai (Haifa Verification Conference, 2007)

The EasyCRC Tool. - Assaf Raman; Shmuel S. Tyszberowicz (ICSEA, 2007)

Derived Requirements Generation: The DRAS Methodology. - David Bar-On; Shmuel S. Tyszberowicz (SwSTE, 2007)

Refactoring Aspects into Java Code. - M. Kleyman; Shmuel S. Tyszberowicz; Amiram Yehudai (SwSTE, 2007)

AspectJTamer: The Controlled Weaving of Independently Developed Aspects. - Constantin Serban; Shmuel S. Tyszberowicz (SwSTE, 2007)

Developing Law-Governed Systems Using Aspects. - Constantin Serban; Shmuel S. Tyszberowicz; Yishai A. Feldman; Naftaly H. Minsky (J. Object Technol., 2008)

GenUTest: a unit test and mock aspect generation tool. - Benny Pasternak; Shmuel S. Tyszberowicz; Amiram Yehudai (Int. J. Softw. Tools Technol. Transf., 2009)

Generating Regression Unit Tests Using a Combination of Verification and Capture & Replay. - Christoph Gladisch; Shmuel S. Tyszberowicz; Bernhard Beckert; Amiram Yehudai (TAP@TOOLS, 2010)

KeYGenU: combining verification-based and capture and replay techniques for regression unit testing. - Bernhard Beckert; Christoph Gladisch; Shmuel S. Tyszberowicz; Amiram Yehudai (Int. J. Syst. Assur. Eng. Manag., 2011)

Data refinement based testing. - David Faitelson; Shmuel S. Tyszberowicz (Int. J. Syst. Assur. Eng. Manag., 2011)

Granulated Code Generation of Interfering Functionalities. - Igor Gelfgat; Shmuel S. Tyszberowicz; Amiram Yehudai (FedCSIS, 2012)

Projective Template-Based Code Generation. - Zeev Chared; Shmuel S. Tyszberowicz (CAiSE Forum, 2013)

Refinement-based testing of delta-oriented product lines. - Ferruccio Damiani; Christoph Gladisch; Shmuel S. Tyszberowicz (PPPJ, 2013)

Specifying a Linked Data Structure in JML for Formal Verification and Runtime Checking. - Christoph Gladisch; Shmuel S. Tyszberowicz (SBMF, 2013)

Generating JML Specifications from Alloy Expressions. - Daniel Grunwald; Christoph Gladisch; Tianhai Liu; Mana Taghdiri; Shmuel S. Tyszberowicz (Haifa Verification Conference, 2014)

JKelloy: A Proof Assistant for Relational Specifications of Java Programs. - Aboubakr Achraf El Ghazi; Mattias Ulbrich; Christoph Gladisch; Shmuel S. Tyszberowicz; Mana Taghdiri (NASA Formal Methods, 2014)

Behavior-preserving abstraction of ESTEREL programs. - Nir Koblenc; Shmuel S. Tyszberowicz (FedCSIS, 2015)

Deverywhere: Develop Software Everywhere. - Yishai A. Feldman; Ari Gam; Alex Tilkin; Shmuel S. Tyszberowicz (MOBILESoft, 2015)

Improving Design Decomposition. - David Faitelson; Shmuel S. Tyszberowicz (SETTA, 2015)

Specifying linked data structures in JML for combining formal verification and testing. - Christoph Gladisch; Shmuel S. Tyszberowicz (Sci. Comput. Program., 2015)

Computing Specification-Sensitive Abstractions for Program Verification. - Tianhai Liu; Shmuel S. Tyszberowicz; Mihai Herda; Bernhard Beckert; Daniel Grahl; Mana Taghdiri (SETTA, 2016)

Duplication for the Removal of Duplication. - Ran Ettinger; Shmuel S. Tyszberowicz (IWSC, 2016)

UML diagram refinement (focusing on class- and use case diagrams). - David Faitelson; Shmuel S. Tyszberowicz (ICSE, 2017)

Supporting Software Architecture Evolution by Functional Decomposition. - David Faitelson; Robert Heinrich; Shmuel S. Tyszberowicz (MODELSWARD, 2017)

Functional Decomposition for Software Architecture Evolution. - David Faitelson; Robert Heinrich; Shmuel S. Tyszberowicz (MODELSWARD (Revised Selected Papers), 2017)

Computing Exact Loop Bounds for Bounded Program Verification. - Tianhai Liu; Shmuel S. Tyszberowicz; Bernhard Beckert; Mana Taghdiri (SETTA, 2017)

Efficient method extraction for automatic elimination of type-3 clones. - Ran Ettinger; Shmuel S. Tyszberowicz; Shay Menaia (SANER, 2017)

Improving design decomposition (extended version). - David Faitelson; Shmuel S. Tyszberowicz (Formal Aspects Comput., 2017)

A novel model-based testing approach for software product lines. - Ferruccio Damiani; David Faitelson; Christoph Gladisch; Shmuel S. Tyszberowicz (Softw. Syst. Model., 2017)

Identifying Microservices Using Functional Decomposition. - Shmuel S. Tyszberowicz; Robert Heinrich; Bo Liu 033; Zhiming Liu 001 (SETTA, 2018)

Using Dependence Graphs to Assist Verification and Testing of Information-Flow Properties. - Mihai Herda; Shmuel S. Tyszberowicz; Bernhard Beckert (TAP@STAF, 2018)

Verification-based test case generation for information-flow properties. - Mihai Herda; Shmuel S. Tyszberowicz; Joachim Müssig; Bernhard Beckert (SAC, 2019)

Software Abstractions and Human-Cyber-Physical Systems Architecture Modelling. - Zhiming Liu 001; Jonathan P. Bowen; Bo Liu 033; Shmuel S. Tyszberowicz; Tingting Zhang (SETSS, 2019)

Emergence in cyber-physical systems: potential and risk. - Shmuel S. Tyszberowicz; David Faitelson (Frontiers Inf. Technol. Electron. Eng., 2020)

Integration of Static and Dynamic Analysis Techniques for Checking Noninterference. - Bernhard Beckert; Mihai Herda; Michael Kirsten; Shmuel S. Tyszberowicz (20 Years of KeY, 2020)

Runtime Verification of Generalized Test Tables. - Alexander Weigl; Mattias Ulbrich; Shmuel S. Tyszberowicz; Jonas Klamroth (NFM, 2021)

NoCFG: A Lightweight Approach for Sound Call Graph Approximation. - Aharon Abadi; Bar Makovitzki; Ron Shemer; Shmuel S. Tyszberowicz (CoRR, 2021)

Verifying Time Complexity of Binary Search using Dafny. - Shiri Morshtein; Ran Ettinger; Shmuel S. Tyszberowicz (F-IDE@NFM, 2021)

Log2MS: a framework for automated refactoring monolith into microservices using execution logs. - Bo Liu 033; Jingliu Xiong; Qiurong Ren; Shmuel S. Tyszberowicz; Zheng Yang (ICWS, 2022)

A lightweight approach for sound call graph approximation. - Aharon Abadi; Bar Makovitzki; Ron Shemer; Shmuel S. Tyszberowicz (SAC, 2022)

iTrustEval: A framework for software trustworthiness evaluation with an intelligent AHP-based method. - Yu Liu; Shmuel S. Tyszberowicz; Zhiming Liu 001; Bo Liu 033 (SMC, 2022)

Mono2MS: Deep Fusion of Multi-Source Features for Partitioning Monolith into Microservices. - Geng Chen; Chenlin Li; Shmuel S. Tyszberowicz; Zhiming Liu 001; Bo Liu 033 (Internetware, 2024)

DSL-MoLab: supporting model-based development of TDL-specific systems enabled by DSL. - Jie Hu; Yaozhong Zhang; Xiujuan Qin; Lvlun Wei; Fangwei Chen; Shmuel S. Tyszberowicz; Mingyue Zhang 002; Bo Liu 033 (Internetware, 2024)

The rCOS framework for multi-dimensional separation of concerns in model-driven engineering. - Bo Liu 033; Shmuel S. Tyszberowicz; Zhiming Liu 001 (J. Syst. Archit., 2024)

A Simple Trace Semantics for Asynchronous Sequence Diagrams. - David Faitelson; Shmuel S. Tyszberowicz (CoRR, 2025)